Re: Unexpected restriction in "let rec" expressions

Re: Unexpected restriction in "let rec" expressions

[oleg]

Andrej Bauer wrote:
> 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.
> ...
> 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)?

`For special cases if c' makes the problem very easy. For example, let
c = int:

# let pseudofixint f : int = f 0;;
val pseudofixint : (int -> int) -> int = <fun>

or let c = int-> int

# let anotherpseudofix f : int -> int = f (fun (x:int) -> x);;
val anotherpseudofix : ((int -> int) -> int -> int) -> int -> int = <fun>

It is only if we insist on a polymorphic function (for all c or at least
c = a-> b for all a and b) that we obtain that fix must be either a
fix-point combinator or a similar misbehaving term such as

# let almostfix (f:'c -> 'c) = f (failwith "what could you expect");;
val almostfix : ('a -> 'a) -> 'a = <fun>

This is because only fix or similar misbehaving combinators let us
`produce' values that do not exist (or at least, claim to produce those
values). For example:

# type unicorn  (* abstract *)
# let f (x:unicorn) = x
val f : unicorn -> unicorn = <fun>

Indeed, we can always demonstrate a value of the type c->c no matter
how bizarre c is. Thus, expression (almostfix f) has the type unicorn
and `gives' us the value of unicorns, `proving' that unicorns exist.

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