Haskell and principal types

[John Hughes]

	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)

Interesting.

Every now and then I propagate for replacing the MR by two forms of binding:

       pat = expr    -- call by NAME binding, fully polymorphic and overloaded
       pat := expr   -- call by NEED binding, completely monomorphic

The point is to make the programmer aware of when monomorphism applies, so its
consequences are not surprising, and also aware (with an = binding) that there
is a risk of recomputation. It sounds as though Clean has adopted a similar
idea.

With "g = isNil", the type of f becomes

     forall a b. (IsNil a, IsNil b) -> a -> b -> (Bool, Bool)

With "g := isNil", it becomes

     forall a. IsNil a => a -> a -> (Bool, Bool)

The two incomparable types for f become types of two different programs;
problem solved (in this example at least).

Karl-Filip, would this idea restore the principal type property in general?

John Hughes