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

[skaller]

Greg Stein wrote:

> > 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 ]

These semantics are 

	(a) incoherent/inconsistent
	(b) not the same as what I propose

I want to explain both points. (b) first:
I propose that if the test were to fail at any point
in the execution of the program, the program is invalid,
and the translator can do anything it wants: behaviour is
undefined. So the test can be elided.
If the test would always succeed, then
it can be elided. It follows the test can ALWAYS be
elided.

Now for (a). There is an assumption: that there is no definite
algorithm given for deducing if the test will fail.
In this case, it is possible that compiler (A) deduces
the test will always fail, and rejects the program,
while compiler (B) isn't smart enough, and compiles code
to raise an exception. In this case, a programmer
may catch the exception and handle it, and this
behaviour would be required of the language.
But that is NOT the behaviour (A) produced.
If one compiler can reject the program, it CANNOT be
a valid program, and in that case, a requirement
on a compiler (that it throw an exception if it is dumb)
cannot be made to stick, since the program is in error.

I think you must decide that the semantics require
a run time error ALWAYS, or, that the test can
be elided ALWAYS. There is no half way ground.

The current requirements for assertion statements
are, effectively, that the test can be elided,
and therefore, invalid programs exist. The fact
that the current CPython interpreter in non-optimising
mode raises an exception is nicety of that particular
implementation, not a requirement of the language.

I'm assuming 

	1) there is ONE python language
	2) both the optimising and non-optimising
		byteocode compiler conform to the semantics

and from this I deduce the above language semantics.
Remember language semantics are constraints on translators,
they're not specifications of what a particular tool does
in cases that no particular behaviour is required.

-- 
John Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia
homepage: http://www.maxtal.com.au/~skaller
voice: 61-2-9660-0850