RE: Solution to the monomorphism restriction/implicit parameter problem
| I just figured out why the monomorphism restriction interacts so weirdly | with implicit parameters, and how to fix it. I'm afraid that I have not read all of the recent exciting flood of messages carefully, but I do remember that the interaction of the monomorphism restriction with implicit parameters was the subject of a long debate some time ago. Indeed, it leads to strange things, as you have found. Below I reproduce a long comment from TcSimplify.lhs (one of GHC's modules) that describes the problem and GHC's solution. It explicitly points out that the currently-adopted solution means that inlining (beta reduction) is not always valid. This is undoubtedly a bad thing. The comment would be better enshrined in GHC's documentation. You say that "All implementations should be changed so that they do the right thing". If only we knew what the Right Thing is! I believe that your suggestion is * adopt solution (C) in the list below (always generalise implicit parameters) * but reject any program for which that would cause the implicit function to be called more than once Maybe that's a good plan, but if so it'd be better to apply it to all overloaded bindings. That is: abandon the monomorphism restriction altogether; instead always generalise every binding (whether function or non-function binding) but warn or reject the program if it seems that the implicit function might be called more than once. Simon Comments from TcSimplify 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. Possible choices ~~~~~~~~~~~~~~~~ (A) Always generalise over implicit parameters Bindings that fall under the monomorphism restriction can't be generalised Consequences: * Inlining 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 (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) (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 ~~~~~~~~~~ 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 = (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 innocent binding 'x = ...' 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 those function calls. So I think I strongly favour (C). Indeed, one could make a similar argument for abolishing the monomorphism restriction altogether. BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
On Tue, 5 Aug 2003, Simon Peyton-Jones wrote:
I'm afraid that I have not read all of the recent exciting flood of messages carefully,
Hi, I'm glad to see that you're around, and I'm very much looking forward to any comments you may have about my proposal.
You say that "All implementations should be changed so that they do the right thing". If only we knew what the Right Thing is!
My solution *is* the Right Thing. :-) It really did exist all along. I think that once you read and understand my implicit parameter proposal this will become clear.
Comments from TcSimplify
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,
No, it's not necessary that z have that type, just that it behave exactly as though it had that type. The reason the expression let f = (<) in (f 'a' 'b', f 'a' 'b') is not rejected even with the monomorphism restriction turned on is that there's a monomorphic specialization of f that behaves exactly as the polymorphic f would have *in this particular expression* -- and that's what actually gets used. Similarly, the expression
let z = x + ?y in z+z
need not be rejected, because there's a monomorphic "specialization" of z that behaves exactly as the polymorphic version would have in this expression -- namely z = (x + ?y) {?y = @y}. (See my implicit parameter proposal for a definition of the new syntax.) -- Ben
I wrote:
My solution *is* the Right Thing. :-)
What I meant is: it always preserves the validity of inlining, it always preserves sharing, and it rejects otherwise-correct programs only in situations which are (I expect) uncommon in practice. -- Ben
participants (2)
-
Ben Rudiak-Gould -
Simon Peyton-Jones