From: "Tom Moertel" <tom-list-haskell@moertel.com>
Okay, then, what is the *right* way to reason about these things?
(Non?-)strictly speaking, there is no *right* way to reason about these things, as Haskell somehow seems to have neglected to acquire a semantics (blush - even Java has one, kind of..). The reason, as far as I can tell, is that everyone assumed that the core of Haskell is sufficiently similar to "standard" calculi (some of which were developed to make this so), so that those or "standard" works on implementation implicitly define what everyone assumes to be Haskell's semantics (I find it funny that the report, which equates "non-strict" and "lazy", refers to potential loss of sharing in two places, without ever bothering to explain how such sharing might come about in the first place.. or am I missing anything?). Perhaps one could say that Haskell was too lazy to acquire a semantics before it was needed?-) But call-by-need lambda-calculus, refered to in other replies, was developed in anticipation or awareness of that need, I think, and is a good place to get started without having to worry about implementation details.
v = 1 : flatten (map single v) = 1 : flatten (map single (1 : flatten (map single v))) = 1 : flatten (single 1 : map single (flatten (map single v))) = 1 : flatten ([1] : map single (flatten (map single v))) = 1 : 1 : flatten (map single (flatten (map single v))) = Aaaarrggggh! You're right.
In essence, call-by-need is normal-order evaluation plus sharing of parameters, so you can adapt your deduction (which follows normal-order reduction, but ignores sharing) by taking care of sharing (I'll use where for that here): v = 1 : flatten (map single v) -> v = 1 : tl_v where tl_v = flatten (single 1 : map single tl_v) -- don't lose that sharing -> v = 1 : tl_v where tl_v = flatten ([1] : map single tl_v) -> v = 1 : tl_v where tl_v = 1 : flatten (map single tl_v) -- this looks familiar .. -> v = 1 : tl_v where tl_v = 1 : tl_tl_v -- there is now only one reference to this tl_tl_v = 1 : flatten (map single tl_tl_v) = v = 1 : 1 : tl_tl_v where tl_tl_v = 1:flatten (map single tl_tl_v) .. I've tried to stay close to your own derivation, but otherwise this should really correspond to Mark Tullsen's earlier posting. This might already enable you to adapt your derivation for the version with triple instead of single, but I would still suggest to have a look at the CBN papers. To complement my own earlier posting, GHood builds on Hood, which doesn't observe sharing or garbage-collection, so if one of these is important to the argument, observations have to be interpreted with more care than usual.Still, it can be quite helpful because it can give you some input about your program's behaviour Hth, Claus