[Types-sig] type-assert operator optimizations (was: New syntax?)

[Greg Stein]

On Tue, 21 Dec 1999, skaller wrote:
> Greg Stein wrote:
>  
> > I think that we definitely want to be able to construct and use typedecl
> > objects at runtime. That's why I prefer the typedef unary operator over
> > your "sub-language."
> 
> Are these options mutually exclusive?

I'm not sure that I understand this question. I think some context was
lost (i.e. what is the sub-language).

> I've implemented operator ! in Viper now, x!t checks type(x) is t, 
>...
> My current feeling: I quite like it -- but the above
> is the only use I have tried, other than specifically 
> for testing it. My feeling, also, is that in those
> circumstances where the test would fail, then the
> program should be considered in error (that is,
> it is not legitimate practice to catch and handle
> the TypeError, so that if a compiler can prove it would
> be raised, it is entitled to reject the program,
> and a lint like checker, to issue a diagnostic.
> [The explicit test, like in the second example above,
> should be used if it is desired to catch and handle
> the raised TypeError]
> 
> This means that the x!t can be optimised to x,
> without affecting strictly conforming program
> semantics.

If the compiler can definitively state that the test will never fail, then
it doesn't have to include a runtime check.

If the compiler can definitively state that the test will always fail,
then it can issue an error and refuse to compile.
[ with the caveat of catching exceptions ]

If the compiler believes that it might fail in some cases, then it could
issue a warning (and go ahead and insert a runtime check).
[ and yes, there can be switches to avoid issuing warnings ]

Cheers,
-g

-- 
Greg Stein, http://www.lyra.org/