Unexpected restriction in "let rec" expressions
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: -- (:) From: Dirk Thierbach Subject: Re: [Caml-list] Unexpected restriction in "let rec" expressions
```On Wed, Feb 27, 2008 at 10:43:18AM +0100, Loup Vaillant wrote:
> 2008/2/26, Nicolas Pouillard <nicolas.pouillard@gmail.com>:
> > A picture can helps...

Fixed names to be consistent with

loop :: ((a,c) -> (b,c)) -> a -> b
loop f a = b where (b,c) = f (a,c)

>>
>>      +---------+
>>   a>-|         |->b
>>      |    x    |
>>   c>-|         |->c
>>      +---------+
>>
>>      +---------+
>>   a>-|         |->b
>>      |    y    |
>>  +->-|         |->-+
>>  |   +---------+   |
>>  +--------c--------+
>>

> I saw this image before, but despite of its clarity, it hasn't solved
> my problem: the chicken and egg one. See, the looping "c" in y looks
> like it has to be produced out of thin air.

It's easier to think this in Haskell, because then one hasn't to deal
with lazyness explicitely. Consider

f (a,c) = (c, a : map (+a) c)

That's a perfectly non-recursive function. Now, what happens when
we apply "loop" to it?

*Main> take 10 \$ loop f 1
[1,2,3,4,5,6,7,8,9,10]
*Main> take 10 \$ loop f 2
[2,4,6,8,10,12,14,16,18,20]

Ah, so it actually does produce values out of thin air :-) How did that
happen? Well, inside f, we used the argument c before it was really
defined, but in doing so, we added information *before* feeding it back
through the loop. One can picture the "incomplete" list going round
(here for a = 1):

?
1,?
1,2,?
1,2,3,?

and so on. Of course that's not what really happens during the
computation -- there lazy evaluation takes care that the unkown part
isn't actually evaluated before it has been defined. With strict
evaluation, the complete argument is evaluated on function call, so
this doesn't work.

BTW, the "canonical" fixpoint operator, also called Y-combinator,

fix : (a -> a) -> a

which has already been mentioned can be thought of in a similar way.

Does that explanation help?

And a semantic explanation with domains (a special kind of partial