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.4 required=5.0 tests=AWL,NO_REAL_NAME 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 D349ABC69 for ; Fri, 4 May 2007 13:47:30 +0200 (CEST) Received: from uni-sb.de (uni-sb.de [134.96.252.33]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l44BlUrW002704 for ; Fri, 4 May 2007 13:47:30 +0200 Received: from mail.cs.uni-sb.de (mail.cs.uni-sb.de [134.96.254.200]) by uni-sb.de (8.14.1/2007040500) with ESMTP id l44BlSAp016679; Fri, 4 May 2007 13:47:28 +0200 (CEST) Received: from mail.ps.uni-sb.de (james.ps.uni-sb.de [134.96.186.68]) by mail.cs.uni-sb.de (8.14.1/2007041300) with ESMTP id l44BlS9L028320; Fri, 4 May 2007 13:47:28 +0200 (CEST) Received: from localhost ([127.0.0.1] helo=www.ps.uni-sb.de ident=www-data) by mail.ps.uni-sb.de with esmtp (Exim 4.50) id 1HjwFz-0001uH-Hl; Fri, 04 May 2007 13:47:28 +0200 Received: from 84.165.181.194 (SquirrelMail authenticated user rossberg) by www.ps.uni-sb.de with HTTP; Fri, 4 May 2007 13:47:27 +0200 (CEST) Message-ID: <61164.84.165.181.194.1178279247.squirrel@www.ps.uni-sb.de> In-Reply-To: <1178241003.7436.10.camel@rosella.wigram> References: <4a051d930705031531m396e42e7i6212137e2fb9cd53@mail.gmail.com> <875c7e070705031616w50ca595m2e55bda049ba7aa6@mail.gmail.com> <1178241003.7436.10.camel@rosella.wigram> Date: Fri, 4 May 2007 13:47:27 +0200 (CEST) From: rossberg@ps.uni-sb.de To: caml-list@yquem.inria.fr Cc: "Chris King" , "skaller" User-Agent: SquirrelMail/1.4.4 MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Priority: 3 (Normal) Importance: Normal X-SA-Exim-Connect-IP: 127.0.0.1 X-SA-Exim-Mail-From: rossberg@ps.uni-sb.de Subject: Re: [Caml-list] wrapping parameterized types X-SA-Exim-Version: 4.2 (built Thu, 03 Mar 2005 10:44:12 +0100) X-SA-Exim-Scanned: Yes (on mail.ps.uni-sb.de) X-Miltered: at discorde with ID 463B1D52.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; rossberg:01 existential:01 o'caml:01 existential:01 quantifier:01 quantifier:01 forall:01 forall:01 cheers:01 sourceforge:01 polymorphic:01 wrote:01 wrote:01 caml-list:01 andreas:01 "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) Here is the constructive proof. Assume: f : (exists a.a) -> b g : forall a. (a -> b) You can construct g from f and vice versa: g = \a. \a:x. f f = \y:(exists a.a). let = y in g a x Cheers, - Andreas