From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.9 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id D0D17BC0A for ; Fri, 8 Jun 2007 22:41:05 +0200 (CEST) Received: from ug-out-1314.google.com (ug-out-1314.google.com [66.249.92.174]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l58Kf5wh010838 for ; Fri, 8 Jun 2007 22:41:05 +0200 Received: by ug-out-1314.google.com with SMTP id p27so963617ugc for ; Fri, 08 Jun 2007 13:41:05 -0700 (PDT) DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:user-agent:mime-version:to:subject:content-type:content-transfer-encoding:sender; b=lIcOd9OUvPSBtOwXQJe1IRNeLsPdRcnrufA18Cl/yVPYKvxy90Fk7P0wIGOChEOjCgiqA8KKszpBDGwqDVkLpmpAZOYuqemg/3Srs+mpYcUOCoaka430XLwlpeYqFDqzJzJYrRnMXyY8hYUXIuB9jS9vtAiM/+20PrzSDJmJlDU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:user-agent:mime-version:to:subject:content-type:content-transfer-encoding:sender; b=kx3nyZHAcJ6yrvLhQ3AD12iwtzsfhIysAKtErgdSZQRQ/MHCcHQSYajiW1ZdYGOXSOPrAA4gNtyvqNqyHUWXqNPAfy6VYQeZnoykDQN5sXYQc5fq/1ron+YWETdAB7ZcCnf0MaypsHIkQRiglrFqNOGVGxfLvlPoMbChH4qzAoA= Received: by 10.66.242.5 with SMTP id p5mr3044552ugh.1181335265084; Fri, 08 Jun 2007 13:41:05 -0700 (PDT) Received: from ?192.168.0.3? ( [87.88.165.197]) by mx.google.com with ESMTP id k30sm5582961ugc.2007.06.08.13.41.04 (version=SSLv3 cipher=RC4-MD5); Fri, 08 Jun 2007 13:41:04 -0700 (PDT) Message-ID: <4669BEDF.9010109@lix.polytechnique.fr> Date: Fri, 08 Jun 2007 22:41:03 +0200 From: Arnaud Spiwack User-Agent: Thunderbird 2.0.0.0 (Windows/20070326) MIME-Version: 1.0 To: caml-list@inria.fr Subject: Existential types and W Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: Arnaud Spiwack X-Miltered: at concorde with ID 4669BEE1.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lix:01 existential:01 coq:01 node:01 node:01 existential:01 ocaml:01 coq:01 subterm:01 subterm:01 forall:01 forall:01 ocaml:01 fascinating:98 thrill:98 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