Implict parameters and monomorphism
26 Apr 2001 09:01:29 -0000
Jeffrey R. Lewis <email@example.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
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
> 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.
\ 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
> 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
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!)