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

[Francois Pottier <francois.pottier@inria.fr>]

Andreas,

On Tue, Apr 30, 2002 at 12:34:26PM +0200, Andreas Rossberg 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).

It seems to me that it is simpler to suppress the pack operation,
i.e. to return Y instead of (pack Y as ...). Then, instead of
quantifying separately over S and ts, you only need to quantify
over S(ts), that is, T, as follows:

  val F : forall T. T -> T

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. But it
seems to offer a simple understanding of the above O'Caml specification.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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