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

Existential types and W
• Arnaud Spiwack
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-06-08 (20:41) From: Arnaud Spiwack Subject: Existential types and W
```Hi caml list ! How are you today ?

The other day I ran into this fascinating experience, since then I just
can't avoid but try and investigate it (a little). I was trying to
devise a data type representing interactively defined (Coq) terms. It
does not really matter, but when I was thinking of the essence of this
object, it looked something like :

type 'a node = { subterms : [`Leaf of 'b hole | `Node of 'b node] list;
build : 'b -> 'a }

The idea was that you open a list of new subterms to define (called
goals), you solve them, then you use the function to create a term of
type 'a. But, what? That requires existential types!

First time ever I had a use in a non-dependently typed program of
existential types. That was quite a thrill, really. I spent like an hour
looking at this type amazed. But well, looking at it does not really
change the fact : that can't be written in OCaml (please correct me if
I'm wrong).

Of course in Coq (or any such system), it's rather straightfoward to
define ( here goes a Coq definition, in case anyone is interested :
Inductive subterm (B:Type)  (node:Type->Type) : Type:=
| Leaf : hole B -> subterm B node
| Node : node B -> subterm B node
.

Inductive node : forall A:Type, Type :=
mkNode : forall (A B:Type) (subterms : subterm B node) (build : B ->
A), node A. )

There go two questions (three if you count "is there possibly a way to
do that in OCaml that I've missed?") :
1/ Do the reader of this list encounter the need of existential type often?
2/ How would the addition of existential types impact the typing
algorithm of OCaml? (because I must confess that I have absolutely no
clue, would there still be a principal type to every expression? would
that increase complexity?)

Arnaud Spiwack

```