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

Tim Peters tim_one@email.msn.com
Sun, 23 Jan 2000 15:11:49 -0500

[John Skaller]
> 	My assumption is that we want optional type checking
> and higher order functions.

I think everyone agrees on that, yes.  Although for "optional type checking"
I am *not* reading "comprehensive type inference in the absence of explicit
declarations", but "optional explicit declarations and no guarantees of type
safety in their absence".

> In general, such a system is likely to be undecidable.

I'd amend that to add "without extreme care".  Strongly typed languages like
Haskell and Miranda support both sophisticated polymorphism and higher-order
functions, without requiring declarations, yet have provably sound &
effective type inference (in the technical senses of those words:  sound ==
"correct", effective == "always terminates").

This wasn't easy to achieve, though, and a mountain of work went into
refining the base Hindley-Milner type system (which was fully developed
*before* e.g. Haskell built on top of it).  Some subtle technical
restrictions were required.


is a good starting-off point for exploring this topic (the "pitfalls" relate
entirely to the type system).

> I also suspect that the proposed system, as it stands,
> is undecidable.

For most plausible ways of filling in the holes, I believe that's correct,
except that ...

Guido is (maybe too <wink>) fond of saying that Python is "a 95% language",
and I expect that will be a Guiding Principle here.  That is, the type
system will be fudged in ways such that it remains tractable, by some
combination of compromise, restriction, and plain giving up.  For example,
it seems already to have been agreed that the type system will not be able
to express the type of Python's "map" function (although there's hope that
the type checker will "know it anyway", as a special case).

This approach doesn't appeal to the axiomatic-deductive mind, so expect not
to like it.  The technical issues are so intricate, though, that our little
group of pragmatic part-timers likely isn't capable of doing significantly
better than that.  Hindley-Milner is about as expressive as "provably
correct" gets even today.

[some great examples of difficulties, which I didn't understand
 at first because people have been writing examples such that
 "|" binds tighter than "->"; so e.g. I first read John's

    Tuple<X> -> Tuple<Y> | X -> Y


    Tuple<X> -> (Tuple<Y> | X) -> Y

instead of the intended (from context)

    (Tuple<X> -> Tuple<Y>) | (X -> Y)

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

Even Hindley-Milner gives up at times (although they don't phrase it in such
raw terms), in the sense of forbidding programs that may nevertheless be
provably correct by going outside the H-M approach (the Haskell "pitfall"
12.1 (restriction to "let-bound polymorphism") is a prime example of this).

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

As above, HOFs alone aren't enough to break the camel's back, but they sure
do put a load it.  Alas, I don't know of a simple characterization of what
is (in aggregate) enough to break it, and the H-M restrictions are so
technical in nature as to suggest a simple characterization doesn't exist.
But I'm no expert in this stuff either.