Why is there a space leak here?

[Claus Reinke]

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