Existential types and W

[Arnaud Spiwack <aspiwack@lix.polytechnique.fr>]

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