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.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 22E71BC69 for ; Fri, 4 May 2007 14:09:47 +0200 (CEST) Received: from postar.fmf.uni-lj.si (vega.fmf.uni-lj.si [193.2.67.45]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l44C9kQn007645 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Fri, 4 May 2007 14:09:46 +0200 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id CBCF013028F for ; Fri, 4 May 2007 14:09:43 +0200 (CEST) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id ITOLPEOV5uq0 for ; Fri, 4 May 2007 14:31:00 +0200 (CEST) Received: from [193.2.67.88] (unknown [193.2.67.88]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 913A41302B7 for ; Fri, 4 May 2007 14:09:43 +0200 (CEST) Message-ID: <463B2364.9070102@fmf.uni-lj.si> Date: Fri, 04 May 2007 14:13:24 +0200 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Icedove 1.5.0.10 (X11/20070328) MIME-Version: 1.0 To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] wrapping parameterized types References: <4a051d930705031531m396e42e7i6212137e2fb9cd53@mail.gmail.com> <875c7e070705031616w50ca595m2e55bda049ba7aa6@mail.gmail.com> <1178241003.7436.10.camel@rosella.wigram> <61164.84.165.181.194.1178279247.squirrel@www.ps.uni-sb.de> In-Reply-To: <61164.84.165.181.194.1178279247.squirrel@www.ps.uni-sb.de> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 463B228A.003 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 andrej:01 rossberg:01 existential:01 o'caml:01 existential:01 quantifier:01 quantifier:01 forall:01 forall:01 ocaml:01 sourceforge:01 polymorphic:01 wrote:01 wrote:01 rossberg@ps.uni-sb.de wrote: > "skaller" wrote: >> On Thu, 2007-05-03 at 19:16 -0400, Chris King wrote: >>> The solution is to use existential types. In a record, you can tell >>> O'Caml that a particular function _must_ be polymorphic: >>> >>> type 'b mylistfun = { listfun: 'a. 'a list -> 'b } >> I'm still confused why this is called an existential, when >> clearly the quantification is universal. > > You have reason to be confused, because this is no existential type. > > Dirk Thierbach: >> It's because the universal quantifier is in a "negative" position, >> which is equivalent to an existential quantifier on the outside. >> Just pretend they are logic formulae instead of types, and then >> >> (\forall a. a) -> b is equivalent to \exists a. (a -> b) > > Actually, no, these are not equivalent. Only the following are: > > (\exists a. a) -> b is equivalent to \forall a. (a -> b) Right, and this is in accordance with the terminology. Note that Dirk misread the precedence of operators: in ocaml 'a . 'a list -> 'b means 'a . ('a list -> 'b) and not ('a . 'a list) -> 'b. So everything is fine. I do agree with skaller that it is a bit perverse to call a quantifier "existential" when it is obviously the universal quantifier, even if it is equivalent to a formula containing an existential. Andrej