From: Barry Margolin
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <5unflv$jbm@tools.bbnplanet.com>
In article <··············@work.nlm.nih.gov>,
Larry Hunter  <······@nlm.nih.gov> wrote:
>
>Vassil Nikolov asks:
>
>  Consider:
>
>  (declare (number x))
>  (if (numberp x) (1+ x) (cdr x))
>
>  Is the compiler justified in refusing to compile that code because of the
>  apparent application of CDR to a non-cons?
>
>There is no error because the else clause (CDR X) is unreachable.  Since X
>can be assumed to be a number (from the declaration), then the test clause
>will always be true.  The compiler would be entirely justified in optimizing
>this IF to machine code that just increments X.

While this is true, it's probably not relevant to his question.

What he seems to have is a compiler that's smart enough to recognize that
CDR is not applicable to X, which is a very easy determination for it to
make.  However, determining that the (cdr x) form cannot be reached
requires a more sophisticated level of flow analysis.  I can very easily
imagine compilers that perform the type check but not the optimization.

I think it would be reasonable for a compiler to issue a warning about this
code, but it shouldn't refuse to compile it.  A compiler should only refuse
to compile code when it can prove that an invalid operation will be
attempted; a compiler that refuses the above code clearly hasn't done
adequate analysis to prove it (since it would be proving a falsehood).

-- 
Barry Margolin, ······@bbnplanet.com
GTE Internetworking, Powered by BBN, Cambridge, MA
Support the anti-spam movement; see <http://www.cauce.org/>
Please don't send technical questions directly to me, post them to newsgroups.

From: ET
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <5uph7s$q8b$1@newsie2.cent.net>
Barry Margolin wrote in article <··········@tools.bbnplanet.com>...

>A compiler should only refuse
>to compile code when it can prove that an invalid operation will be
>attempted.

Which is equivalent to solving the halting problem.  I might *never* load
and run the compiled image.
From: Vassili Bykov
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <873557821.18412@dejanews.com>
In article <············@newsie2.cent.net>, "ET" <········@eval-apply.com>
wrote:
> Barry Margolin wrote in article <··········@tools.bbnplanet.com>...
> >A compiler should only refuse
> >to compile code when it can prove that an invalid operation will be
> >attempted.
>
> Which is equivalent to solving the halting problem. [...]

I can't believe it is, unless one tries to make unnecessary
generalizations of a reasonable practical issue.

-------------------==== Posted via Deja News ====-----------------------
      http://www.dejanews.com/     Search, Read, Post to Usenet
From: ET
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <5v8vrb$gg6$1@newsie2.cent.net>
 It is a generalization, but I don't think it is unreasonable.
In the trivial case, if I have a file with the following code:

(+ 'x 3)

it is pretty obvious that one couldn't expect to run it,
and therefore compiling it becomes moot.  However, if
I add a conditional,

(if (some-nontrivial-condition-p)
    (+ 'x 3))

I have something completely different.  This expression
is an error (meaningless?) only if some-nontrivial-condition-p halts and
returns true.

This is a practial case.

Vassili Bykov wrote in article <···············@dejanews.com>...

>In article <············@newsie2.cent.net>, "ET" <········@eval-apply.com>
>wrote:
>> Barry Margolin wrote in article <··········@tools.bbnplanet.com>...
>> >A compiler should only refuse
>> >to compile code when it can prove that an invalid operation will be
>> >attempted.
>>
>> Which is equivalent to solving the halting problem. [...]
>
>I can't believe it is, unless one tries to make unnecessary
>generalizations of a reasonable practical issue.
>
>-------------------==== Posted via Deja News ====-----------------------
>      http://www.dejanews.com/     Search, Read, Post to Usenet
From: Barry Margolin
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <5va65e$37g@pasilla.bbnplanet.com>
In article <············@newsie2.cent.net>, ET <········@eval-apply.com> wrote:
> It is a generalization, but I don't think it is unreasonable.
>In the trivial case, if I have a file with the following code:
>
>(+ 'x 3)
>
>it is pretty obvious that one couldn't expect to run it,
>and therefore compiling it becomes moot.  However, if
>I add a conditional,
>
>(if (some-nontrivial-condition-p)
>    (+ 'x 3))
>
>I have something completely different.  This expression
>is an error (meaningless?) only if some-nontrivial-condition-p halts and
>returns true.
>
>This is a practial case.

So the compiler isn't allowed to refuse to compile this, because it can't
solve the halting problem.  I believe that's what I implied.  However,
consider this case:

(if (program-halts-p #'some-function)
    (+ 'x 3)
    (+ 'x 4))

You don't need to solve the halting problem to know that this form is
undefined, so a compiler could refuse to compile this.

-- 
Barry Margolin, ······@bbnplanet.com
GTE Internetworking, Powered by BBN, Cambridge, MA
Support the anti-spam movement; see <http://www.cauce.org/>
Please don't send technical questions directly to me, post them to newsgroups.
From: ET
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <5ve5to$ifc$1@newsie2.cent.net>
 Barry Margolin wrote in article <··········@pasilla.bbnplanet.com>...>So the compiler isn't allowed to refuse to compile this,
because it can't
>solve the halting problem.  I believe that's what I implied.  However,
>consider this case:
>
>(if (program-halts-p #'some-function)
>    (+ 'x 3)
>    (+ 'x 4))
>
>You don't need to solve the halting problem to know that this form is
>undefined, so a compiler could refuse to compile this.

I don't know.  If SOME-FUNCTION were defined as the read-eval-print-loop,
couldn't I reasonably expect this conditional to act just like the lisp
interpreter until I exited?
From: Rob Warnock
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <5vl1c4$1833a@fido.asd.sgi.com>
Barry Margolin  <······@bbnplanet.com> wrote:
+---------------
| (if (program-halts-p #'some-function)
|     (+ 'x 3)
|     (+ 'x 4))
| 
| You don't need to solve the halting problem to know that this form is
| undefined, so a compiler could refuse to compile this.
+---------------

Unless somebody did a (set! + my-whizzy-extended-plus) earlier...


-Rob

-----
Rob Warnock, 7L-551		····@sgi.com   http://reality.sgi.com/rpw3/
Silicon Graphics, Inc.		Phone: 650-933-1673 [New area code!]
2011 N. Shoreline Blvd.		FAX: 650-933-4392
Mountain View, CA  94043	PP-ASEL-IA
From: Rob Warnock
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <5vl1fh$v0gq@fido.asd.sgi.com>
Whoops!  I just wrote:

+---------------
| Unless somebody did a (set! + my-whizzy-extended-plus) earlier...
+---------------

Sorry, for a second I forgot this wasn't comp.lang.scheme.
(Hmmm... Now how do you say the same thing in CL...?)


-Rob

-----
Rob Warnock, 7L-551		····@sgi.com   http://reality.sgi.com/rpw3/
Silicon Graphics, Inc.		Phone: 650-933-1673 [New area code!]
2011 N. Shoreline Blvd.		FAX: 650-933-4392
Mountain View, CA  94043	PP-ASEL-IA
From: Barry Margolin
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <5vl2dt$pet@pasilla.bbnplanet.com>
In article <···········@fido.asd.sgi.com>,
Rob Warnock <····@rigden.engr.sgi.com> wrote:
>+---------------
>| Unless somebody did a (set! + my-whizzy-extended-plus) earlier...
>+---------------
>
>Sorry, for a second I forgot this wasn't comp.lang.scheme.
>(Hmmm... Now how do you say the same thing in CL...?)

You don't.  In CL, the consequences are undefined if you redefine any of
the functions in the COMMON-LISP package.

-- 
Barry Margolin, ······@bbnplanet.com
GTE Internetworking, Powered by BBN, Cambridge, MA
Support the anti-spam movement; see <http://www.cauce.org/>
Please don't send technical questions directly to me, post them to newsgroups.
From: Gareth McCaughan
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <86en71s772.fsf@g.pet.cam.ac.uk>
Someone from Emergent Technologies wrote:

> >A compiler should only refuse
> >to compile code when it can prove that an invalid operation will be
> >attempted.
> 
> Which is equivalent to solving the halting problem.  I might *never* load
> and run the compiled image.

Surely all this means is that no compiler can guarantee to ignore
every bit of code that won't ever be executed. Is this really a
problem?

-- 
Gareth McCaughan       Dept. of Pure Mathematics & Mathematical Statistics,
·····@dpmms.cam.ac.uk  Cambridge University, England.
From: ET
Subject: Re: when type mismatch can be legal?
Date: 
Message-ID: <5v910i$k7o$1@newsie2.cent.net>
Gareth McCaughan wrote in article <··············@g.pet.cam.ac.uk>...

>Someone from Emergent Technologies wrote:
>
>> >A compiler should only refuse
>> >to compile code when it can prove that an invalid operation will be
>> >attempted.
>>
>> Which is equivalent to solving the halting problem.  I might *never* load
>> and run the compiled image.
>
>Surely all this means is that no compiler can guarantee to ignore
>every bit of code that won't ever be executed. Is this really a
>problem?

Yes (although it took me a moment to parse that first sentence).
I think that in all but the most trivial of cases, the compiler will be
unable to prove what *must* be executed, I also think that the compiler
shouldn't refuse to compile code it *thinks* *might* be executed, even
if such code is nonsensical.  So I think the compiler basically should
*(almost) never* refuse to compile (syntactically correct) code.