The madness of implicit parameters: cured?
When I first learned about implicit parameters I thought they were a great idea. The honeymoon ended about the time I wrote some code of the form "let ?foo = 123 in expr2", where expr2 used ?foo implicitly, and debugging eventually unearthed the fact that ?foo's implicit value was not being set to 123 in expr2. That was enough to scare me off of using implicit parameters permanently. More recently, I've realized that I really don't understand implicit parameters at all. They seemed simple enough at first, but when I look at an expression like f x = let g y = ?foo in g I realize that I have no idea what f's type should be. Is it (?foo :: c) => a -> b -> c or is it a -> ((?foo :: c) => b -> c) ? As far as I can tell, these are not the same type: you can distinguish between them by partially applying f with various different values of ?foo in the implicit environment. GHC tells me that f has the former type, but I still have no idea why: is it because g has an implicit ?foo parameter and f implicitly applies its own ?foo to g before returning it? Why would it do that? Or is it because ?foo is here interpreted as referring to an implicit parameter bound in the call of f, instead of in g? That doesn't make sense either. The final straw was: Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g 1 Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g () 2 This is insanity. I can't possibly use a language feature which behaves in such a non-orthogonal way. Now the interesting part: I think I've managed to fix these problems. I'm afraid that my solution will turn out to be just as unimplementable as my original file I/O proposal, and that's very likely in this case since I'm far from grokking Haskell's type system. So I'm going to present my idea and let the gurus on this list tell me where I went wrong. Here we go. First, discard the current implicit-parameter scheme entirely. (I'll eventually build up to something very similar.) Now introduce the idea of "explicit named parameters" to Haskell. This requires three extensions: a new kind of abstraction, a new kind of application, and a way of representing the resulting types. The abstraction could be done with a new lambda form, but instead I'll use a special prefix on identifiers which are to be considered named parameters, namely the character #. The new application form will be [F] { #x = [G] } where [F] and [G] are expressions. [F] must evaluate to a function with an explicit named parameter #x. The type notation for a named parameter will be (#name :: type). They can appear only on the left side of a ->. Named parameters can only be passed by name, so their order relative to positional parameters and each other doesn't matter; therefore we may as well "bubble them up" to the head of the list of arguments. In fact, we could put them in the context with the type classes, but I won't do so. Examples: cons :: (#elem :: a) -> (#list :: [a]) -> [a] cons #elem #list = #elem : #list cons { #elem = 'h', #list = "ello" } -- legal cons 'h' "ello" -- illegal: named params must be passed by name cons { #list = "ello" } -- legal, has type (#elem :: Char) -> String cons { #list = "ello", #elem = 'h' } -- legal cons { #list = "ello" } { #elem = 'h' } -- legal append :: (#right :: [a]) -> [a] -> [a] append left #right = ... -- named args gravitate left Now introduce the idea of "auto-lifted named parameters". I'll distinguish these from ordinary named parameters by using an @ prefix instead of #. These are exactly the same as ordinary named parameters except that if they appear in the type on the right hand side of an application node, they are implicitly lifted to the whole node. For example, if [F] has an auto-lifted parameter @p, and [G] has auto-lifted parameters @p and @q, then [F][G] is implicitly converted to something like \@p @q -> [F] { @p = @p } ( [G] { @p = @p, @q = @q } ). Finally, introduce the following syntax: * As an expression, ?x is short for \@x -> @x. * On the left hand side of the = sign in a named application, ?x is the same as @x. * For backward compatibility, "let ?x = [E] in [F]" should be treated as equivalent to "[F] { ?x = [E] }". Now we have something almost the same as the current implicit-parameter system, except that it behaves in a much safer and saner way. For example, looking at the confusing expressions from the beginning again: f x = let g y = ?foo in g This obviously has type (?foo :: c) -> a -> b -> c. It doesn't matter where the ?foo parameter appears in the type because it will always be referred to explicitly, by name, exactly once in each call of f. let ?x = 1 in let g = ?x in let ?x = 2 in g This reduces as follows: let ?x = 1 in let g = ?x in let ?x = 2 in g ( let g = \@x -> @x in g { @x = 2 } ) { @x = 1 } (\@x -> @x) { @x = 2 } { @x = 1 } 2 { @x = 1 } At this point we get a type error, as we should: a let binding of an implicit parameter that's never used is almost certainly a coding error. let ?x = 1 in let g () = ?x in let ?x = 2 in g () Reduces in exactly the same way as the previous case, with the same result. Again, this is as is should be. Why are the semantics so much clearer? I think the fundamental problem with the existing semantics is the presence of an implicit parameter environment, from which values are scooped and plugged into functions at hard-to-predict times. By substituting a notation which clearly means "I want this implicit parameter of this function bound to this value right now, and if you can't do it I want a static type error", we avoid this ambiguity. More thoughts, assuming this all pans out (knocking on wood): * Explicit named parameters seem like a useful idea too. Maybe they should be added to Haskell. * We should really, really drop the "let ?x" form and switch to the record-update notation. In "( let g = ?x in g { ?x = 2 } ) { ?x = 1 }" it's obvious what's going to happen and what the result will be, but in "let ?x = 1 in let g = ?x in let ?x = 2 in g" it's very unclear, even though, under the translation above, these two forms are equivalent. * I think it may be possible to extend this to provide default values for named parameters, which would be really really cool (no more separate foo and fooBy functions). -- Ben
On Sat, 2 Aug 2003 00:45:07 -0700 (PDT) Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
When I first learned about implicit parameters I thought they were a great idea. The honeymoon ended about the time I wrote some code of the form"let ?foo = 123 in expr2", where expr2 used ?foo implicitly, and debugging eventually unearthed the fact that ?foo's implicit value was not being set to 123 in expr2. That was enough to scare me off of using implicit parameters permanently.
More recently, I've realized that I really don't understand implicit parameters at all. They seemed simple enough at first, but when I look at an expression like
f x = let g y = ?foo in g
I realize that I have no idea what f's type should be. Is it
(?foo :: c) => a -> b -> c
or is it
a -> ((?foo :: c) => b -> c)
Do you have problems finding the type of f x = let g y = 4 in g ? it works -EXACTLY- the same way.
? As far as I can tell, these are not the same type: you can distinguish between them by partially applying f with various different values of ?foo in the implicit environment.
If you do apply f you get (?foo :: c) => b -> c. GHC tells me
that f has the former type, but I still have no idea why: is it because g has an implicit ?foo parameter and f implicitly applies its own ?foo to g before returning it? Why would it do that? Or is it because ?foo is here interpreted as referring to an implicit parameter bound in the call of f, instead of in g? That doesn't make sense either.
The constraint should just be thought of as an extra "explicit" parameter, or think of it as using the same mechanism dictionary passing for type classes uses. Implicit parameters aren't as "flexible" as full dynamic scoping would be. For example, f g = let ?foo = 5 in g () g x = ?foo f g :: {foo :: a) => a NOT f g :: Num a => a i.e. it doesn't evaluate to 5. So you can't bind the free implicit variables of a passed in HOF (basically you can't have type ({?foo :: t => a -> t) -> b), and similarly you can't return HOF's with free implicit parameters (no type a -> ({?foo :: t => t -> b)) If I'm not way rusty with CL, here are similar examples with full dynamic scoping,
(defvar *x* 0) *X* (defun f (g) (let ((*x* 5)) (funcall g))) F (defun g () *x*) G (f #'g) 5 (defun f (x) (defun g (y) *x*)) F (let ((*x* 1)) (f 'a)) G (funcall * 'b) 0 (let ((*x* 2)) (funcall ** 'b)) 2
The final straw was:
Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g 1 Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g () 2
This is insanity. I can't possibly use a language feature which behaves in such a non-orthogonal way.
Compare, let g = (<) in (g 'a' 'b',g 1 2) let g x y = x < y in (g 'a' 'b',g 1 2) the problem with this is again -EXACTLY- the same because implicit parameters behave very much like class constraints, because class constraints pretty much ARE implicit parameters. The problem here is the monomorphism restriction. This applies to implicit parameters as well for the same reasons (and because implicit parameters are very likely handled by the same code.) In fact, if you use -fno-monomorphism-restriction, your examples above give you the same numbers. ___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | GHC Interactive, version 5.04.3 / /_\\/ __ / /___| | http://www.haskell.org/ghc/ \____/\/ /_/\____/|_| Type :? for help. Loading package base ... linking ... done. Loading package haskell98 ... linking ... done. Prelude> :set -fglasgow-exts Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g 1 Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g () 2 Prelude> :set -fno-monomorphism-restriction Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g 2 Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g () 2 Whether your additions would be worthwhile anyways, I haven't really thought about.
On Sat, 2 Aug 2003, Derek Elkins wrote:
Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
More recently, I've realized that I really don't understand implicit parameters at all. They seemed simple enough at first, but when I look at an expression like
f x = let g y = ?foo in g
I realize that I have no idea what f's type should be.
Do you have problems finding the type of
f x = let g y = 4 in g ? it works -EXACTLY- the same way.
No, there is a big difference: There's just one dictionary value for each type class instance, and it's global to the whole application. As a result, it doesn't matter when hidden dictionary arguments are applied. But implicit parameters are scoped, so it matters a lot when they're applied. This opens up a big can of worms that the type-context system has never had to deal with before.
Implicit parameters aren't as "flexible" as full dynamic scoping would be. For example,
f g = let ?foo = 5 in g () g x = ?foo
f g :: {foo :: a) => a NOT f g :: Num a => a i.e. it doesn't evaluate to 5.
But it should. Or rather, either it should evaluate to 5 or it should be a compile-time error, because the programmer clearly thought that g within the body of f had a implicit parameter ?foo when in fact it didn't. In my proposal this is a type error; the message would be something like "g () does not have an implicit parameter ?foo, in the expression 'let ?foo = 5 in g ()'". It would be easy to add a helpful message to the effect that function arguments can't have implicit parameters (which is still true in my proposal).
The final straw was:
Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g 1 Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g () 2
Compare,
let g = (<) in (g 'a' 'b',g 1 2)
let g x y = x < y in (g 'a' 'b',g 1 2)
One of your expressions behaves as expected, the other is a type error. I'm happy with both of these outcomes. But my expressions both typecheck, but then do different things. That's scary. I was burned by this once, and now when I try to write code with implicit parameters I have to think to myself constantly, "is this going to do what I expect? Is this going to do what I expect?". The big selling point of functional programming is that it makes programs easy to reason about, but implicit parameters (as presently implemented) violate this principle to an extent that I've never seen in any other language except Perl.
In fact, if you use -fno-monomorphism-restriction, your examples above give you the same numbers.
I should point out that this is the only case in which the presence or absence of the monomorphism restriction changes the meaning of a correct program. In other words, it's not a restriction at all here, but an interpretation. I hope that worries you at least a little bit. My proposal does not behave that way: at worst, turning on the monomorphism restriction creates an error where there was none before, just as in the case of type class constraints. -- Ben
On Sun, 3 Aug 2003 08:01:52 -0700 (PDT) Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
On Sat, 2 Aug 2003, Derek Elkins wrote:
Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
More recently, I've realized that I really don't understand implicit parameters at all. They seemed simple enough at first, but when I look at an expression like
f x = let g y = ?foo in g
I realize that I have no idea what f's type should be.
Do you have problems finding the type of
f x = let g y = 4 in g ? it works -EXACTLY- the same way.
No, there is a big difference: There's just one dictionary value for each type class instance, and it's global to the whole application. As a result, it doesn't matter when hidden dictionary arguments are applied. But implicit parameters are scoped, so it matters a lot when they're applied. This opens up a big can of worms that the type-context system has never had to deal with before.
I wasn't talking about the semantics, I was talking about the type-inference. The "Implicit Parameters: dynamic scoping and static typing" makes a point at least twice that the interpretation of code using implicit parameters is dependent on the type not just the syntax.
Implicit parameters aren't as "flexible" as full dynamic scoping would be. For example,
f g = let ?foo = 5 in g () g x = ?foo
f g :: {foo :: a) => a NOT f g :: Num a => a i.e. it doesn't evaluate to 5.
But it should. Or rather, either it should evaluate to 5 or it should be a compile-time error, because the programmer clearly thought that g within the body of f had a implicit parameter ?foo when in fact it didn't.
How does g not have an implicit parameter. It could not but that's not the issue here. The issue is the programmer thought that the binding to ?foo would influence g. Here the type would make it obvious that it shouldn't. Whether you want this ability or not in this or the other example is debatable.
In my proposal this is a type error; the message would be something like"g () does not have an implicit parameter ?foo, in the expression 'let?foo = 5 in g ()'". It would be easy to add a helpful message to the effect that function arguments can't have implicit parameters (which is still true in my proposal).
Would let ?foo = 4 = id be an error then? or let ?foo = 4 in 4? There is no reason to require the body to use an implicit parameter.
The final straw was:
Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g 1 Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g () 2
Compare,
let g = (<) in (g 'a' 'b',g 1 2)
let g x y = x < y in (g 'a' 'b',g 1 2)
One of your expressions behaves as expected, the other is a type error. I'm happy with both of these outcomes. But my expressions both typecheck, but then do different things. That's scary. I was burned by this once, and now when I try to write code with implicit parameters I have to think to myself constantly, "is this going to do what I expect? Is this going to do what I expect?".
Indeed, this is pretty bad, but except for the monomorphism restriction issue, the behavior doesn't seem any less comprehensible than dynamic scoping ever is. However, what to expect is pretty obvious when looking at the type(at least as far as dynamic scoping is obvious.) The documentation should mention this behavior or implicit parameters should not suffer the monomorphism restriction and the documentation should warn against the potential lack of sharing.
The big selling point of functional programming is that it makes programs easy to reason about, but implicit parameters (as presently implemented) violate this principle to an extent that I've never seen in any other language except Perl.
Implicit parameters are meant to implement dynamic scoping. Dynamic scoping does typically make programs more difficult to reason about. I can only think of a few cases where implicit parameters might be a good idea. Perhaps I should see what Ashley Yakeley is doing with them as I virtually never use them. I typically use a Reader monad whenever I want behavior like this.
In fact, if you use -fno-monomorphism-restriction, your examples above give you the same numbers.
I should point out that this is the only case in which the presence or absence of the monomorphism restriction changes the meaning of a correct program. In other words, it's not a restriction at all here, but an interpretation. I hope that worries you at least a little bit.
I think, the authors of the implicit parameters paper were in favor of not having the monomorphism restriction here. I'm surprised this isn't documented in the GHC User-guide (an example would also be nice.) I would prefer that the behavior was independent of -fno-monomorphism-restriction, either through (yet another) flag, or by fixing one choice or the other. I'd prefer a flag, but if it were fixed, I'd be in favor of the -fno-monomorphism-restriction interpretation.
In article <Pine.LNX.4.21.0308020030420.6841-100000@dark.darkweb.com>, Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
The final straw was:
Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g 1 Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g () 2
This is insanity. I can't possibly use a language feature which behaves in such a non-orthogonal way.
It's a type inference problem: Prelude> let ?x = 1 in let {g :: Int;g = ?x;} in let ?x = 2 in g 1 Prelude> let ?x = 1 in let {g :: (?x :: Int) => Int;g = ?x;} in let ?x = 2 in g 2 Prelude> let ?x = 1 in let {g :: () -> Int;g () = ?x;} in let ?x = 2 in g () 1 Prelude> let ?x = 1 in let {g :: (?x :: Int) => () -> Int;g () = ?x;} in let ?x = 2 in g () 2 The type of g is ambiguous, and GHC arbitrarily goes with different options in the two different cases. Ideally, GHC would complain about the ambiguity. IIRC with -fglasgow-exts turned on there are other cases when GHC infers the "wrong" type if you don't specify it. This is because with higher-order types, there isn't necessarily an inferable "most general" type for some expressions. But implicit parameters work very well if you have the type of everything specified. I use them extensively in HScheme without trouble. -- Ashley Yakeley, Seattle WA
In article <Pine.LNX.4.21.0308020030420.6841-100000@dark.darkweb.com>, Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
Now we have something almost the same as the current implicit-parameter system, except that it behaves in a much safer and saner way.
Hmm... you have this: [?x,?x] {@x=1} -- OK [?x] {@x=1} -- OK [] {@x=1} -- not OK You've disallowed the last one in an attempt to prevent ambiguity. However, not only is this ugly, it isn't sufficient. Consider this: let ?x = 1 in ((let g = \_ _ -> ?x in let ?x = 2 in g ?x) ?x) converts to: ((let g = \_ _ -> \@x -> @x in ((g (\@x -> @x)) {@x = 2})) (\@x -> @x)){@x = 1} 1. do @-application first ((let g = \_ _ -> \@x -> @x in (g 2)) (\@x -> @x)){@x = 1} (((\_ _ -> \@x -> @x) 2) (\@x -> @x)){@x = 1} ((\_ -> \@x -> @x) (\@x -> @x)){@x = 1} (\@x -> @x){@x = 1} 1 2. do let-substitution first ((((\_ _ -> \@x -> @x) (\@x -> @x)) {@x = 2}) (\@x -> @x)){@x = 1} (((\_ -> \@x -> @x) {@x = 2}) (\@x -> @x)){@x = 1} ((\_ -> 2) (\@x -> @x)){@x = 1} (\_ -> 2) 1 2 Again, it all depends on the type of 'g'. -- Ashley Yakeley, Seattle WA
First of all, thanks for reading my proposal, and I apologize for the ill-considered rant which preceded it. I hope you won't hold it against me -- we should all be on the same side here. On Sun, 3 Aug 2003, Ashley Yakeley wrote:
((let g = \_ _ -> \@x -> @x in ((g (\@x -> @x)) {@x = 2})) (\@x -> @x)){@x = 1} ((let g = \_ _ -> \@x -> @x in (g 2)) (\@x -> @x)){@x = 1}
This reduction is incorrect. Auto-lifted parameters on the RHS of an application get lifted out, so g (\@x -> @x) => (\@x -> g { @x = @x } @x) Therefore g (\@x -> @x) { @x = 2 } => (\@x -> g { @x = @x } @x) { @x = 2 } => g { @x = 2 } 2, not (g 2) as you wrote. Several of the other steps in your reductions are incorrect for the same reason. I think the following is a correct reduction, although it's easy to get them wrong when you do them by hand: let ?x = 1 in ((let g = \_ _ -> ?x in let ?x = 2 in g ?x) ?x) => ((let g = \_ _ -> ?x in g ?x {?x=2} ) ?x) {?x=1} => ((let g = \_ _ @x -> @x in g (\@x -> @x) {@x=2} ) (\@x -> @x)) {@x=1} => (\_ _ @x -> @x) (\@x -> @x) {@x=2} (\@x -> @x) {@x=1} => (\@x -> (\_ _ @x -> @x) { @x = @x } @x) {@x=2} (\@x -> @x) {@x=1} => (\_ _ @x -> @x) {@x=2} 2 (\@x -> @x) {@x=1} => (\_ _ -> 2) 2 (\@x -> @x) {@x=1} => (\_ -> 2) (\@x -> @x) {@x=1} => (\@x -> (\_ -> 2) @x) {@x=1} => (\_ -> 2) 1 => 2 This is the answer I expected intuitively. If you can produce a correct reduction which yields anything else, then I'll concede defeat. (For now.)
[?x,?x] {@x=1} -- OK [?x] {@x=1} -- OK [] {@x=1} -- not OK
Interesting. Can you give an example of this problem cropping up in a more realistic context? Certainly no one will write "[] {@x=1}", since either it's an error or it's exactly equivalent to "[]". My intuition is that this is a minor problem which would bite very rarely in practice, like "show []". And, let me emphasize again, it's safe: programs will not silently behave in an unexpected way because of this. By the way, I respectfully disagree that requiring explicit ?x bindings to be used is ugly. It's an ugly additional rule in the current framework, which treats implicit parameters as a way of simulating a Lisp-like dynamic environment, but it's the natural state of affairs in my proposal, which treats implicit parameters as parameters. In my proposal it's ugly /not/ to require explicit ?x bindings to be used -- it would be like defining (f x) to be f when f is not a function. -- Ben
I just noticed something interesting. Consider f #name = g where g #name = "hello" This apparently has type (#name :: a) -> (#name :: b) -> String. Should the two #names be merged? Clearly not, because ordinary positional parameters never get merged, and named parameters are supposed to be the same except that they're referred to by name. Then the following should be legal: f { #name = 1 } { #name = 2 } So when named parameters have different names their relative order doesn't matter, but when they have the same name it certainly does! But this is actually a simplification, not a complication, because it means that the distinction between positional and named parameters is a chimera. Positional parameters behave just like named parameters having a special out-of-band name, so ordinary abstraction and application can be treated as sugar for named abstraction and application. That's not quite the whole story, though: f #name #name = #name Is this (#name :: a) -> (#name :: b) -> a, or (#name :: a) -> (#name :: b) -> b, or an error? This problem crops up because my notation for abstracting named parameters involves punning (which I hadn't noticed before): It uses the same identifier in the interface and the implementation. The proper notation would be something like this: f { #name = x } { #name = y } = y On the other hand, auto-lifted parameters with the same name clearly should be merged. This is another way in which they differ from ordinary named parameters, and suggests that they should indeed go in the (unordered) type context, while ordinary named parameters clearly shouldn't. I don't think this is actually a problem with my proposal, but it worries me a bit because it suggests that the semantics of named parameters aren't quite as obvious as I previously thought. -- Ben
I kinda think someone mentioned this, perhaps even you. Or maybe I'm thinking of something else. As I'm feeling too lazy to check the archives, at the risk of saying something stupid or repeating something said, you may want to look at named instances (google should turn something up with a little effort.) It seems to cover some of the same issues/ideas you are having now, though in a different context.
On Sun, 3 Aug 2003, Derek Elkins wrote:
I kinda think someone mentioned this, perhaps even you. Or maybe I'm thinking of something else. As I'm feeling too lazy to check the archives, at the risk of saying something stupid or repeating something said, you may want to look at named instances (google should turn something up with a little effort.) It seems to cover some of the same issues/ideas you are having now, though in a different context.
I found a paper on named instances at http://www.cs.uu.nl/people/ralf/hw2001/4.html Thanks for pointing me to this; it's very interesting. As part of my proposal I was thinking about the possibility of decoupling the typeclass system from implicitness, but there were enough complications that I gave up. But this paper makes it look doable. Given plus :: (Num a) => a -> a -> a, the application plus (1::Int) currently has type Int -> Int. But it could equally well have type (Num Int) => Int -> Int. This type has the advantage of being more versatile: in principle you can supply your own type class. The problem is that usually you want Int -> Int, and it would be terribly cumbersome to have to apply the default Num Int dictionary by hand every time. That's as far as I got. But the paper points out that implicit context reduction in this case is perfectly safe and predictable as long as there's a global default value for the dictionary. Two implicit reductions can't conflict because the value passed implicitly is always the same, and an implicit reduction can't conflict with an explicit one because the explicit reduction changes the type, making the implicit reduction illegal. The paper suggests the notation f # MyInstance, but of course I think it should be something like f { Num Int = MyInstance } or f { MyInstance }. This notation is uglier, but it's more consistent and it avoids stealing a nice short infix operator which people have proposed to use for many other things. This works for named parameters too (explicit and implicit). You could write something like default #name = value or even just #name = value since this introduces no ambiguity if named parameters never clash with ordinary variable identifiers. Then implicit reduction is perfectly safe (in the sense that the behavior is unaffected by type signatures). This is better than the parameter-defaulting scheme I was thinking of. There are some complications, but I think they all have solutions: 1. The default value for #name has to be global to the whole application, so functions in other modules with a named parameter #name will have to use your default. Solution: make parameter names part of the module namespace. 2. You can't have named parameters with the same name but different types, if there's a global default. Solution: Invent a new notation for explicitly typing the defaults (not sure this is possible), or just live with the limitation. Haskell doesn't have Java-style overloading. 3. Problems arise in the case of duplicate dictionary types. Consider f x y = (x+1,y+1) with type (Num a, Num b) => a -> b -> (a,b). Then g = f (1::Int) (2::Int) has type (Num Int, Num Int) => (Int,Int). In the expression g { Num Int = ... }, which typeclass parameter are we applying? The solution, as pointed out in the paper, is to make the typeclass parameters explicit in the definition of f. Then f has type Num a => Num b => ... and g has type Num Int => Num Int => (Int,Int), and the order of application is unambiguous. There are additional subtleties described in the paper which I don't understand yet. -- Ben
Trouble for implicit parameter defaults: consider ?foo = 0 let x = ?foo in (x + ?foo) { ?foo = 1 } This evaluates to 1 when the monomorphism restriction is turned on, and 2 when it's off. This is no worse than the current behavior of implicit parameters even without defaults, but I still think that it should be forbidden because it's very important that the monomorphism restriction be a restriction only. This doesn't apply to defaults for explicit named parameters, but they have their own problems: consider #foo = 1 f :: (#foo :: a) => a f #foo = g g #foo = #foo main = print ( f { #foo = 2 } :: Int ) This prints 2 if the type signature for f is included, and 1 if it's omitted. I think this can be solved by forbidding any name with a default from appearing more than once in any function type. Also, reading "Type classes: exploring the design space" (http://research.microsoft.com/users/simonpj/Papers/type-class-design-space/) has given me serious doubts about explicit dictionary passing. It seems as though it would make program behavior too dependent on otherwise minor changes to the type inference rules. Even without explicit dictionary passing I think you would still be able to write sort :: (#comparator :: a -> a -> Ordering) => [a] -> [a] #comparator = compare -- Ben
Ben Rudiak-Gould wrote:
[...] The final straw was:
Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g 1 Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g () 2
This is insanity. I can't possibly use a language feature which behaves in such a non-orthogonal way.
Well, this is not insanity (only a little bit). In the first example, you define a *value* g, i.e., g is bound to the value of ?x in its current environment (though this value is not yet evaluated due to lazy evaluation), whereas in the second example you define a function. The real insanity in this point is that Haskell -- in contrast to Clean -- offers no way to distinguish function bindings and value bindings and therefore you cannot define nullary functions (except by some judicious use type signatures), which is the heart of the monomorphism restriction mentioned by somebody else on this list (and discussed regularly on this list :-).
Now the interesting part: I think I've managed to fix these problems. I'm afraid that my solution will turn out to be just as unimplementable as my original file I/O proposal, and that's very likely in this case since I'm far from grokking Haskell's type system. So I'm going to present my idea and let the gurus on this list tell me where I went wrong. Here we go.
[...]
Now introduce the idea of "explicit named parameters" to Haskell. This requires three extensions: a new kind of abstraction, a new kind of application, and a way of representing the resulting types.
This looks quite similar to the labeled parameters in Objective Caml. However, Objective Caml's solution seems to be more general. For instance, you can pass labeled parameters in arbitrary order and you can have default value for optional arguments.
[...]
Why are the semantics so much clearer? I think the fundamental problem with the existing semantics is the presence of an implicit parameter environment, from which values are scooped and plugged into functions at hard-to-predict times.
If you keep the distinction between values and functions in mind, I do not think that it is hard to predict when an implicit parameter is substituted (if you are willing to accept the principal problem that it is hard to predict which value is substituted with every kind of dynamic scoping :-).
By substituting a notation which clearly means "I want this implicit parameter of this function bound to this value right now, and if you can't do it I want a static type error", we avoid this ambiguity.
IMHO, this problem were solved much easier by introducing a new syntax to distinguish value and (nullary) function bindings, as was already repeatedly asked for on this list in the context of the monomorphism restriction. Personally, I'd suggest to use let x <- e in ... to introduce a value binding (as it is quite similar to the bindings introduced in a do-statement) and use let x = e to introduce a nullary function. (I prefer <- over := which John Hughes and others suggested some time ago because we don't loose an operator name). Thus, you example let ?x = 1 in let g = ?x in let ?x = 2 in g will behave as you did expect, viz. evaluate to 2, whereas let ?x = 1 in let g <- ?x in let ?x = 2 in g will return 1. Regards Wolfgang
I just figured out why the monomorphism restriction interacts so weirdly with implicit parameters, and how to fix it. We all know that when the monomorphism restriction is turned on, the following doesn't work: let f = (<) in (f 1 2, f 'a' 'b') On the other hand, the following does work: let f = (<) in (f 'a' 'b', f 'a' 'b') Why does it work? The answer to this is non-trivial: the compiler must inspect every use of f in the body of the let statement and try to statically deduce what dictionary will be passed in each case. If the deduction succeeds in all cases and the dictionary is the same in all cases, then the compiler can safely pre-apply that dictionary, reducing f to a monotype, without changing the semantics of the program. Otherwise, it can't safely do so, and must abort with an error message. In short, a let value binding of an expression with type-class constraints is valid precisely if the compiler can reduce it to a monotype without changing the semantics of the program. Exactly the same rule should apply to implicit parameters. In the case of implicit parameters, safety is ensured if in every use of the bound variable, its implicit parameter refers to the same explicit binding of that parameter. For example, the expression let g = ?x in (g,g) should be accepted provided there is an enclosing binding of ?x, because in both uses of g the implicit parameter ?x refers to that same binding. On the other hand, an expression like let g = ?x in (g, let ?x = 1 in g) must be rejected, since it necessarily involves two calls to g. A much more important example is this: let ?x = 1 in (let g = ?x in (let ?x = 2 in g)) Here g is used just once, so it can be reduced safely. The value that should be used for the reduction is the value that is in scope where g is used (that is, 2), because that is the only way to preserve the semantics of the program. For some reason, the current implementations use ?x = 1 for the early reduction, even though this alters the semantics of the program. In fact, ?x = 1 is not even in scope at the early reduction point, since by the axiomatic semantics in the Lewis et al. paper, let ?x = 1 in (let g = ?x in (let ?x = 2 in g)) is equivalent to let g = ?x in (let ?x = 1 in (let ?x = 2 in g)) (see section 3.1, bottom left corner of the page). All implementations should be changed so that they do the right thing. There are some complications which I'll discuss in a followup message. -- Ben
Complications: * In my examples it's easy to tell whether all uses of the implicit parameter refer to the same explicit binding, but it may be difficult when recursion is involved. This problem has already arisen in the case of type class constraints, and has been solved, so I'm confident it can be solved for implicit parameters too. Unfortunately, the two cases are not quite the same: f :: (Num a) => a -> b f x = f (x+1) g :: (?x :: Int) -> b g = g {?x = ?x+1} Here all calls of f use the same implicit argument, but calls of g use different ones. * It might be harder to pre-apply the implicit value if it's not in scope at the early application point, as in: let g = ?x in ([deeply nested expr...] let ?x = [...] in g) But referential transparency means that it can always be done; it's just tricky. * It's not really necessary for safety that all uses of the implicit parameter refer to the same explicit binding; they just need to refer to the same value. So this could be accepted: let ?x = 1 in (let g = ?x in (g, let ?x = 1 in g)) even though it would be rejected if one of the 1s were changed to something else. Cases like this would be rare, though, and it's not clear that programs of this type should really be accepted anyway, since the safety is rather fragile. None of these complications threatens the overall validity of the monomorphism restriction, because the algorithm on which the monomorphism restriction is based is heuristic anyway: the only requirement is that when it says a reduction is safe, it mustn't be wrong. If the complicated cases end up being too complicated, it's perfectly acceptable to give up and say they're unsafe. This one is a slightly different story: * Pre-application might introduce space leaks. My intuition says to ignore this issue, because (1) let-abstraction always has the potential of introducing space leaks, and (2) Even if you explicitly write something like "length [1..1000000] + length (tail [1..1000000])" the compiler is allowed to combine the two lists without telling you, even though this introduces a space leak. -- Ben
I wrote:
Exactly the same rule should apply to implicit parameters. In the case of implicit parameters, safety is ensured if in every use of the bound variable, its implicit parameter refers to the same explicit binding of that parameter. For example, the expression
let g = ?x in (g,g)
should be accepted provided there is an enclosing binding of ?x, because in both uses of g the implicit parameter ?x refers to that same binding.
I think what I wrote above is misleading. The "explicit" or "enclosing" binding need not be local, or even in a known location, as long as the compiler can prove that there's only one of them. And this is always possible in the case of non-local bindings. E.g.: f () = let g = ?x in (g,g) Each time f is invoked it will be passed exactly one implicit ?x. The compiler has no idea where that value was explicitly bound, but it can still prove that the two uses of g always refer to the same ?x. -- Ben
participants (4)
-
Ashley Yakeley -
Ben Rudiak-Gould -
Derek Elkins -
Wolfgang Lux