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_NEUTRAL 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 BF1B2BC69 for ; Fri, 4 May 2007 17:58:25 +0200 (CEST) Received: from ik-out-1112.google.com (ik-out-1112.google.com [66.249.90.182]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l44FwPEm020811 for ; Fri, 4 May 2007 17:58:25 +0200 Received: by ik-out-1112.google.com with SMTP id c29so860040ika for ; Fri, 04 May 2007 08:58:25 -0700 (PDT) DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=LZ9HBaPwVBqP+881C5uPypNzq0emoKl/SHtoGMTZVpi7Ap18ZEy2ngm/HGSeMddcYkjXAc68f6CUclqfkJUd6kXf8MpnMO4DmxvtYH0LmfJ8JutiTjH/SDwAlANcRsLgNIjmqSJSF5yqEwb5+25iyLXtrb78Wc10okpyFqzoOzs= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=UglRscU+A8m6axeDOmJ7a0VxdawL4R6a8ESvLR4GFNY/MBm/BLuesOXhnaaDbOaQj47+9D8uR2aPdPUQs6q3mqpKPRaPUVi4ZzybvT8VcLzQ52PMW4PwjY2oobTlgerTjyxb+SLqKALGarKvp7GPZZea/8uu6yE2OKczhF1gC+0= Received: by 10.78.160.4 with SMTP id i4mr1638446hue.1178294304674; Fri, 04 May 2007 08:58:24 -0700 (PDT) Received: by 10.78.156.19 with HTTP; Fri, 4 May 2007 08:58:24 -0700 (PDT) Message-ID: <4a051d930705040858m6a0f1c5cpf134c7e55bd3ce7b@mail.gmail.com> Date: Fri, 4 May 2007 11:58:24 -0400 From: "Christopher L Conway" Sender: christopherleeconway@gmail.com To: "Dirk Thierbach" Subject: Re: [Caml-list] wrapping parameterized types Cc: caml-list@yquem.inria.fr In-Reply-To: <20070504133405.GA5521@feanor> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline 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> <20070504133405.GA5521@feanor> X-Google-Sender-Auth: e2ee5a7a6ba1573a X-Miltered: at discorde with ID 463B5821.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; semantics:01 existential:01 pointers:01 andrej:01 rossberg:01 quantifier:01 existential:01 quantifier:01 forall:01 forall:01 ocaml:01 polymorphism:01 polymorphism:01 val:01 mylist:01 Can anyone point me to where the semantics of these, um, existential type declarations are defined? This topic is mentioned only scantly in the manual. I'd also be interested in pointers to the underlying type theory. Thanks, Chris On 5/4/07, Dirk Thierbach wrote: > 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 > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > >