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-05 (08:17) |
From: | Loup Vaillant <loup.vaillant@g...> |
Subject: | Re: [Caml-list] Polymorphic recursion |
2007/4/5, Brian Hurt <bhurt@spnz.org>: > > > On Tue, 3 Apr 2007, Loup Vaillant wrote: > > > I was reading Okasaki's book, "Purely functionnal data structures", > > and discovered that ML (and Ocaml) doesn't support non uniforms > > function definitions. > > > > So, even if: > > > > (**) > > type 'a seq = Unit | Seq of ('a * ('a * 'a)seq);; > > (**) > > This way lies GADTs, which are a really neat idea, but even the > Haskeller's aren't 100% sure how to implement correctly yet. > > In any case, there's a fairly simple work around which does work in the > current type system, which Okasaki describes IIRC. Basically, you just > do: > > type 'a tuple = Tuple of 'a tuple * 'a tuple | Leaf of 'a;; > > type 'a mono_seq = Unit | Set of 'a tuple * 'a seq;; > > which is a bit of a pain, but works. (note: I have renamed "mono_seq" for disambiguation) This workaround doesn't work exactly as intended: as Okasaki pointed at, the binary tree "tuple" is not guaranteed to be balanced. Therefore, even if we can build a trivial injection of type (* seq -> mono_seq *), it will not be a surjection as well. We have lost an invariant, and are forced to maintain it programmatically. This kind of workaround is well known: we call it abstract type. What I find cool with polymorphic types is that more invariants can be checked directly by the type system. It has two advantages: -> It is less error prone when writing the module attached to the type. -> Sometimes, a programmer outside the module can even do pattern matching on this type and still be guaranteed she will not produce a single wrong value. For these reasons,I wanted a way to exploit polymorphic type. You all provided three. I don't mind the syntactic burden, provided someone come up a syntactic shortcut. Loup