Haskell and principal types

[Karl-Filip Faxen]

Hi all!

I've been spending some time the last year writing up a formalization 
of the Haskell type system (actually, most of the static semantics).
In doing so, I've come across an oddity. It seems that Haskell does not 
have the principal type property, ie there are Haskell expressions
which, in a given typing environment, can be assigned at least two types
that are not generic instances of each other but can not be assigned
any type more generic that the two. The culprit is the monomorphism 
restriction. I was kind of surprised, thinking that principal types
were likely to hold for Haskell, but it seems not.

The monomorphism restriction goes like this in my inference rules:

If a declaration group contains a pattern binding with a nonvariable pattern
or one where there is no type signature for the variable, then the context
parts of the type schemes derived for the bound variables must be empty.

The difference to for instance "Typing Haskell in Haskell" is that my
formalization is a set of inference rules (starting from the draft static
semantics by Peyton Jones and Wadler), so many different types can be 
derived for the same typing environment and expression, wheras THIH is 
a program which computes a single type.

So here is the offending program:

class IsNil a where
  isNil :: a -> Bool

instance IsNil [b] where
  isNil [] = True
  isNil _  = False

f x y = let g = isNil
         in (g x, g y)

The monomorphism restriction applies to the binding of "g" since
there is no type signature. Thus it is not legal to derive 
"forall a . IsNil a => a -> Bool", but two legal possibilities are

- forall b . [b] -> Bool, and
- a -> Bool (without quantification and with "IsNil a" among the predicates).

These two choices lead to different types for "f":

- forall a b . [a] -> [b] -> (Bool,Bool), and
- forall a . IsNil a => a -> a -> (Bool,Bool)

These two are incomparable (neither is a generic instance of the other). 
I can not see that it is legal to derive a type for "g" which will allow
some type for "f" that is more general than both of these.

As far as I can see, the inference algorithm from "Typing Haskell in Haskell" 
would give the second type, which is also what GHC derives.

The trick here is the instance declaration for "IsNil [a]" which has an
empty instance context, ie it is not important what the element type is.

So, is this already well known in the Haskell community, or is it a new 
result? Of course, it is not a result until one has *proved* that *no*
type more general than the two above is derivable, but it is a
strong conjecture. In the "Type Classes in Haskell" paper from TOPLAS,
the smaller system without the monomorphism restriction was conjectured
to have principal types. Also, the Haskell Report (section 4.1.4) states:

"Haskell 's extended Hindley-Milner type system can infer the principal 
type of all expressions, including the proper use of overloaded class 
methods (although certain ambiguous overloadings could arise, as described in 
Section 4.3.4)."

But there is no ambiguity involved here.

Cheers,

     /kff

Jones: Typing Haskell in Haskell, in Proceedings of the Third Haskell Workshop
Hall et al: Type Classes in Haskell, TOPLAS vol 18 no 2
Peyton Jones and Wadler: A Static Semantics for Haskell, draft paper, Glasgow