Existential types and W

Existential types and W

[Arnaud Spiwack]

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

Re: [Caml-list] Existential types and W

[Daniel Bünzli]

Le 8 juin 07 à 22:41, Arnaud Spiwack a écrit :

> 1/ Do the reader of this list encounter the need of existential  
> type often?

Sometimes it can be useful to express an abstract type + operations  
without going through functors which only provide static existential  
types. This allows to store in the same datastructure such types +  
operations with different implementations. For example imagine a  
spatial datastructure with both float32 bigarrrays and regular caml  
float arrays.

> 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?)

I don't know.

But if you really need them they can be encoded in the current type  
system, see the discussion here [1].

Best,

Daniel

[1] http://caml.inria.fr/pub/ml-archives/caml-list/ 
2004/01/52732867110697f55650778d883ae5e9.fr.html