On Aug 28, 2009, at 5:31 PM, Bernd Brassel wrote:
> Okay, then how about the following example: for the declarations
>
> data C a = C ?a
> plus (C x) (C y) = x+y
>
> do the following expressions all have the same semantics?
>
> e1 = let x=C (0?1) in plus x x
> e2 = let y=0?1 in let x=C y in plus x x
> e3 = let y=0?1 in let x=C y in const (plus x x) y
Instead of trying the implementation again, I express these examples
monadically and use the equational laws from [1] to reason about their
meaning. The extension to the laws that implements annotated arguments
is in the (HNF) rule. Specialised to the data type above, the (HNF)
rule is:
share (return (C a)) = return (return (C a))
instead of the original deeply sharing version:
share (return (C a)) = share a >>= \a' -> return (return (C a'))
Your datatype and functions are translated as follows:
data C m a = C (m a)
plus a b = a >>= \ (C c) ->
b >>= \ (C d) ->
c >>= \ x ->
d >>= \ y ->
return (x+y)
const x _ = x
e1 = share (return (C (return 0 `mplus` return 1))) >>= \x ->
plus x x
-- y is not shared (does not occur more than once)
e2 = let y = return 0 `mplus` return 1
in share (return (C y)) >>= \x -> plus x x
-- now, y is shared
e3 = share (return 0 `mplus` return 1) >>= \y ->
share (return (C y)) >>= \x -> const (plus x x) y
We can see that e1 = e2 by substituting the let bound variable y and
evaluating the const call. However, for e3 we must apply the (Choice)
rule on the first occurrence of share which yields:
share (return 0) >>= \y -> share (return (C y)) >>= \x -> plus x x
`mplus`
share (return 1) >>= \y -> share (return (C y)) >>= \x -> plus x x
This reduces (in several steps) to:
plus (return (C (return 0))) (return (C (return 0)))
`mplus`
plus (return (C (return 1))) (return (C (return 1)))
and finally to: return 0 `mplus` return 2
On the other hand, e1---using the adjusted (HNF) rule---reduces to:
return (return (C (return 0 `mplus` return 1))) >>= \x -> plus x x
= plus (return (C (return 0 `mplus` return 1)))
(return (C (return 0 `mplus` return 1)))
= ...
= return 0 `mplus` return 1 `mplus` return 1 `mplus` return 2
So, e1 and e2 have the same semantics but e3 has a different semantics
when using the changed (HNF) rule (with the original (HNF) rule (that
is, without annotations) e3 has the same semantics as e1 and e2). I
have added your examples to [2].
They show that my interpretation of Wolfgangs proposal in the explicit
sharing framework is probably inaccurate (I think, also with
annotations, e1, e2, and e3 should have the same semantics.)
The question is then: what is the intended meaning of Wolfgangs
proposal and how can we formalise it?
If the translation scheme to monadic code would introduce 'share' for
let-bound variables regardless of whether they are shared then e2
would have the same meaning as e3 under the new (HNF) rule. But the
semantics of e1 would still be different -- as intended by the
annotation. In fact, I suspect that Wolfgang's intuition behind his
proposal is that all expressions e1, e2, and e3 can yield the result
1, so this change in the translation scheme would go into the wrong
direction.
Cheers,
Sebastian
[1]:
http://www.cs.rutgers.edu/~ccshan/rational/lazy-nondet.pdf
[2]:
http://gist.github.com/176983
--
Underestimating the novelty of the future is a time-honored tradition.
(D.G.)
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mo Aug 31 2009 - 09:29:57 CEST