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 = (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. Question 2: type signatures ~~~~~~~~~~~~~~~~~~~~~~~~~~~ OK, so it it legal to give an explicit, user type signature to f, thus: f :: Int -> Int f x = (x::Int) + ?y At first sight this seems reasonable, but it has the nasty property that adding a type signature changes the dynamic semantics. Consider this: (let f x = (x::Int) + ?y in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+5) vs (let f :: Int -> Int f x = x + ?y in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+6) Indeed, simply inlining f (at the Haskell source level) would change the dynamic semantics. 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 = (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: * 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 (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.
On Tue, Apr 24, 2001 at 04:04:54PM -0700, Simon Peyton-Jones wrote:
Question 1: can we "inherit" implicit parameters ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this:
f x = (x::Int) + ?y ... f :: Int -> Int [versus] f :: (?y::Int) => Int -> Int
Question 2: type signatures ~~~~~~~~~~~~~~~~~~~~~~~~~~~ OK, so it it legal to give an explicit, user type signature to f, thus:
f :: Int -> Int f x = (x::Int) + ?y ...
It seems desirable to provide some way to allow either possible answer to Question 1 (i.e., dynamically scoped or statically scoped ?y). Is there some syntax for that (other than providing a type signature, which I agree is not desirable)? --Dylan Thurston
Tue, 24 Apr 2001 22:51:41 -0400, Dylan Thurston <dpt@math.harvard.edu> pisze:
It seems desirable to provide some way to allow either possible answer to Question 1 (i.e., dynamically scoped or statically scoped ?y).
You can bind its value to a statically scoped variable. IMHO it shoult not be surprising that it's not just an identifier with static visibility. Since it needs not to be statically visible in a top level definition, it's normal that it applies its scoping rules in local definitions too. Why would it magically turn into an ordinary identifier for inner scopes? It dynamically appears in each place it is used. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
25 Apr 2001 07:18:50 GMT, Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> pisze:
Why would it magically turn into an ordinary identifier for inner scopes? It dynamically appears in each place it is used.
In other words since ?x is legal in an inner scope no matter whether it appears in an outer scope or not, it's meaning in the inner scope should not depend on that fact. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
On Tue, Apr 24, 2001 at 04:04:54PM -0700, Simon Peyton-Jones wrote:
Question 1: can we "inherit" implicit parameters ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this:
f x = (x::Int) + ?y ... f :: Int -> Int [versus] f :: (?y::Int) => Int -> Int
Question 2: type signatures ~~~~~~~~~~~~~~~~~~~~~~~~~~~ OK, so it it legal to give an explicit, user type signature to f, thus:
f :: Int -> Int f x = (x::Int) + ?y ...
It seems desirable to provide some way to allow either possible answer to Question 1 (i.e., dynamically scoped or statically scoped ?y). Is there some syntax for that (other than providing a type signature, which I agree is not desirable)?
One alternative (which I played around with a while ago) is to have implicit parameters explicitly bound at a function definition. Thus if we want to "inherit" our implicit paramater, we would have: f ?y x = (x :: Int) + ?y with type f :: (?y :: Int) => Int -> Int If the "?y" isn't put on the function binding, then it needs to have occurred in an enclosing function binding. Eg g ?y = let f x = ... in ... The same approach extends to definitions of non-functions, now taking on function-like syntax, to take implicit parameters. For the "z" example, we get z ?y = (x::Int) + ?y This still gives us a type of z :: (?y :: Int) => Int but the "function-like" nature is now explicit, and thus IMHO, in this case there is a more reasonable argument for dropping the monomorphism restriction. If I write let z ?y = x + ?y in z + z In seems far more obvious that z will be evaluated twice. Hmmm. I haven't made this particularly clear, but hopefully most of you can see what I am getting at. Semantics is entirely as with existing implicit parameter proposals. This is all just syntax. -Rob
On Wed, 25 Apr 2001, Robert Ennals wrote:
Thus if we want to "inherit" our implicit paramater, we would have:
f ?y x = (x :: Int) + ?y
I like the current solution better. They are called "implicit parameters" because they are, well, implicit :-)
The semantics is still implicit. When one calls the function f, one would only explicitly pass x, not y. Eg one can do g :: (y :: Int) => Int g ?y = f 1 And for top level functions, one could make it optional anyway, as there is nowhere else for the variable to have come from. -Rob
Tue, 24 Apr 2001 16:04:54 -0700, Simon Peyton-Jones <simonpj@microsoft.com> pisze:
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.
I agree! -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
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
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
Jeffrey R. Lewis <jeff@galconn.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 lambda-expressions. 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 lambda-expression:
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. Just consider: \ 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 expression shows:
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 (http://ist.unibw-muenchen.de/Haskell/ModConstraints/) 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!) Best regards, Wolfram
participants (7)
-
Dylan Thurston -
Jeffrey R. Lewis -
kahl＠heraklit.informatik.unibw-muenchen.de -
Marcin 'Qrczak' Kowalczyk -
qrczak＠knm.org.pl
-
Robert Ennals -
Simon Peyton-Jones