This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Polymorphic recursion
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-04-04 (16:52) From: Roland Zumkeller 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/

```