Re: [Caml-list] Re: Encoding "abstract" signatures

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

François,

Francois Pottier <francois.pottier@inria.fr> 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