Re: [Caml-list] Polymorphic recursion

["Loup Vaillant" <loup.vaillant@gmail.com>]

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