Version franēaise
Home     About     Download     Resources     Contact us    
Browse thread
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 <dthierbach@g...>
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
and round the loop, and with each step gaining more information
(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
orders) can make the "gain more information" idea concrete, and also
make a bit more clear why it is called a "fixpoint". Google for those
if you want to learn more.

- Dirk