Haskell and principal types

[Karl-Filip Faxen]

Hello again!

John Hughes suggested that Haskell should have two forms of binding,
one with call-by-name (does not preserve sharing) semantics and =

polymorphism and overloading and monomorphic with call-by-need =

(preserves sharing).

The question is; would this restore principal types in general?
Actually, I don't know. I came across this problem when I was
thinking about how one would go about constructing a complete
inference algorithm for Haskell (Mark Jones's THIH algorithm, as
well as other algorithms built on W, fails to type some programs =

containing type synonyms).

So my idea was to see if was possible to do type inference in two =

passes, forgetting about type classes on the first pass, and then
go back and collect and solve class constraints. For that strategy
to work, the classes must not influence the other part of the types,
ie the type schemes derived would only need to get their context =

parts filled in by the later pass. And as far as I could see, it
was defaulting and the monomorphism restriction that could cause
trouble. And while thinking of ways to make the trouble from the
monomorphism restriction go away, I came up with this counter
example.

So I have absolutely not done any general proof about principality,
but if my idea about doing HM typechecking first and then patch the
class stuff can be made to work, I suppose that would be quite close
to a proof of principal types. And I think that John's suggestion
does fix the problem with the monomorphism restriction (since the
restriction goes away and we already have constructs with the type
of :=3D in the language, eg "case e of x -> body" or "(\x->body) e".
What remains is the defaulting mechanism.

Cheers,

   /kff