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

[Jeremy Hylton]

>>>>> "JS" == skaller  <skaller@maxtal.com.au> writes:

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

  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.  Since 
    (X,) -> (Y,) <: X -> Y
it seems like the first half is unnecessary.

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?

  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?  Perhaps you mean that a language with higher
order funtions and <some other property that I can't recover from
context>, is undecidable?  If so, exactly what property is it that
gets in the way?

Jeremy