Implict parameters and monomorphism

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

As a minor point in our draft paper

``From Type Classes to Module Constraints''

http://ist.unibw-muenchen.de/Haskell/ModConstraints/

we argue that implicit parameters and conventional type class contexts
are really the same thing.

This immediately dictated the answers to the first two questions,
and provides guidance for the third:

 > Question 1: can we "inherit" implicit parameters
 > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 > Consider this:
 > 
 > 	   f x = (x::Int) + ?y
 > 
 > where f is *not* a top-level binding.
 > From the RHS of f we'll get the constraint (?y::Int).
 > 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) => 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.

Wholeheartedly agreed --- the first would break many things.

 > Question 2: type signatures
 > ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 > OK, so is it legal to give an explicit, user type signature to f, thus:
 > 
 > 	   f :: Int -> Int
 > 	   f x = (x::Int) + ?y
 > 
 [...]
 >
 > Conclusion: the above type signature is illegal.  You'll get a message
 > of the form "could not deduce (?y::Int) from ()".

Must be so.


 > Question 3: monomorphism
 > ~~~~~~~~~~~~~~~~~~~~~~~~
 [...] 
 > 
 > Possible choices
 > ~~~~~~~~~~~~~~~~
 > (A) Always generalise over implicit parameters
 >     Bindings that fall under the monomorphism restriction can't
 > 	   be generalised
 > 
 >     Consequences:
 > 	   * Inlning remains valid
 > 	   * No unexpected loss of sharing
 > 	   * But simple bindings like
 > 		   z = ?y + 1
 > 	     will be rejected, unless you add an explicit type signature
 > 	     (to avoid the monomorphism restriction)
 > 		   z :: (?y::Int) => Int
 > 		   z = ?y + 1
 > 	     This seems unacceptable

To me, it seems just as unacceptable as the other type signatures
I have to figure out only because of the monomorphism restriction.

It is, in fact, a logical consequence of the monomorphism restriction.
So as far as the monomorphism restriction is going to be kept,
this is the way to go.

 > (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 = ?y + 1
 > 	     accepted (get value of ?y from binding site)
 > 
This is really unacceptable.
Just like the rejected alternatives
in questions 1 and 2, it relies on breaking an otherwise coherent system.

 > (C) Always generalise over implicit parameters
 >     Bindings that fall under the monomorphism restriction can't
 > 	   be generalised, EXCEPT for implicit parameters
 > 
 >     Consequences
 > 	   * Inlining remains valid
 > 	   * Unexpected loss of sharing (from the extra generalisation)
 > 	   * Simple bindings like
 > 		   z = ?y + 1
 > 	     accepted (get value of ?y from occurrence sites)
 > 
 > 
 > Discussion
 > ~~~~~~~~~
 [...]
 >
 > Choice (C) really says "the monomorphism restriction doesn't apply
 > to implicit parameters".

Precisely.

 > Which is fine, but remember that every
 > innocent binding 'x = ...' that mentions an implicit parameter in
 > the RHS becomes a *function* of that parameter, called at each
 > use of 'x'.

Just like anything that is bound to a type with a context.

 > Now, the chances are that there are no intervening 'with'
 > clauses that bind ?y, so a decent compiler should common up all
 > those function calls.  So I think I strongly favour (C).  Indeed,
 > one could make a similar argument for abolishing the monomorphism
 > restriction altogether.

Indeed, this already is an argument for abolishing the monomorphism
restriction altogether.


Best regards,

Wolfram