From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA18164; Wed, 1 May 2002 17:46:06 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA18159 for caml-list@pauillac.inria.fr; Wed, 1 May 2002 17:46:05 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id PAA14021 for ; Wed, 1 May 2002 15:17:48 +0200 (MET DST) Received: from smtp.web.de (smtp02.web.de [217.72.192.151]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g41DHlD14094; Wed, 1 May 2002 15:17:47 +0200 (MET DST) Received: from [213.7.133.204] (helo=melbourne) by smtp.web.de with smtp (WEB.DE(Exim) 4.52 #1) id 172tzJ-0002Po-00; Wed, 01 May 2002 15:17:42 +0200 Message-ID: <000801c1f112$d4c266e0$e8abfea9@melbourne> From: "Andreas Rossberg" To: , References: <3CCD55BD.6DB352F5@ps.uni-sb.de> <20020429172853.A6314@pauillac.inria.fr> <3CCD794B.142F65D@ps.uni-sb.de> <20020430090732.A16788@pauillac.inria.fr> <000701c1f032$a69072c0$e8abfea9@melbourne> <20020430171846.A28745@pauillac.inria.fr> Subject: Re: [Caml-list] Re: Encoding "abstract" signatures Date: Wed, 1 May 2002 15:19:29 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 8bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 6.00.2600.0000 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2600.0000 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk François, Francois Pottier wrote: > > > How do you express > > > > functor F (X : sig module type T end) (Y : X.T) = (Y : X.T) > > > > without parameterizing over the set of existentially quantified variables > > somehow? I had in mind something like (again assuming non-applicative > > functors, because they are much simpler): > > > > LAMBDA k. Lambda S:(k->*). Lambda ts:k. lambda Y:S(ts). > > pack Y as exists ts:k.S(ts) > > You make the functor F polymorphic in the number of type components > defined by the signature S. As far as I understand, this is made > necessary by the desire to hide these types in the functor's result > (i.e. the pack operation). This is just one reason. More generally, it's the need for a coherent encoding in the higher-order setting we face. If we say that type functor(X : sig type t val x : t end) -> ... maps to something like forall t. t -> ... then consequently functor(Y : sig module type T end) -> ... -> functor(X : Y.T) -> ... must map to some type that yields the above as the result of some sequence of applications. We need to be polymorphic in the form of the quantification to achieve that. So even by ignoring type abstraction you cannot avoid the problem. But if you replace "type" by "module type" in the above argument signature you see why there actually cannot be an encoding with the desired properties: the encoding of the latter type also had to contain quantifiers for all potential *kind arguments* induced by applying an argument with nested signatures. There is no fixed point for the level of abstractions we had to do, unless we allowed for dependent types at some level. > I must say I don't know exactly what is lost with this simplification; > is there a loss of abstraction? The answer isn't obvious to me. Well, besides the aforementioned problems, you don't represent type abstraction at all (which, I would argue, is a central feature) - the functor in question would not differ from functor F (X : sig module type T end) (Y : X.T) = Y Or was your question about abstraction in some other sense? - Andreas ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners