Browse thread
Parameterized signatures needed ?
-
Pierre CREGUT - FT . BD/CNET/DTL/MSV
-
Francois Pottier
-
Xavier Leroy
- Pierre CREGUT - FT . BD/CNET/DTL/MSV
-
Xavier Leroy
-
Francois Pottier
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Pierre CREGUT - FT . BD/CNET/DTL/MSV <pierre.cregut@c...> |
| Subject: | Re: Parameterized signatures needed ? |
> 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