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

[skaller]

Jeremy Hylton wrote:

>   JS>   Consider a function which accepts an X, or a tuple of X's,
>   JS> such functions do exist in the standard library I think: the
>   JS> declaration:
> 
> I don't understand the problem you're describing.  If we have a
> function with the type
>     f: (X,) -> (Y,) | X -> Y    (using Guido's notation for tuple)
> and we call the function with an argument of type (1,)
>     f((1,))
> then this function application should check.  

> I imagine you're trying to specify a type that restricts the function
> to only returning a Y-tuple if it's argument is an X-tuple, but also
> accepts other non-tuple types.  I don't think it will be possible to
> specify a type that enforces that restriction (although I'm not sure).
> 
> Did I understand this example correctly?

	Yes, I think so. Some functions accept a NON-Tuple X as
a singleton tuple, where a tuple is required 'in principal'. 
Such 'conveniences' are always a bad idea -- but you can't
tell amateur language designers that kind of thing. They will
always come up with an argument that it is sound in the current
system -- and fail to see that it is also fragile and will break
if the system is generalised.

	This is the main reason C++ is such a mess: it is based
on C, which is one of the worst designed languages around.

>   JS>   Just to be clear what I believe: if the type system supports
>   JS> higher order functions, it will be undecidable.  I am NOT sure
>   JS> of this (but it sounds right).
> 
> I don't understand this claim.  I am familiar with many languages that
> have both sound static type systems and higher order functions.  Am I
> mistaking your here? 

	# let rec f () = f;;
	This expression has type unit -> 'a but is here used with type 'a

Ocaml will not accept this function. Python does:

	def f(): return f 

You can't do this in C or C++ either. The type involves type recursion.
But the function is OK: it is the type system which is broken here.

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