Re: [Caml-list] Polymorphic recursion

["Roland Zumkeller" <roland.zumkeller@gmail.com>]

On 04/04/07, Alain Frisch <Alain.Frisch@inria.fr> wrote:
> Alain Frisch wrote:
> > but since there is no value of type ('a * 'a as 'a)
>
> Sorry, there are actually values in this type, but they are all
> structurally equal to the result of "let rec x = (x,x) in x".

Yes, but "('a * 'a as 'a) seq" has more than one value (modulo
structural equality), so it works to *some* extent:

# let rec x = (x,x);;
val x : 'a * 'a as 'a =
# size (Seq (x,Unit));;
- : int = 1
# size (Seq (x, Seq (x,Unit)));;
- : int = 3

However, you are right in pointing out that this limited use won't be
helpful for most applications, so I'd suggest:

# let rec size = function
| Unit -> 0
| Seq (_, b) -> 1 + 2 * size (Obj.magic b);;
    val size : 'a seq -> int = <fun>

The function can be checked in richer type systems with annotations
(e.g. Coq's), so we know that Obj.magic is not dangerous here.

Roland

-- 
http://www.lix.polytechnique.fr/~zumkeller/