Implict parameters and monomorphism

[kahl@heraklit.informatik.unibw-muenchen.de]

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