Existential types and W
 Arnaud Spiwack
[
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:   (:) 
From:  Arnaud Spiwack <aspiwack@l...> 
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 nondependently 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