Re: [Camllist] Polymorphic Variants and Number Parameterized Typ es
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20020501 (15:37) 
From:  Andreas Rossberg <AndreasRossberg@w...> 
Subject:  [Camllist] Encoding "abstract" signatures 
Francois Pottier <francois.pottier@inria.fr> 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 nonapplicative 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 camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners