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 RAA17118; Wed, 1 May 2002 17:37:38 +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 RAA17113 for caml-list@pauillac.inria.fr; Wed, 1 May 2002 17:37:38 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id MAA20530 for ; Tue, 30 Apr 2002 12:32:58 +0200 (MET DST) Received: from smtp.web.de (smtp01.web.de [194.45.170.210]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g3UAWv529906; Tue, 30 Apr 2002 12:32:57 +0200 (MET DST) Received: from [213.7.132.163] (helo=melbourne) by smtp.web.de with smtp (WEB.DE(Exim) 4.50 #15) id 172UwK-0007Ib-00; Tue, 30 Apr 2002 12:32:57 +0200 Message-ID: <000701c1f032$a69072c0$e8abfea9@melbourne> From: "Andreas Rossberg" To: Cc: References: <3CCD55BD.6DB352F5@ps.uni-sb.de> <20020429172853.A6314@pauillac.inria.fr> <3CCD794B.142F65D@ps.uni-sb.de> <20020430090732.A16788@pauillac.inria.fr> Subject: [Caml-list] Encoding "abstract" signatures Date: Tue, 30 Apr 2002 12:34:26 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit 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 Francois Pottier wrote: > > On Mon, Apr 29, 2002 at 06:48:11PM +0200, Andreas Rossberg wrote: > > > > Well, if you have a functor like > > > > F : functor(X : sig module type S module Y:S end) -> ... > > > > then it would be polymorphic in an unknown number of types. > > Perhaps our views differ. What I gathered from Jones' and Russo's > papers was that modules do not contain types. Yes. But Russo describes how you can encode ML module types in such a setting (Jones was not interested in that, AFAIR). As long as you don't have nested signatures you can recover the full expressiveness of functors (including generativity) by just using universal and existential quantification. (For other readers: the module type functor(X : sig type t val x : t end) -> sig type u val y : u end can be encoded as forall t. {x:t} -> exists u. {y:u} Well, with OCaml's applicative functors you had to lift the existential quantifier, but you get the idea.) What I was saying is that this encoding does not easily extend to the full OCaml module system, because abstract signatures pose a problem: the number of quantifiers you have to generate in the encoding is not fixed. I reckonned some more complex kind system and kind polymorphism might enable you to recover their expressiveness. But I am not at all sure (see below). > So, the module type > S cannot be a component of X; rather, the type of the functor F > will be universally quantified over S. This leads me to something > like: > > F : forall S. functor (X : S) -> ... > > where the distinction between X and Y is eliminated, because it > becomes superfluous. In fact, the `functor' syntax and the name > X are just sugar, since a functor is a function. So I would really > write > > F : forall S. S -> ... > > > The application > > > > F (struct module type S = sig type t type u val x : t end > > module Y = struct type t = int > > type u = bool > > val x = 7 end > > end) > > > > corresponds to something like > > > > F {t:*,u:*} {x:int} {t=int,u=bool} {Y={x=7}} > > I would simply apply > > F { x : int } { x = 7 } > > or, perhaps (if abstraction is desired) > > F (exists t,u.{ x : t }) (pack { x = 7 } as exists t,u.{ x : t }) > > So, in this example, we seem to need neither higher kinds nor > kind polymorphism. But perhaps my encoding doesn't have the > features you'd wish? 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) (Oops, I got the kind of S wrong in my previous posting). But as I said I did not think about it much, so I have no idea whether this really scales. In particular, when you nest signatures you might hit the same problem of an unfixed number of quantifiers, but for kinds. In fact, I am pretty certain it does not fly, because nested signatures essentially give you Type:Type, i.e. you'd most likely need an infinite hierarchy of universes... - 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