Version française
Home     About     Download     Resources     Contact us    
Browse thread
Parameterized signatures needed ?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ 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