Implict parameters and monomorphism

[Jeffrey R. Lewis]

Simon Peyton-Jones wrote:

> This is a long message about the design of implicit parameters.
> In particular, it is about the interaction of the monomorphism
> restriction with implicit parameters.  This issue was discussed
> in the original implicit-parameter paper, but I wanted to articulate
> it afresh and propose some design choices
>
> Simon
>
>
> Question 3: monomorphism
> ~~~~~~~~~~~~~~~~~~~~~~~~
> There's a nasty corner case when the monomorphism restriction bites:
>
>         z = (x::Int) + ?y
>
> The argument above suggests that we *must* generalise
> over the ?y parameter, to get
>         z :: (?y::Int) => Int,
> but the monomorphism restriction says that we *must not*, giving
>         z :: Int.
> Why does the momomorphism restriction say this?  Because if you have
>
>         let z = x + ?y in z+z
>
> you might not expect the addition to be done twice --- but it will if
> we follow the argument of Question 2 and generalise over ?y.

It may help to clarify the question by giving a concrete semantics to the monomorphism restriction.  I'll focus on a simplification it that will suffice: a binding is restricted if it is of the form `x = E'.  The monomorphism restriction can then be understood by the following translation:

[[ let x = E1 in E2 ]] = (\x -> E2) E1
[[ let f p1 .. pn = E1 in E2 ]] = let f = \p1 .. pn -> E1 in E2 ]]

where `let' in the translation is a straight polymorphic let - no more funny business w/ mono restrictions, etc.

In other words, the monomorphism restriction converts certain let bindings to lambda bindings.  The typing and sharing consequences follow from this translation.  This is a bit naive, because a restricted binding can still be polymorphic over non-"constrained" variables (where "constrained" here means constrained by a type class predicate), but this just requires a more detailed translation to get right, it doesn't harm the main point.

The example above becomes:
    (\z -> z + z) (x + ?y)

Given this semantics, which design choice makes the most sense?

(A) Doesn't seem to make sense.  Under the translation, there's no basis for rejecting the binding - you've simply got a lambda binding, and generalization doesn't come into play.

(B)  Follows naturally from the translation.  A restricted binding is a lambda binding, and thus isn't generalized.  An unrestricted binding is a polymorphic let binding, and thus *is* generalized.

(C) Doesn't immediately follow from the translation because the criteria for a restricted binding has become more complex.  Indeed, it's no longer syntactic - we have to do some inference before deciding whether a binding is restricted or not.  Not necessarily a bad thing, it just makes the whole thing more complex.  But once you've extended the definition of a restricted binding to exclude ones with implicit parameters, everything follows as a consequence of the translation, thus it is a coherent design choice.

My preference?  B is a straightforward consequence of the monomorphism restriction (as understood by my translation).  Hence, that's how hugs does it, and how GHC 4.08 does it.  GHC 5.00 adopted A, but I don't think that will last for long.  C might be nice.  I don't have strong preferences.

But what about Simon's point about inlining?  I believe it's a bit misleading in the following sense: if you understand the monomorphism restriction to restrict certain bindings to be lambda bindings, then inlining of restricted bindings is beta reduction.  Beta reduction in the face of implicit parameters holds, but involves a bit more work, and thus shouldn't be done naively (see the POPL paper).  Bottom line: inlining can be done in the case of B, but requires more care.  Incidentally, the compiler itself needn't worry about this, because it does all of its transformations after the dictionary translation (where all the implicit parameters have been translated to explicit parameters).

As a side note: interactions between the monomorphism restriction and defaulting can also break inlining.  You already have to be careful.

But I don't really want to oversell that point.  I think option C might be nice, because it would make it easier to do source code inlining.  But we could also achieve this by just abolishing the monomorphism restriction!  So I'm a little torn by C.  I see the benefits, but it complicates the already complicated monomorphism restriction, and I just can't help but think that if we're going to go that far, we'd be better off just getting rid of the monomorphism restriction, and making this whole thing a non-issue.  If we're not willing to get rid of the monomorphism restriction, I'd stick with B.

--Jeff