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

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

On Wed, May 01, 2002 at 03:19:29PM +0200, Andreas Rossberg 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).

> 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

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.

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