Browse thread
Polymorphic recursion
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2007-04-04 (16:52) |
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/