Unexpected restriction in "let rec" expressions

Unexpected restriction in "let rec" expressions

[Loup Vaillant]

hello,

I was trying to translate this simple Haskell definition in Ocaml:

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

However, the direct translation doesn't work:

# let loop f a =
  let rec (b, c) = f (a, c) in
    b;;
    Characters 25-31:
    let rec (b, c) = f (a, c) in
            ^^^^^^
Only variables are allowed as left-hand side of `let rec'

So I try to bypass this restriction:

# let loop f a =
  let rec couple = f (a, snd couple) in
    fst couple;;
    Characters 34-51:
    let rec couple = f (a, snd couple) in
                     ^^^^^^^^^^^^^^^^^
This kind of expression is not allowed as right-hand side of `let rec'


Any ideas about what is this restriction, an what is it for?

Thanks,
Loup

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Jean-Christophe Filliâtre]

Loup Vaillant a écrit :
> I was trying to translate this simple Haskell definition in Ocaml:
> 
> loop :: ((a,c) -> (b,c)) -> a -> b
> loop f a = b
>   where (b,c) = f (a,c)
> 
> However, the direct translation doesn't work:
> 
> # let loop f a =
>   let rec (b, c) = f (a, c) in
>     b;;
>     Characters 25-31:
>     let rec (b, c) = f (a, c) in
>             ^^^^^^
> Only variables are allowed as left-hand side of `let rec'
> 
> So I try to bypass this restriction:
> 
> # let loop f a =
>   let rec couple = f (a, snd couple) in
>     fst couple;;
>     Characters 34-51:
>     let rec couple = f (a, snd couple) in
>                      ^^^^^^^^^^^^^^^^^
> This kind of expression is not allowed as right-hand side of `let rec'
> 
> 
> Any ideas about what is this restriction, an what is it for?

Ocaml has call-by-value, and it cannot figure out a value to be passed
as f's second argument. To be convinced, just imagine that the type of
this argument is empty (an empty type can be introduced by "type empty"
without definition, for instance).

-- 
Jean-Christophe

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Damien Doligez]

On 2008-02-26, at 13:24, Loup Vaillant wrote:

> This kind of expression is not allowed as right-hand side of `let rec'
>
> Any ideas about what is this restriction, an what is it for?


The restriction is documented in section 7.3 of the reference manual,
and it's here to make recursive definitions work correctly under
eager evaluation.

-- Damien

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Loup Vaillant]

2008/2/26, Damien Doligez <damien.doligez@inria.fr>:
> The restriction is documented in section 7.3 of the reference manual,
>  and it's here to make recursive definitions work correctly under
>  eager evaluation.

OK, I got it. By the way, replacing "couple" by "couple ()" does the trick:

# let loop f a =
    let rec couple () = f (a, snd (couple ())) in
      fst (couple ());;
    val loop : ('a * 'b -> 'c * 'b) -> 'a -> 'c = <fun>

Now, I have yet to figure out the purpose of this so called "fixpoint
operator" (and if the above will work at all :-).

Thank you all,
Loup

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Gabriel Kerneis]

[-- Attachment #1: Type: text/plain, Size: 997 bytes --]

Le Tue, 26 Feb 2008 15:34:37 +0100, "Loup Vaillant"
<loup.vaillant@gmail.com> a écrit :
> # let loop f a =
>     let rec couple () = f (a, snd (couple ())) in
>       fst (couple ());;
>     val loop : ('a * 'b -> 'c * 'b) -> 'a -> 'c = <fun>
> 
> Now, I have yet to figure out the purpose of this so called "fixpoint
> operator" (and if the above will work at all :-).

No, it won't:
Objective Caml version 3.10.1
# let loop f a =
    let rec couple () = f (a, snd (couple ())) in
      fst (couple ());;
    val loop : ('a * 'b -> 'c * 'b) -> 'a -> 'c = <fun>
# loop (fun x -> x) 1 ;;
Stack overflow during evaluation (looping recursion?).

Whereas:

GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
Prelude> :load test
[1 of 1] Compiling Main             ( test.hs, interpreted )
Ok, modules loaded: Main.
*Main> loop id 1
1

You could (maybe) get it using the Lazy module.

Regards,
-- 
Gabriel Kerneis

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 189 bytes --]

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[blue storm]

Your "loop" function looks similar to some concepts of "Circular
programming" ( http://www.haskell.org/haskellwiki/Circular_programming
).

I've been interested in the translation of such code into OCaml a few
weeks ago, and i came with a different solution, wich use lazy
evaluation (of course there may be a better way to do it) :

let trace f input =
  let rec out_feed = lazy (f (input, lazy (snd (Lazy.force out_feed)))) in
  let a = Lazy.force out_feed in fst a

The returned type (('a * 'b lazy_t -> 'c * 'b) -> 'a -> 'c) express
the fact that the input tuple is lazy on its second parameter.

Here is the repIImin example, translated into OCaml :
type 'a tree = Leaf of 'a | Branch of ('a tree * 'a tree)

let repIImin tree =
  let rec repIImin' = function
  | Leaf r, min -> lazy (Leaf (Lazy.force min)), r
  | Branch (a, b), mini ->
      let (a', mina) = repIImin' (a, mini) in
      let (b', minb) = repIImin' (b, mini) in
      lazy (Branch (Lazy.force a', Lazy.force b')), (min mina minb)
 in Lazy.force (trace repIImin' tree)

However, i'm not sure this example is very useful. The intended
benefits (one pass traversal) is moot, as it actually is a two-pass
traversal (one being hidden in the call tree of the Lazy.force
functions), and the code is of course much slower than the plain
two-pass version.

-- bluestorm

On 2/26/08, Loup Vaillant <loup.vaillant@gmail.com> wrote:
> 2008/2/26, Damien Doligez <damien.doligez@inria.fr>:
> > The restriction is documented in section 7.3 of the reference manual,
> >  and it's here to make recursive definitions work correctly under
> >  eager evaluation.
>
> OK, I got it. By the way, replacing "couple" by "couple ()" does the trick:
>
> # let loop f a =
>     let rec couple () = f (a, snd (couple ())) in
>       fst (couple ());;
>     val loop : ('a * 'b -> 'c * 'b) -> 'a -> 'c = <fun>
>
> Now, I have yet to figure out the purpose of this so called "fixpoint
> operator" (and if the above will work at all :-).
>
> Thank you all,
> Loup
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Dirk Thierbach]

On Tue, Feb 26, 2008 at 01:24:57PM +0100, Loup Vaillant wrote:
> I was trying to translate this simple Haskell definition in Ocaml:
> 
> loop :: ((a,c) -> (b,c)) -> a -> b
> loop f a = b
>   where (b,c) = f (a,c)

How do you expect that to work under strict instead of lazy evaluation? :-)

- Dirk

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Nicolas Pouillard]

[-- Attachment #1: Type: text/plain, Size: 950 bytes --]

Excerpts from loup.vaillant's message of Tue Feb 26 15:34:37 +0100 2008:
> 2008/2/26, Damien Doligez <damien.doligez@inria.fr>:
> > The restriction is documented in section 7.3 of the reference manual,
> >  and it's here to make recursive definitions work correctly under
> >  eager evaluation.
> 
> OK, I got it. By the way, replacing "couple" by "couple ()" does the trick:
> 
> # let loop f a =
>     let rec couple () = f (a, snd (couple ())) in
>       fst (couple ());;
>     val loop : ('a * 'b -> 'c * 'b) -> 'a -> 'c = <fun>
> 
> Now, I have yet to figure out the purpose of this so called "fixpoint
> operator" (and if the above will work at all :-).

A picture can helps...

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

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

loop x = y

Regards,

-- 
Nicolas Pouillard aka Ertai

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 194 bytes --]

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Andrej Bauer]

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

You said the above was a "so-called fixpoint operator". To see in what 
sense this really is a fixpoint operator consider the type:

   ((a * c) -> (b * c)) -> a -> b                    (1)

It is equivalent (under currying-uncurrying) to

   (a -> (c -> b) * (c -> c)) -> a -> b              (2)

We could write down a term of this type if we had a way of going from
type c -> c to type c. More precisely, consider any term

   fix : (c -> c) -> c,

where the name "fix" suggests that we will plug in a fix-point operator 
at the end of the day. Before reading on, you should try to write down a 
term of type (2), given that we have fix. I will bet that your brain 
will produce the same solution as described below.

We can get a term of type (2) by defining

   let loop' f x =
     let (g, h) = f x in g (fix h)

Converting from (2) back to (1) gives us an equivalent term

   let loop f x =
     let f' y = (fun z -> fst (f (y, z))), (fun z -> snd (f (y, z))) in
       loop' f' x

or by beta-reducing:

   let loop f x =
     fst (f (x, fix (fun z -> snd (f (x, z)))))

You are now free to plug in whatever you wish for fix, but presumably 
you would like fix to compute fixed points. This may be somewhat 
troublesome in an eager language, especially if c is not a function type.

In fact, we may recover fix from loop as follows:

   let fix' f = loop (fun (_, z) -> (z, f z)) ()

To see that fix' is the same as fix, we just beta-eta reduce:

   fix' f =
   loop (fun (_, z) -> (z, f z)) () =
   fst (fix (fun z -> f z), f (fix (fun z -> f z))) =
   fix (fun z -> f z) =
   fix f

Indeed, loop is a generalized fixpoint operator.

But I think the nice picture drawn by Nicolas Pouillard is worth a 
thousand lambda terms.

Best regards,

Andrej

P.S. Can someone think of anything else other than a fixpoint operator 
that we could use in place of fix to get an interesting program (maybe 
for special cases of c, such as c = int -> int)?

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Loup Vaillant]

OK, I'm starting to understand all this a bit more, thank you all.

2008/2/26, Nicolas Pouillard <nicolas.pouillard@gmail.com>:
> A picture can helps...
>
>      +---------+
>   a>-|         |->c
>      |    x    |
>   b>-|         |->b
>      +---------+
>
>      +---------+
>   a>-|         |->c
>      |    y    |
>   +->-|         |->-+
>   |   +---------+   |
>   +--------b--------+
>
>  loop x = y

I saw this image before, but despite of its clarity, it hasn't solved
my problem: the chicken and egg one. See, the looping "b" in y looks
like it has to be produced out of thin air. The only solution I can
guess is that x must, for some value of "a", produce the outputs "c"
and "b" independently of the input "b". Then, the recursion in loop
must reach this particular value of "a".

Maybe I could understand this by writing a factorial function, using a
non recursive function and loop (I hope this is possible).

2008/2/27, Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>:
>  where the name "fix" suggests that we will plug in a fix-point operator
>  at the end of the day. Before reading on, you should try to write down a
>  term of type (2), given that we have fix. I will bet that your brain
>  will produce the same solution as described below.

It did :-), but it will take a bit of my time to understand the rest.

Cheers,
Loup

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Dirk Thierbach]

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

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Loup Vaillant]

2008/2/27, Dirk Thierbach <dthierbach@gmx.de>:
> [...]
>  Does that explanation help?

Yes, it does, but I have difficulties reducing this expression. Do you
have another example which can be reduced to head normal form (say the
result is an int instead of a list)?

Thanks,
Loup

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Dirk Thierbach]

On Wed, Feb 27, 2008 at 03:04:03PM +0100, Loup Vaillant wrote:
> Yes, it does, but I have difficulties reducing this expression. 

Where is the problem?

> Do you have another example which can be reduced to head normal form
> (say the result is an int instead of a list)?

Not with ground types, but would the factorial function help?

f (x,g) = (g x, g') where
  g' 0 = 1
  g' y = y * g (y-1)

*Main> [loop f x | x <- [0..10]]
[1,1,2,6,24,120,720,5040,40320,362880,3628800]

One can imagine that in a similar way to the list: The function g
goes round the loop and more and more results get defined.

BTW, lazy evaluation uses weak head normal form (WHNF), not head normal
form.

- Dirk

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Pal-Kristian Engstad]

Loup Vaillant wrote:
> loop :: ((a,c) -> (b,c)) -> a -> b
> loop f a = b
>   where (b,c) = f (a,c)
>   
Remember that values in Haskell are lazy, which simply means that they 
are pointers to things that is either a pointer to a function to 
evaluate it, or the cached value. (This works, since all Haskell values 
are immutable.)

So, what we have here is a specification on how to calculate (b,c) from 
(a, c), given a function f :: (a,c) -> (b, c), and a. In order to 
evaluate b, we must evaluate the pair (b, c), i.e. evaluate the function 
call. Here we're using the value c, which is undefined - except that we 
have one constraint. The second result value is the same as c, and since 
a value is always immutable, it means that the second result value must 
be the *same value* as the second input value.

In other words, we're telling the compiler: Given a function f :: (a, c) 
-> (b, c) and a value of type a, loop f a will give the result b by 
evaluating (b, c') = f (a, c) where c' == c always.

An example function is:

g (a, c) = (c a, (*2))

Here' the constraint is telling us that c == (*2), and since we're 
returning the first parameter, the result is [c a == (*2) a == a * 2].

Another:

g (a, c) = (a + c, 2)

Now, c == 2, thus loop g a == a + 2.

The other examples are of the same theme.

g (a, c) = (c, a : map (+a) c), means that c == a : map (+a) c, which 
again is a recursive definition, and since everything is lazy this 
works. The first element in the list is a, when the second element is 
requested, map (+a) c is requested, but that means requesting c again 
which equals a : map (+a) c, so we get map (+a) (a : map (+a) c), which 
requires just the head  of the cons-cell,which is a, so the result is 
(+a) a : map (+a) (map (+a) c), which is (a + a) : (map (+a) $ map (+a) c)

Hope it helps,

PKE

-- 
Pål-Kristian Engstad (engstad@naughtydog.com), 
Lead Graphics & Engine Programmer,
Naughty Dog, Inc., 1601 Cloverfield Blvd, 6000 North,
Santa Monica, CA 90404, USA. Ph.: (310) 633-9112.

"Most of us would do well to remember that there is a reason Carmack
is Carmack, and we are not Carmack.",
                       Jonathan Blow, 2/1/2006, GD Algo Mailing List

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Loup Vaillant]

2008/2/27, Dirk Thierbach <dthierbach@gmx.de>:
> On Wed, Feb 27, 2008 at 03:04:03PM +0100, Loup Vaillant wrote:
>  > Yes, it does, but I have difficulties reducing this expression.
>
> Where is the problem?

After reducing the call to loop and inlining f in the resulting
expression, I couldn't reduce the recursive let anymore. I thought of
replacing the let by a lambda expression, but since it is recursive,
it can't be done (or at least it's not trivial). But this is not a
problem anymore.

>  > Do you have another example which can be reduced to head normal form
>  > (say the result is an int instead of a list)?
>
> Not with ground types, but would the factorial function help?
>
>  f (x,g) = (g x, g') where
>   g' 0 = 1
>   g' y = y * g (y-1)
>
>  *Main> [loop f x | x <- [0..10]]
>  [1,1,2,6,24,120,720,5040,40320,362880,3628800]

Cool, this is exactly what I wanted, thanks.

>  BTW, lazy evaluation uses weak head normal form (WHNF), not head normal
>  form.

This is precisely why I wanted the result type to be such that
WHNF=>HNF. Int is such a type. List is not.

Loup

Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Loup Vaillant]

Yahoo! I got it, many thanks!

2008/2/27, Pal-Kristian Engstad <pal_engstad@naughtydog.com>:
> Loup Vaillant wrote:
>  > loop :: ((a,c) -> (b,c)) -> a -> b
>  > loop f a = b
>  >   where (b,c) = f (a,c)
>
> Remember that values in Haskell are lazy, which simply means that they
>  are pointers to things that is either a pointer to a function to
>  evaluate it, or the cached value. (This works, since all Haskell values
>  are immutable.)

No problem with that. I just have some subtleties to learn about lazy
graph reduction yet. What is a bit harder is to turn myself in a
strictness analyzer when writing lazy code in my favorite strict
language :-).

> [...]
>
>  In other words, we're telling the compiler: Given a function f :: (a, c)
>  -> (b, c) and a value of type a, loop f a will give the result b by
>  evaluating (b, c') = f (a, c) where c' == c always.

That is the explanation I have waited for. I didn't have the idea to
push mathematical reasoning to the end, so I continued to bother
myself with an order of evaluation (even lazy), forgetting what a non
strict semantic really means. Thank you.

Loup

PS: do you use Ocaml (or whatever FP language or technique) at
naughtydog? What for, then (provided you can tell me, of course)?