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?
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
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
