Jeffrey R. Lewis <jeff@galconn.com> argued that the monomorphism restriction enabled translations of let-bindungs into lambda-bindings:
let z = x + ?y in z+z
[...]
The example above becomes: (\z -> z + z) (x + ?y)
In Hindley-Milner type systems, the point about let-bindings is that they can generalise. Not all let-bindings make use of that power, but those that do cannot be converted to first-order-typed lambda-expressions. I now expand a little bit on these trivialities, but only for being able to draw parallels below. For example, the following expression cannot be converted into a lambda-expression:
let myid = \ x -> x in (myid 5, myid 'c')
This is because type inference derives a polymorphic type for the let-bound variable
myid :: a -> a
(or, more precisely, myid :: forall a . a -> a), and this polymorphism is actually needed. It is, howeverm, possible to override polymorphism by supplying a type annotation:
let myid :: Int -> Int myid = \ x -> x in (myid 5, myid 6)
This can now be converted into a lambda expresssion:
(\ myid -> (myid 5, myid 6)) ((\ x -> x) :: Int -> Int)
In Haskell, an additional point about let-bindings is that let-bound variables may have constrained types, that is, types with context, no matter whether this is a class context or an implicit parameter constraint. Lambda-bound variables must not have constrained types as long as we want constraints be well-separated from the rest of the type. Just consider: \ q -> ( \ (z :: (?y :: Int) => Int) -> q + (z with ?y = q) + ?x) The type of this would have to be (?x :: Int) => Int -> ((?y :: Int) => Int) -> Int As far as I can see, currently nobody wants that. To my mind, let-bindings that make use of the constraint-power cannot be converted to lambda-bindings in the same way as let-bindings that make use of the type generalisation power cannot be converted to (first-order) lambda-bindings. With implicit parameters, it is perfectly possible to write
let z = x + ?y in (z with ?y = 5) + (z with ?y = 6)
This is the reason why the type checker derives (given x :: Int)
z :: (?y :: Int) => Int
And the above expression cannot be converted to a lambda-expression. The situation corresponds to that with type classes, as the following expression shows:
let z () = 0 in (z () + (5 :: Int), z () + (6.5 :: Double))
where we have
z :: Num a => () -> a
Just like polymorphism, type classes can be forced away via type annotation (IF there is an instance for that class):
let z :: () -> Int z () = 0 in (z () + (5 :: Int), z () + 6)
In the paper mentioned in my last message (http://ist.unibw-muenchen.de/Haskell/ModConstraints/) we argue that this is really supplying a module (or dictionary) argument (the ``default instance''), and that more direct ways to supply module (or dictionary) arguments would be useful. One such direct way is the ``with'' clause of implicit parameters --- restricted to one-entry dictionaries. And there are no default instances for these, so they cannot be forced away via type signatures. Otherwise --- I feel I have to insist --- the situation for implicit parameters is EXACTLY the same as for type classes. Therefore, the monomorphism restriction enforces Simon's (A); and Simon's (C) would be a first step towards finally abolishing the monomorphism restriction. Another argument towards the latter is that this is not a dark, undecidable corner of the type system. With this I mean that the type inference algorithm does not NEED user-supplied type declarations in order to do its job reliably. Therefore, it should not make a difference whether I supply one or not. (As long as the monomorphism restriction prevails, I strongly urge implementors not to say just ``cannot justify context ...'', but to output the full derived type, since then I could just copy that into the source!) Best regards, Wolfram