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

[Andreas Rossberg <rossberg@ps.uni-sb.de>]

Hi François,

Francois Pottier wrote:
> 
> > 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.
> 
> Oh, I see what you mean. It's a good point. But still I think I can encode
> the second functor as
> 
>       forall T. () -> T -> ...
> 
> (where (), the empty structure type, corresponds to Y and T corresponds to X)
> which, when applied to an empty structure, yields
> 
>      forall T. T -> ...
> 
> as expected (provided the ``forall'' quantifier doesn't get in the way of
> application, i.e. polymorphic instantiation and abstraction are transparent,
> as in ML).

OK, consider applying

	module type T = sig type t type u val x : t * u end

Then, in the encoding, application should yield the result type

	forall t,u. t * u -> ...

So you cannot simply `reuse' T's quantifier. Also note that in general
the quantifier(s) in question might be buried deep inside the RHS of the
arrow, even in contravariant position. (Moreover, it is not obvious to
me whether we could use implicit type application, because polymorphism
is first-class (a field or argument of functor type would be
polymorphic)).

> > functor in question would not differ from
> >
> >     functor F (X : sig module type T end) (Y : X.T) = Y
> 
> Indeed it wouldn't. But I fail to see the point; if Y's type is X.T,
> there is no difference between Y and (Y : X.T), is there? The two
> functors in question have the same type in O'Caml.

Ah, yes, you are right, I forgot about that. Actually, I see that as an
unfortunate limitation of OCaml's module typing: it has to forget some
sharing because it lacks proper singleton types (and thus loses
principality). Ideally, the type of the above variant of F should be

	functor(X : sig module type T end) -> functor(Y : X.T) -> that Y

where I write "that Y" for the singleton type inhabited by Y only (a
subtype of X.T). That functor is essentially the polymorphic identity
functor, while the other variation was a polymorphic eta-expansion of
the abstraction operator.

But in fact, what that means is that in OCaml both functors must be
represented by a type with an existential quantifier. Otherwise you
would not witness any difference between module expressions

	M

and

	F (struct module type T = ABSTRACT_SIG_OF_M end) (M)

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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