[Types-sig] how to do a typecase? (was: Static typing: Towards closure?)

skaller skaller@maxtal.com.au
Tue, 25 Jan 2000 00:47:56 +1100


Tim Peters wrote:
> 
> [John Skaller, on def f(): return f]
> > ...
> >       The question is: what will a type checker do,
> > seeing this function? Will it loop forever trying to compute
> > the type of f?
> 
> I still won't call this a "type checking" problem; it's a (potential)
> problem for a type *inferencer*, but:
> 
> >       The answer is: probably. And we must allow this if type
> > declations are optional. The only way to disallow the above
> > function is to require everything be explicitly typed, in
> > which case there is no way to name the type of the function
> > above.
> 
> Bingo.  Checking that use matches declaration is easier than inferring
> declaration from use.  "Mere checking" is hard enough for a first version,
> though!

I don't think  these two things are separable.
Consider:

	decl x : int
	y = 1
	x = y

How can you check y = x, if you do not infer the type of y?
The RHS of an assignment is an EXPRESSION: the type of the
expression MUST be deduced in order to check that it is compatible
with the LHS variable.

In the very simplest of cases, where the types of all identifiers
(including all functions) are known and monomorphic, a single
bottom up pass will compute the type of any expression.

This is one sense in which Guido's 'checked module' idea makes
sense, because it requires precisely that -- provided unchecked
modules are not imported.

As soon as ANY untyped identifier enters the picture, we're stuffed.
It is NOT good enough to assume the type is 'ANY', since that is
guarranteed to cause a type error in almost every possible use.
[That is, almost all functions/expressions propogate type information:
their type depends on the types of the component subexpressions]

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