Date: Fri, 17 Sep 1999 15:01:04 +0200
From: "Pierre CREGUT - FT . BD/CNET/DTL/MSV" <pierre.cregut@cnet.francetelecom.fr>
To: Xavier Leroy <Xavier.Leroy@inria.fr>
Subject: Re: Parameterized signatures needed ?
In-Reply-To: <19990916185939.24663@pauillac.inria.fr>; from Xavier Leroy on Thu, Sep 16, 1999 at 06:59:39PM +0200
> This looks less natural to me. A very limited form of "row
> polymorphism" can already be expressed with module type parameters and
> sub-structures, as in:
>
> module d(X:sig
> module type X
> module F(a:A) : sig
> module b: sig type t module M: X end
> module c:C with type t = b.t
> end
> end) : ...
>
> but it's very limited and not really practical.
>
Only because you cannot express sharing type constraints on M because X is
abstract. As it is written, you have
a module b with a type t and a contents that does not use it. You can
also write [module b : sig type t include X end]
but this does not solve the problem and it express more than you want.
All I would like to say is if there is a t used in X then it has to be
this C.t but I do not require t to exist. But the [with type] construct adds
that t must exist and must be immediately checkable.
So in fact there are two solutions :
- allow [X with type t = C.t] even if X is abstract and may not have a t
component : it means that if X is realized by a signature with
a type t then we add the constraint t = C.t
- X(t) (the solution proposed in my first post) : then the type does not need
to be named t in X(t) as we can say module type X(t) = sig type u = t end
The first solution is more limited but adds no syntax. It just requires a
special treatment of defered constraints for abstract signature when X
is given an actual value.
I am not sure it is strictly related with subtyping. It deals only with
the stamp calculus, not with the visibility of components.
-- Pierre Cregut - pierre.cregut@cnet.francetelecom.fr - +33 2 96 05 16 28 FT.CNET - DTL/MSV - 2 avenue Pierre Marzin - 22307 Lannion Cedex - France
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:25 MET