Re: Unexpected restriction in "let rec" expressions

[oleg@okmij.org]

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.