Implict parameters and monomorphism

[Simon Peyton-Jones]

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 1: can we "inherit" implicit parameters
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:

	f x =3D (x::Int) + ?y

where f is *not* a top-level binding.
From the RHS of f we'll get the constraint (?y::Int). =20
There are two types we might infer for f:

	f :: Int -> Int

(so we get ?y from the context of f's definition), or

	f :: (?y::Int) =3D> Int -> Int

At first you might think the first was better, becuase then
?y behaves like a free variable of the definition, rather than
having to be passed at each call site.  But of course, the WHOLE
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.

Question 2: type signatures
~~~~~~~~~~~~~~~~~~~~~~~~~~~
OK, so it it legal to give an explicit, user type signature to f, thus:

	f :: Int -> Int
	f x =3D (x::Int) + ?y

At first sight this seems reasonable, but it has the nasty property
that adding a type signature changes the dynamic semantics.=20
Consider this:

	(let f x =3D (x::Int) + ?y
 	 in (f 3, f 3 with ?y=3D5))  with ?y =3D 6

		returns (3+6, 3+5)
vs
	(let f :: Int -> Int=20
	     f x =3D x + ?y
	 in (f 3, f 3 with ?y=3D5))  with ?y =3D 6

		returns (3+6, 3+6)

Indeed, simply inlining f (at the Haskell source level) would change the

dynamic semantics. =20

Conclusion: the above type signature is illegal.  You'll get a message
of the form "could not deduce (?y::Int) from ()".

Question 3: monomorphism
~~~~~~~~~~~~~~~~~~~~~~~~
There's a nasty corner case when the monomorphism restriction bites:

	z =3D (x::Int) + ?y

The argument above suggests that we *must* generalise=20
over the ?y parameter, to get=20
	z :: (?y::Int) =3D> Int,
but the monomorphism restriction says that we *must not*, giving
	z :: Int. =20
Why does the momomorphism restriction say this?  Because if you have

	let z =3D 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.



Possible choices
~~~~~~~~~~~~~~~~
(A) Always generalise over implicit parameters
    Bindings that fall under the monomorphism restriction can't
	be generalised
=09

    Consequences:
	* Inlning remains valid
	* No unexpected loss of sharing
	* But simple bindings like
		z =3D ?y + 1
	  will be rejected, unless you add an explicit type signature
	  (to avoid the monomorphism restriction)
		z :: (?y::Int) =3D> Int
		z =3D ?y + 1
	  This seems unacceptable
=09

(B) Monomorphism restriction "wins"
    Bindings that fall under the monomorphism restriction can't
	be generalised
    Always generalise over implicit parameters *except* for bindings
	that fall under the monomorphism restriction

    Consequences
	* Inlining isn't valid in general
	* No unexpected loss of sharing
	* Simple bindings like
		z =3D ?y + 1
	  accepted (get value of ?y from binding site)

(C) Always generalise over implicit parameters
    Bindings that fall under the monomorphism restriction can't
	be generalised, EXCEPT for implicit parameters
   =20
    Consequences
	* Inlining remains valid
	* Unexpected loss of sharing (from the extra generalisation)
	* Simple bindings like
		z =3D ?y + 1
	  accepted (get value of ?y from occurrence sites)


Discussion
~~~~~~~~~~
None of these choices seems very satisfactory.  But at least we should
decide which we want to do.

It's really not clear what is the Right Thing To Do.  If you see

	z =3D (x::Int) + ?y

would you expect the value of ?y to be got from the *occurrence sites*
of 'z', or from the valuue of ?y at the *definition* of 'z'?  In the
case of function definitions, the answer is clearly the former, but
less so in the case of non-fucntion definitions.   On the other hand,
if we say that we get the value of ?y from the definition site of 'z',
then inlining 'z' might change the semantics of the program.

Choice (C) really says "the monomorphism restriction doesn't apply
to implicit parameters".  Which is fine, but remember that every=20
innocent binding 'x =3D ...' that mentions an implicit parameter in
the RHS becomes a *function* of that parameter, called at each
use of 'x'.  Now, the chances are that there are no intervening 'with'
clauses that bind ?y, so a decent compiler should common up all=20
those function calls.  So I think I strongly favour (C).  Indeed,
one could make a similar argument for abolishing the monomorphism
restriction altogether.