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


_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to