[Types-sig] Typing

[Jeremy Hylton]

I want to clarify a single issue you raised in your message.

>In THIS code, a simple checker will find no error, but in 
>THIS code:
>
>	decl y : int | string
>	decl x : int | string
>	for i in [0,1]:
>		x = [10,'ten'][i]
>		y = [20,'twenty][i]
>		print x + y
>
>we must issue an error, because the possibility that x is an int,
>and y is a string, and x + y would be wrong, exists .. and cannot
>be excluded by bottom up analysis. It is not definite there
>is an error .. and it is not definite that there is not.

When you say "we must issue an error," I think you should say "we must
insert a runtime check."  I realize that Guido has as a stated goal
that checked modules do not raise type errors as runtime.  But as you
say, it is impossible to check your example at compile time.

We would lose enormous expressivity if we limited ourselves to
programs that are entirely statically checkable at compile time.  I
think there is no way to avoid some amount of runtime checks.  (Heck,
Java couldn't escape them either.)

If we do issue a dynamic check for the example code, we might also
issue a compile time warning:  "Your code might raise a TypeError at
runtime: int + string."  I'm not sure how helpful this warning would
be; I expect it primarily depends on how often they occur.  (I think I
agree with your intuition that union types like these will tend to
pile up into lots of hairy unions.)

Jeremy