[Types-sig] Type-checked code calling unchecked code

skaller skaller@maxtal.com.au
Tue, 25 Jan 2000 00:24:23 +1100


scott wrote:

> > With Greg, you could write
> >
> > i = j() ! int
> >
> 
> Just wanted to point out that in the case of '!', you get a runtime
> error if you are wrong.  in the case of typecase, you get a compile
> time error if it's wrong (typewise, of course).  I feel like I'm
> repeating myself re: the runtime errors associated with !, but I think
> it's important that it be pointed out, since the goal as I understand
> it is greater compile time safety, and since the issue hasn't really
> been addressed at all.

Greg Stein's semantics are NOT the ones I advocate -- 
but the syntax is fine. I define

	x ! y

as an assertion, and like all assertions in Vyper -- and indeed in
Python
-- if they are wrong, then the language translator is NOT required 
to raise a TypeError, in fact, it can do anything it wants. 
In particular, it can ASSUME that the assertion holds, 
and optimise accordingly, and it can PROVE (perhaps) that the 
assertion is false, and issue a compile time diagnostic.

So you're wrong: operator ! can yield compile time diagnostics
if the semantics are suitably chosen; Greg simply didn't chose the
right semantics. <g>

-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
homepage: http://www.maxtal.com.au/~skaller
download: ftp://ftp.cs.usyd.edu/au/jskaller