[The issue is the semantics of guards in pattern-bindings. As defined,
they are useless if they use a variable bound in the pattern.]
Brian writes:
> I can't see anything in the report to limit guards to mention only free
> variables, but if pattern variables are used in the guards, big problems
> arise with the current translation.
Well, to be more precise, such bindings usually evaluate to _|_
(they will whenever any pattern variable is needed to compute
the result of a guard). For example,
(x,y) | x < 2 || y > 3 = (1,1)
binds both x and y to _|_, rather than 1 as might be expected
[...
Brian argues that patterns should be bound *before* guards are matched
...]
> So I think we need a different semantics for pattern bindings to the
> translation given in the report. I don't know how to express it, though.
One possible dynamic semantics is:
p | g1 = e1
...
| gn = en
== p = let x1@p = e1 in
if g1 then x1
...
else let xn@p = en in
if gn then xn
else error
where the xi are new unbound variables.
This allows:
(x,y) | x == y = (1,x)
== (x,y) = let x1@(x,y) = (1,x) in
if x == y then x1
else error
[I haven't expanded the pattern bindings since they're "obviously"
right, but rather complicated].
It doesn't allow:
[x] | x > 2 = [1]
| x > 3 = e2
| x < 10 = e3
e1 = [1]
e2 = [4,5]
e3 = [9]
The match failure in the second clause will cause termination rather than
matching the third clause. This is probably what's expected, though?
An alternative to allow my second example to match on the third
clause might be:
p | g1 = e1
...
gn = en
== p = let
t1 = case e1 of x1@p' | g1' -> x1
| otherwise -> t2
_ -> t2
...
tn = case en of xn@p' | gn' -> xn
in t1
where (p',gi') = (p,gi) with variables renamed consistently.
The fixpoint now appears at the outer level:
== p = fix ( \ ^p ->
let
t1 = case e1 of x1@p' | g1' -> x1
| otherwise -> t2
_ -> t2
...
tn = case en of xn@p' | gn' -> xn
in t1)
I believe this works (Gofer crashes, but hbc accepts my translation!).
Kevin
