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

[skaller]

Jeremy Hylton wrote:
> 
> >>>>> "JS" == skaller  <skaller@maxtal.com.au> writes:
> 
>   JS>   So on the assumption that we want a rich enough type system to
> 
> You're the only person I know who is making such an assumption.

> I have assumed that we are discussing a static type system that is
> decidably verifiable; there is a necessary sacrifice of expressiveness
> in order to allow static checking of programs.  Your lengthy post
> refutes a strawman argument (although it's a lovely display of your
> erudition).

	My assumption is that we want optional type checking
and higher order functions. In general, such a system is likely to 
be undecidable. I also suspect that the proposed system, as it stands, 
is undecidable. 

	Consider a function which accepts an X, or a tuple of X's,
such functions do exist in the standard library I think:
the declaration:

	Tuple<X> -> Tuple<Y> | X -> Y #1

declares the argument type correctly -- assuming a strict left to
right matching. However, this makes the | operator non-commutative.
What that means, I'm not sure, but I guess it will make a mess
of inference -- introducing control flow into the inference
algorithm by way of ordering considerations. To give an example in

	y = f((1,)

we want the X to be 'int', not Tuple(int). Note that this example
in itself can NOT be declared inline with the syntax

	def f(x: Tuple<X> | X) -> Tuple<Y> | Y

because this is a _different_ type:

	Tuple<X> | X -> Tuple<Y> | Y  #2

[The first type is a subtype of this one. ie. stricter]

	So the problem, as I see it, is that the type
system being desribed IS that rich. in the case above,
SUPPOSE the client declared a function with an ARGUMENT
like #1, and called it with an argument like #2,
then what will the checker say?

	The program is CORRECT. I doubt that the checker
can be required to compute that: this requires calculating
the most general unifier, and for the rich type schema
being described, it isn't decidable how to do that AFAIK.

	Just to be clear what I believe: if the type
system supports higher order functions, it will be undecidable.
I am NOT sure of this (but it sounds right).

	If it does not, map, apply and reduce cannot be declared. **

	Once higher order functions are introduced,
subtyping must be calculated, and it is indecidable for functions.

	** Just to be sure you don't get confused here and think
this consideration only applies to 'functional' functions,
be aware it applies to 'functional objects' as well. In particular,
it applies to class methods. For example:

	class X:
		def f(x:A) -> A: ...
	class Y(X):
		def f(x:B) -> C

In order that class Y be a subtype of X***, it is necessary that B's
f have C <= A <= B where <= means 'is subtype of'. This is the
standard rule for methods -- returns are covariant, arguments
are contravariant.

	Checking that requires signature matching on functions,
that is, determining if a function signature is a subtype of
another.

	*** Please note VERY carefully that subtyping
is unrelated to subclassing.

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