Version française
Home     About     Download     Resources     Contact us    
Browse thread
Polymorphic recursion
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Roland Zumkeller <roland.zumkeller@g...>
Subject: Re: [Caml-list] Polymorphic recursion
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/