[Caml-list] Encoding "abstract" signatures

["Andreas Rossberg" <AndreasRossberg@web.de>]

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 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