[Python-3000] Type Comparisons with Godel Numbers

[Bill Birch]

On Sat, 22 Apr 2006 06:39 pm, Guido van Rossum wrote:
...
>
> No. This is the kind of thing that would very quickly turn "optional"
> typing into *mandatory* typing. One library package adds type
> declarations. Now all packages that use it are required to either add
> type declarations or explicit conversions or checks. The cost of
> repeated explicit conversions/checks strongly suggests that adding
> type declaration is the better choice -- and now you have a ripple
> effect (similar to the way 'const' declarations, once added, cascade
> in C or C++ code). Soon enough the entire library uses type
> declarations and now all user code is faced with the same choice. All
> style guides will strongly suggest type declarations. And we end up
> with Java without curly braces.
recapping:

What exactly is list[int]? -  list[int] is shorthand for

	type(list[0]) <: int and  type(list[1]) <: int and type(list[2]) <: int ...

where "t1 <: t2" means t1 is a structural subtype of t2

otherwise stated as:
	
	for any natural number n, list[n] <: int 

which is essentially an un-typed viewpoint.

So we  add the type variable to the runtime object. Luca Cardelli's paper on 
the typed lambda calculus has a lot to say about adding types 
(http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.A4.pdf) If I 
understand the math right, we can expressed this as a bounded universal 
quantifier? 

	all[a <: int] list[a]

You would have to construct it specifically with the type attribute:

	var = list[int]               # py3k
	var[0] = 42                  # OK
	var[1] = "foo"       # run-time type error

Java arrays work this way.  quote "More formally: an assignment to an element 
of an array whose type is A[], where A is a reference type, is checked at 
run-time to ensure that the value assigned can be assigned to the actual 
element type of the array, where the actual element type may be any reference 
type that is assignable to A." see 
(http://java.sun.com/docs/books/jls/second_edition/html/arrays.doc.html)        

The implications of this for the programmer are that type errors would be 
found closer to the source. But, as was pointed out there will be a 
proliferation of listOf(T) constructors.  And a proliferation of performance 
soaks. 

so...

In my experience deep type checking at runtime is really useful, common, but 
rarely called type checking. Normally we to write it manually (and call it 
"input validation" or "checking preconditions"). Usually on major system 
boundaries.  Especially in distributed systems. I would be happy to pay the 
cost of run-time type checking if I could invoke it explicitly. Then I could 
choose where the performance hit happens and how often.

But how can dynamic type checks be made obvious and explicit syntactically?

Maybe with an annotation:

@enforce_types
def func(x: t1, y: t2) -> t3:
    ...body...
 
or with an explicit check:

def func(x, y) :
	if not x, y <: t1, t2:
		throw "mate, you have a type error"
		
Perhaps we could limit type definitions to interfaces only, and allow 
preconditions and postconditions there. This would be simple to grasp. If you 
implement an interface, you'll be paying the cost of runtime type checks.  
After all the whole point of interfaces in Python is to enforce compliance 
with a standard. Remember this is not Java, we already have multiple 
inheritance.