### Re: The madness of implicit parameters: cured?

At 2003-08-04 22:33, Ben Rudiak-Gould wrote: This illustrates what you pointed out earlier, that the program's semantics can be changed by adding explicit type signatures which include implicitly-parameterized parameters. But wasn't avoiding this a design goal of your proposal? If it is valid, then this must be a valid reduction: ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} Not unless you give an explicit type signature, no. So effectively your proposal is the same as the existing implicit parameter mechanism, except that the compiler is a bit stricter in certain cases where the types are ambiguous? -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

On Mon, 4 Aug 2003, Ashley Yakeley wrote: ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} ^^^ (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} This reduction is incorrect. The underlined parameter needs to be lifted out, so (\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x) becomes [EMAIL PROTECTED] - ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) @x) If we next apply (\a - ...) to @x, something interesting happens: we have to rename to avoid variable capture. I didn't realize this was ever necessary with implicit parameters. The renaming is impossible with my punning notation, so I'll have to write this out again with separate interface and implementation names (yuck): [EMAIL PROTECTED] - ((\a - ((a,[EMAIL PROTECTED] - t) [EMAIL PROTECTED] = 2})) s) Now names of the form @x only appear on the left hand side of {...=...} forms, as they should, and I chose different internal names for lexically distinct bindings. Further reduction should yield the expected answer. The key point is that /everything/ in my proposal is lexically scoped. That's why everything works as expected. The current system uses quasi-dynamic scoping, which is why things work pretty much as expected most of the time but not always. Whenever you're in doubt about the correct way to do a reduction in my system, do whatever preserves hygiene. And the rules for lifting implicit parameters are isomorphic to the type-inference rules for the implicit parameter context, so if you're ever in doubt about which parameters to lift, figure out how the type is inferred. A simpler query: what types can f have here? Which if any should the compiler infer? f a b = (a,b) [EMAIL PROTECTED] = 2} Yow. The compiler certainly won't infer anything for this, but if we allow explicit typings we get stuff like f1 :: (Num a, Num b) = a - ((?x :: b) = b) - (a,b) f1 a b = (a,b) [EMAIL PROTECTED] = 2} f2 :: (Num a, Num b) = ((?x :: a) = a) - b - (a,b) f2 a b = (a,b) [EMAIL PROTECTED] = 2} f1 ?x ?x [EMAIL PROTECTED] = 1} == (1,2) f2 ?x ?x [EMAIL PROTECTED] = 1} == (2,1) This issue never occurred to me. I'd like to just ban these types, but they look potentially useful, and in fact I see that you use them in HScheme. I think it's up to the community to decide this one. It's sad to lose the nice property of independence of type, but my proposal is still a lot better than what we've got. Note that we also have: f0 :: (Num a, Num b) = a - b - (a,b) f0 a b = (a,b) [EMAIL PROTECTED] = 2} == type error: (a,b) has no parameter @x f3 :: (Num a, Num b) = ((?x :: a) = a) - ((?x :: b) = b) - (a,b) f3 a b = (a,b) [EMAIL PROTECTED] = 2} f3 ?x ?x [EMAIL PROTECTED] = 1} == type error: (f3 ?x ?x) has no param. @x And given that type, which of these are valid? f ?x ?x f ?x 1 f 1 ?x f 1 1 I don't think there's any way to forbid any of these while also allowing types like those of f1 and f2 above. In fact, I don't think you can forbid them without also forbidding fromJust' :: (?default :: a) = Maybe a - a fromJust' (Just x) = x fromJust' Nothing = ?default I see what you're driving at, though: can/should I forbid the compiler from inferring a type for (a,b) [EMAIL PROTECTED] = 2} under these circumstances? I think the answer is yes, but I'm not sure. Can anyone weigh in who's actually implemented a type inferencer for Haskell? -- Ben ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

On Mon, 4 Aug 2003, Ashley Yakeley wrote: At 2003-08-04 18:19, Ben Rudiak-Gould wrote: ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} ^^^ (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} This reduction is incorrect. It's a simple beta-reduction, it must be correct. This is a different lambda calculus, with a different beta rule. You can see the same effect in the type inference rules for implicit parameters: If f has type Int - String and ?x has type (?x :: Int) = Int, then f ?x has type (?x :: Int) = String, i.e. the implicit ?x parameter is lifted out of the RHS to become a parameter of the whole application node. This rule is what makes implicit parameters implicit. As you pointed out, this reduction behavior depends on f's type, so this is necessarily a typed lambda calculus. But that's okay because Haskell is statically typed. -- Ben ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

On Mon, 4 Aug 2003, Ashley Yakeley wrote: At 2003-08-04 20:00, Ben Rudiak-Gould wrote: This is a different lambda calculus, with a different beta rule. You can see the same effect in the type inference rules for implicit parameters: If f has type Int - String and ?x has type (?x :: Int) = Int, then f ?x has type (?x :: Int) = String, i.e. the implicit ?x parameter is lifted out of the RHS to become a parameter of the whole application node. This rule is what makes implicit parameters implicit. Ah. Actually I think the beta rule is unchanged with Haskell's implicit parameters. Consider: x :: (?x :: Int) = Int f :: Int - String f :: ((?x :: Int) = Int) - ((?x :: Int) = String) -- specialisation f x :: (?x :: Int) = String -- apply beta rule I think it amounts to the same thing. This is a nice way of looking at it, though. Either way, the effect is that implicit parameters don't disappear into function applications unless the function has been explicitly typed to take them; instead they grow to encompass larger and larger portions of the containing function, until eventually they become parameters of the whole function. Result: you don't have to put them there by hand. So is this valid or not? b :: (?x :: Int) = Int b = [EMAIL PROTECTED] - @x f :: ((?x :: Int) = Int) - (Int,Int) f = \a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) f b :: (Int,Int) f b = ((b,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) = (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) Yes, it is. This illustrates what you pointed out earlier, that the program's semantics can be changed by adding explicit type signatures which include implicitly-parameterized parameters. If it is valid, then this must be a valid reduction: ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} Not unless you give an explicit type signature, no. Without it the compiler will infer a different type for f which does not have any arguments with implicit parameters, because inferred types never do (see section 2.1 in the original paper). Without this assumption the compiler couldn't infer a principal type. (Specialization doesn't help here, because the set of valid specializations depends on f's internals, and can't be captured by a principal type.) -- Ben ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

At 2003-08-04 18:19, Ben Rudiak-Gould wrote: ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} ^^^ (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} This reduction is incorrect. It's a simple beta-reduction, it must be correct. b :: (?x :: Int) = Int b = [EMAIL PROTECTED] - @x f :: ((?x :: Int) = Int) - (Int,Int) f = \a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) f b :: (Int,Int) f b = ((b,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

On Mon, 4 Aug 2003, Ashley Yakeley wrote: At 2003-08-04 22:33, Ben Rudiak-Gould wrote: This illustrates what you pointed out earlier, that the program's semantics can be changed by adding explicit type signatures which include implicitly-parameterized parameters. But wasn't avoiding this a design goal of your proposal? Yes, and you convinced me that I had to give up on this goal. I'm attached to my ideas, but only as long as they're right. If it is valid, then this must be a valid reduction: ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} Not unless you give an explicit type signature, no. So effectively your proposal is the same as the existing implicit parameter mechanism, except that the compiler is a bit stricter in certain cases where the types are ambiguous? Yes, it's effectively the same; that was the point. I'm not trying to create a new language extension, but an improved conceptual foundation for the existing extension. It's fine if I don't end up with quite the design I expected, as long as it coheres. The important thing here is the *idea* of treating implicit parameters as a special kind of named parameter, rather than via a problematic analogy with Lisp dynamic typing. Everything else falls naturally (and, I hope, inevitably) out of that idea. This idea has been very successful so far. For one thing, I just found the solution to the monomorphism restriction problem that people have been struggling with for as long as implicit parameters have existed. The reason I found that answer is that my new treatment changes the design space in such a way that the solution falls out naturally with a little coaxing. More than anything else, this makes me think that I've hit on the right approach to implicit parameters. -- Ben ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

At 2003-08-03 14:09, Ben Rudiak-Gould wrote: This reduction is incorrect. Auto-lifted parameters on the RHS of an application get lifted out I am interpreting this as Auto-lifted parameters on the RHS of an application get lifted out before [EMAIL PROTECTED] 'beta'-reduction can be done. I think this is ambiguous: ((\a - ((a,?x) [EMAIL PROTECTED] = 2})) ?x,?x) [EMAIL PROTECTED] = 1} ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} 1. (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} (([EMAIL PROTECTED] - (@x,@x)) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} ((2,2),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} ([EMAIL PROTECTED] - ((2,2),@x)) [EMAIL PROTECTED] = 1} ((2,2),1) 2. ([EMAIL PROTECTED] - ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) @x,@x)) [EMAIL PROTECTED] = 1} ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) 1,1) (((1,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}),1) ((([EMAIL PROTECTED] - (1,@x)) [EMAIL PROTECTED] = 2}),1) ((1,2),1) A simpler query: what types can f have here? Which if any should the compiler infer? f a b = (a,b) [EMAIL PROTECTED] = 2} And given that type, which of these are valid? f ?x ?x f ?x 1 f 1 ?x f 1 1 -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

At 2003-08-04 18:19, Ben Rudiak-Gould wrote: [EMAIL PROTECTED] - ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) @x) If we next apply (\a - ...) to @x, something interesting happens: we have to rename to avoid variable capture. I don't see why, isn't this much the same as ordinary names? (\a - ((\a - a) 1,a)) 2 ((\a - a) 1,2) (1,2) -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

At 2003-08-04 20:00, Ben Rudiak-Gould wrote: This is a different lambda calculus, with a different beta rule. You can see the same effect in the type inference rules for implicit parameters: If f has type Int - String and ?x has type (?x :: Int) = Int, then f ?x has type (?x :: Int) = String, i.e. the implicit ?x parameter is lifted out of the RHS to become a parameter of the whole application node. This rule is what makes implicit parameters implicit. Ah. Actually I think the beta rule is unchanged with Haskell's implicit parameters. Consider: x :: (?x :: Int) = Int f :: Int - String f :: ((?x :: Int) = Int) - ((?x :: Int) = String) -- specialisation f x :: (?x :: Int) = String -- apply beta rule As you pointed out, this reduction behavior depends on f's type, so this is necessarily a typed lambda calculus. But that's okay because Haskell is statically typed. So is this valid or not? b :: (?x :: Int) = Int b = [EMAIL PROTECTED] - @x f :: ((?x :: Int) = Int) - (Int,Int) f = \a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) f b :: (Int,Int) f b = ((b,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) = (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) If it is valid, then this must be a valid reduction: ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1} -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

On Sat, 2 Aug 2003, Derek Elkins wrote: Ben Rudiak-Gould [EMAIL PROTECTED] 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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

In article [EMAIL PROTECTED], Ben Rudiak-Gould [EMAIL PROTECTED] 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] [EMAIL PROTECTED] -- OK [?x] [EMAIL PROTECTED] -- OK [] [EMAIL PROTECTED] -- 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 = \_ _ - [EMAIL PROTECTED] - @x in ((g ([EMAIL PROTECTED] - @x)) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} 1. do @-application first ((let g = \_ _ - [EMAIL PROTECTED] - @x in (g 2)) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} (((\_ _ - [EMAIL PROTECTED] - @x) 2) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} ((\_ - [EMAIL PROTECTED] - @x) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} ([EMAIL PROTECTED] - @x)[EMAIL PROTECTED] = 1} 1 2. do let-substitution first \_ _ - [EMAIL PROTECTED] - @x) ([EMAIL PROTECTED] - @x)) [EMAIL PROTECTED] = 2}) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} (((\_ - [EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} ((\_ - 2) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} (\_ - 2) 1 2 Again, it all depends on the type of 'g'. -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

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 = \_ _ - [EMAIL PROTECTED] - @x in ((g ([EMAIL PROTECTED] - @x)) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} ((let g = \_ _ - [EMAIL PROTECTED] - @x in (g 2)) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} This reduction is incorrect. Auto-lifted parameters on the RHS of an application get lifted out, so g ([EMAIL PROTECTED] - @x) = ([EMAIL PROTECTED] - g { @x = @x } @x) Therefore g ([EMAIL PROTECTED] - @x) { @x = 2 } = ([EMAIL PROTECTED] - 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 ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] ) ([EMAIL PROTECTED] - @x)) [EMAIL PROTECTED] = (\_ _ @x - @x) ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = ([EMAIL PROTECTED] - (\_ _ @x - @x) { @x = @x } @x) [EMAIL PROTECTED] ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = (\_ _ @x - @x) [EMAIL PROTECTED] 2 ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = (\_ _ - 2) 2 ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = (\_ - 2) ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = ([EMAIL PROTECTED] - (\_ - 2) @x) [EMAIL PROTECTED] = (\_ - 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] [EMAIL PROTECTED] -- OK [?x] [EMAIL PROTECTED] -- OK [] [EMAIL PROTECTED] -- not OK Interesting. Can you give an example of this problem cropping up in a more realistic context? Certainly no one will write [] [EMAIL PROTECTED], 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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

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. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

At 2003-08-03 14:09, Ben Rudiak-Gould wrote: ((let g = \_ _ - [EMAIL PROTECTED] - @x in ((g ([EMAIL PROTECTED] - @x)) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} ((let g = \_ _ - [EMAIL PROTECTED] - @x in (g 2)) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1} This reduction is incorrect. Auto-lifted parameters on the RHS of an application get lifted out, so g ([EMAIL PROTECTED] - @x) = ([EMAIL PROTECTED] - g { @x = @x } @x) Hmm... I assume you mean specifically this: g ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] - (g { @x = @x } @x) Supposing you have this: g = \_ - 3 then you have this reduction: g ?x g ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] - (g { @x = @x } @x) [EMAIL PROTECTED] - ((\_ - 3) { @x = @x } @x) error: can't apply (\_ - 3) { @x = @x } Something else I haven't mentioned is that you shouldn't use (-) as such in the type signatures. This is because (-) is an ordinary type-constructor. For instance, if you define this: type Func = (-) then all these are the same type: Func a b (-) a b a - b But in your scheme, (-) has been extended to allow certain pseudo-types in its first position. It might be better to use a different syntax rather than overload (-) with something that isn't a type-constructor. -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

On Sun, 3 Aug 2003, Ashley Yakeley wrote: At 2003-08-03 14:09, Ben Rudiak-Gould wrote: g ([EMAIL PROTECTED] - @x) = ([EMAIL PROTECTED] - g { @x = @x } @x) Hmm... I assume you mean specifically this: g ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] - (g { @x = @x } @x) Supposing you have this: g = \_ - 3 Yeah, the application rule is actually more complicated than that: it depends on knowing all the auto-lifted parameters of both the LHS and the RHS. The set of autolifted parameters of the application node is the union of these two sets, and each parameter is passed on only to the function(s) that need it. This means that in a dynamically-typed implementation, application is necessarily quite strict: both the LHS and the RHS need to be reduced to HNF, whereas normally you need only WHNF on the LHS and nothing on the RHS. However, I don't think this is a problem in Haskell, since all the necessary information can be derived statically from the type. Something else I haven't mentioned is that you shouldn't use (-) as such in the type signatures. This is because (-) is an ordinary type-constructor. Okay, good point. (=) seems like the obvious choice. I shall use it henceforth. -- Ben ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### Re: The madness of implicit parameters: cured?

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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell

### 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 [EMAIL PROTECTED] @q - [F] { @p = @p } ( [G] { @p = @p, @q = @q } ). Finally, introduce the following syntax: * As an expression, ?x is short for [EMAIL PROTECTED] - @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 = [EMAIL PROTECTED] - @x in g { @x = 2 } ) { @x = 1 }

### Re: The madness of implicit parameters: cured?

On Sat, 2 Aug 2003 00:45:07 -0700 (PDT) Ben Rudiak-Gould [EMAIL PROTECTED] 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 formlet ?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. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell