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=1.0 required=5.0 tests=AWL,SPF_FAIL 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 35599BC69 for ; Fri, 4 May 2007 10:32:03 +0200 (CEST) Received: from mail.gmx.net (mail.gmx.net [213.165.64.20]) by discorde.inria.fr (8.13.6/8.13.6) with SMTP id l448W2H0002732 for ; Fri, 4 May 2007 10:32:02 +0200 Received: (qmail invoked by alias); 04 May 2007 08:32:01 -0000 Received: from dialin-145-254-251-027.pools.arcor-ip.net (EHLO dialin-145-254-251-027.pools.arcor-ip.net) [145.254.251.27] by mail.gmx.net (mp035) with SMTP; 04 May 2007 10:32:01 +0200 X-Authenticated: #11134691 X-Provags-ID: V01U2FsdGVkX1+P9H4tFDqPCKn1HENfySQozqDseT9oO1HZ1hMH6S 8pFeW6+hDp9hDd Received: from dirk by feanor.private-host.de with local (masqmail 0.2.20) id 1HjsuY-0U9-00 for ; Fri, 04 May 2007 10:13:06 +0200 Date: Fri, 4 May 2007 10:13:06 +0200 To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] wrapping parameterized types Message-ID: <20070504081306.GA1708@feanor> References: <4a051d930705031531m396e42e7i6212137e2fb9cd53@mail.gmail.com> <875c7e070705031616w50ca595m2e55bda049ba7aa6@mail.gmail.com> <1178241003.7436.10.camel@rosella.wigram> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <1178241003.7436.10.camel@rosella.wigram> User-Agent: Mutt/1.5.6+20040523i From: Dirk Thierbach X-Y-GMX-Trusted: 0 X-Miltered: at discorde with ID 463AEF82.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; existential:01 o'caml:01 existential:01 quantifier:01 quantifier:01 forall:01 polymorphic:01 wrote:01 wrote:01 caml-list:01 exists:03 confused:03 types:03 types:03 logic:04 On Fri, May 04, 2007 at 11:10:03AM +1000, skaller wrote: > On Thu, 2007-05-03 at 19:16 -0400, Chris King wrote: > > On 5/3/07, Christopher L Conway 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. 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) using DeMorgan's rule. - Dirk