>From: Ben Rudiak-Gould <Benjamin.Rudiak-Gould(a)cl.cam.ac.uk>
>Subject: Re: Bang patterns, ~ patterns, and lazy let
>
>It's also not that case that !x has the same
>meaning in both proposals, e.g.
>
> let { !x = y ; !y = const 'a' x } in x
>
>means 'a' in the current proposal but _|_ in yours.
>
>
Aargh, you're right, it does mean _|_ in mine! That's not very nice.
But wait, I'm not sure about
let { !x = const undefined y ; !y = const 'a' x } in y
desugars in the current proposal to
let { x = const undefined y ; y = const 'a' x } in x `seq` y `seq` y
which is _|_, but absent implicit ~,
let { x = const undefined y ; y = const 'a' x } in y
had better (and does) mean 'a'.
Applying the rules on the wiki, the first step is to translate the first
expression into a tuple binding, omitting the implicit ~:
let (x,y) = (const undefined y, const 'a' x) in y
This desugars to
let (x,y) = fix (\ ~(x,y)->(const undefined y, const 'a' x)) in y
which evaluates to 'a'. In other words, despite the ! on x, the current
proposal is not strict in x.
Maybe the intention was that !s on the lhs of let bindings should be
transferred to the corresponding patterns when a tuple pattern is
introduced? Let's try it: then the example desugars by pattern tupling to
let (!x, !y) = (const undefined y, const 'a' x) in y
Now we can introduce fix:
let (!x, !y) = fix (\ ~(!x, !y) -> (const undefined y, const 'a' x))
in y
and finally case:
case fix (\~(!x,!y) -> (const undefined y, const 'a' x)) of ~(!x,
!y) -> y
and this is consistent with what you said above.
But if I return to your first example, and do the same thing, I get
let !x = y; !y = const 'a' x in x
desugars by tupling to
let (!x, !y) = (y, const 'a' x) in x
which desugars by fix and case introduction to
case fix (\ ~(!x, !y) -> (y, const 'a' x)) of ~(!x, !y) -> x
The first approximation to the fixed point is _|_, so the second is
(_|_, 'a'). Now, when ~(!x,!y) is matched against (_|_,'a') then *both*
variables are bound to _|_ --- the effect of the ~ is just to delay
matching (!x,!y) until one of the variables is used, but as soon as y,
say, *is* used, then the match is performed and, of course, it loops.
Thus (_|_, 'a') is the fixed point. For the same reason, x and y are
both bound to _|_ in the body of the case, and so the entire expression
evaluates to _|_, not 'a' as you claimed.
Bottom line: I can't find a way to interpret the translation rules in
the Haskell report, modified as the Wiki page suggests, to produce the
results you expect in both cases.
But maybe the fault is in the translation rules in the Haskell report.
It was always rather tricky to explain a group of recursive bindings in
Haskell in terms of a single tuple binding, because Haskell tuples are
lifted. I see that you have a more direct understanding of what ! is
supposed to mean. Is it possible, I wonder, to give a direct
denotational semantics to a declaration group--say mapping environments
to environments--in which there is only one case for ! (its natural
semantics in patterns)? Such a semantics should have the property that
let x1 = e1; x2 = e2 in e0 === let x1 = e1 in let x2 = e2 in e0
provided x1 does not occur in e2. Finding a simple and compositional
denotational semantics with these properties, and proving the law above,
would be a good way to show that ! patterns do NOT introduce semantic
warts---and would probably also suggest that the
semantics-by-translation used in the report is fundamentally flawed. We
did construct denotational semantics of fragments of Haskell as part of
the original design, and it had quite an impact on the result--I
recommend it as a way of debugging ideas!
John
