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 concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 30FA4BC69 for ; Fri, 4 May 2007 15:49:44 +0200 (CEST) Received: from mail.gmx.net (mail.gmx.net [213.165.64.20]) by concorde.inria.fr (8.13.6/8.13.6) with SMTP id l44DnhrO008375 for ; Fri, 4 May 2007 15:49:43 +0200 Received: (qmail invoked by alias); 04 May 2007 13:49:42 -0000 Received: from dialin-145-254-251-104.pools.arcor-ip.net (EHLO dialin-145-254-251-104.pools.arcor-ip.net) [145.254.251.104] by mail.gmx.net (mp006) with SMTP; 04 May 2007 15:49:42 +0200 X-Authenticated: #11134691 X-Provags-ID: V01U2FsdGVkX1+SwkJSzcqSGvjn+TjA6Y0rGPjqmZTGwpx0ZT0qil nG5p8UP/0zb/uu Received: from dirk by feanor.private-host.de with local (masqmail 0.2.20) id 1HjxvB-1RE-00 for ; Fri, 04 May 2007 15:34:05 +0200 Date: Fri, 4 May 2007 15:34:05 +0200 To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] wrapping parameterized types Message-ID: <20070504133405.GA5521@feanor> 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> <463B2364.9070102@fmf.uni-lj.si> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <463B2364.9070102@fmf.uni-lj.si> User-Agent: Mutt/1.5.6+20040523i From: Dirk Thierbach X-Y-GMX-Trusted: 0 X-Miltered: at concorde with ID 463B39F7.003 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 rossberg:01 quantifier:01 existential:01 quantifier:01 forall:01 forall:01 existential:01 ocaml:01 polymorphism:01 polymorphism:01 val:01 mylist:01 mylist:01 quantifiers:01 Andrej Bauer wrote: >rossberg@ps.uni-sb.de wrote: >> 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. Well, as classical logical formulae, they clearly are :-) Which IMHO is enough to explain the name. Notice I said "pretend", and didn't use the word "intuitionistically". >> Only the following are: >> >> (\exists a. a) -> b is equivalent to \forall a. (a -> b) But that doesn't explain why the usage in the example is called "existential". All "normal" types are forall-quantified on the outside, so this isn't really a new feature in any way. > Right, and this is in accordance with the terminology. Well, then maybe I don't understand the terminology :-) > Note that Dirk misread the precedence of operators: No, I didn't, but maybe I was to terse. The point is that records in OCaml allow rank-2 polymorphism, and one can use rank-2 polymorphism to encode existential types. The crucial point in the example is here: >>>> type 'b mylistfun = { listfun: 'a. 'a list -> 'b } [...] >>>> val app_to_mylist : 'a mylistfun -> mylist -> 'a = So, ignoring records, app_to_mylist has the type app_to_mylist : (\forall 'a. 'a list -> 'b) -> mylist -> 'b Now, "morally" this is similar to app_to_mylist : \exists 'a. ('a list -> 'b) -> mylist -> 'b as pointed out before. So one can indeed pretend that 'a is existentially qualified in this function. And this is important, because that's what makes the whole thing work ("there is a type 'a such that app_to_mylist executes, but we don't now in advance which one"). And the encoding of "real" existential types using rank-2 polymorphisms is very similar. Which is again a reason to make a connection between existential quantifiers and forall-quantifiers in negative positions, and call such an encoding "existential type". OTOH, the conversion from (\forall 'a. 'a list -> 'b) to ((\exists 'a. 'a list) -> b) really doesn't explain anything. Or maybe it does, and I don't understand it, but so far, the other explanation makes a lot more sense to me. - Dirk