On Mon, 4 Aug 2003, Ashley Yakeley wrote:
((\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x),\@x -> @x) {@x = 1} ^^^ ((\@x -> @x,\@x -> @x) {@x = 2},\@x -> @x) {@x = 1}
This reduction is incorrect. The underlined parameter needs to be lifted out, so (\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x) becomes \@x -> ((\a -> ((a,\@x -> @x) {@x = 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): \{@x=s} -> ((\a -> ((a,\{@x=t} -> t) {@x = 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) {@x = 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) {@x = 2} f2 :: (Num a, Num b) => ((?x :: a) => a) -> b -> (a,b) f2 a b = (a,b) {@x = 2} f1 ?x ?x {@x = 1} ==> (1,2) f2 ?x ?x {@x = 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) {@x = 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) {@x = 2} f3 ?x ?x {@x = 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) {@x = 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