Parameterized signatures needed ?

Parameterized signatures needed ?

[Pierre CREGUT - FT . BD/CNET/DTL/MSV]

Here is a small but complex puzzle with modules. I will use lowercase names for
modules and uppercase for signatures to simplify.

I have a process creating from a module a:A a module with two sub-modules
b:B and c:C containing both a same type t

  module F(a:A) : sig module b:B module c:C with type t = b.t end

>From a and c I build other components. From b, I can also build other
things, they must be related later with the type t given by c.

So I want to build a functor d describing an a, building a c and using these,
b is also given back but not used inside d.
So A and C are fixed and well known but B is not and in fact there are
different kind of F giving different signature B.

  module d(X:sig
		module type B 
		module F(a:A) : sig 
		    module b:B 
		    module c:C with type t = b.t 
		  end
	      end) : 
    sig 
      type t
      module b : B with type t = t
      val ... : ... t ...
    end =
  struct
    module a = struct ... end
    module bc = F(a)
    type t = bc.b.t
    module b = bc.b and c = bc.c
  end

But I cannot speak of t because it is not a component of the abstract
signature B.

I could try 

   module b : B' where B' = sig type t include B end

but I will never relate a t in B and the specified t this way.

I could try in the specification of the functor argument

   module type B = sig type t end

but then B is really limited to what I gave.

So we lack something to parameterize such abstract signature : the "with type"
construct is too external.
May be we should dig out parameterized signatures :

  module type B(type t) = sig .... end

Its interface would be :

  module type B(type t)

and it would be used like this :

  module d(X:sig
		module type B (type t)
		module F(a:A) : sig module c:C module b: B(type t = c.t) end
	      end) : 
    sig 
      type t
      module b : B(t)
      val ... : ... t ...
    end

My questions are :
- is there another way to build d achieving the same result but with standard
  Objective Caml syntax ?
- are there been any work recently on parameterized signatures dealing with
  those problems ?

PS 1> a,b,c,d.. it looks like a stupid school example but i have real code 
behind it. b and c cannot be separated because the internal structure of the
abstract types provided by c depends on what you expect from b.

PS 2> parameterized signature existed in the original proposal for a module
system, but D. MacQueen showed that it was impossible to think of all the
possible sharing you wanted to express before hand. I am not considering
replacing sharing constraints with parameterized signatures but using both.

PS 3> parameterized signatures built this way are still rather abstract as
long as you do not try to use interface specifying their contents. 
I don't think there is any problem to type-check them and we are not threatened
by Lilibridge & Harper counter-examples.

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

Re: Parameterized signatures needed ?

[Francois Pottier]

Hello Pierre,

If my understanding of your problem is correct, you are trying to
write a functor which does two things at once:

 * it requires its argument to have some field t, and makes use
   of it;

 * it wants to return its argument, unchanged, as (part of) its
   result.

A similar problem appears in the expression language, rather than a in
the module language, if we replace modules with records, and functors
with functions. Imagine I write a function along the following lines:

  let f r =
    < read r.t, then return r >
    
It is desirable to have the ability of applying f to any record which
at least one field named t, regardless of its other fields. But which
type can we give to f? I know of two possible answers.

One solution is to define a subtyping relationship on records, so that
records with more fields are subtypes of records with fewer
fields. Then, the type of f would be

  'a -> 'b where 'a < { t : 'b }

In other words, for all 'a, 'b such that 'a is a subtype of { t : 'b },
f has type 'a -> 'b. This is a satisfactory type, because it requires
the argument type to carry a field named t, but returns it unchanged,
even if it contains other, unknown fields. However, this type involves
an explicit subtyping constraint.

The other solution is to use row variables, as is currently done in
O'Caml to deal with objects. Then, f would have type

  { t : 'b; 'rho } -> { t : 'b; 'rho }

In other words, the argument is required to be a record with at least
one field t of type 'b. 'rho is bound to the types of the other,
unknown fields. The argument is then returned unchanged. This
type does not involve subtyping, but requires performing unification
which row variables (which O'Caml already does).

I have discussed your problem at the level of the expression language,
because I think it is well-understood in this setting. What you have
done is uncover the same problem at the level of the module language.
The module language is less powerful than the expression language, as
far as typing is concerned. Indeed, it does have a notion of
``sub-signatures'', which resembles subtyping on record types, but
it does not allow explicit sub-signature constraints. In view of the
solutions which exist at the level of expressions, one may suggest
extending O'Caml with

 * either explicit sub-signature constraints, e.g.

   module d(X:sig
		 module type B < sig type t end
		 module F(a:A) : sig
		     module b:B
		     module c:C with type t = b.t
		   end
	       end) : ...

 * or row variables in signatures, although I am not sure which form
   this would take.

I hope I am making sense here. Comments, anyone?

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/

Re: Parameterized signatures needed ?

[Xavier Leroy]

> In view of the
> solutions which exist at the level of expressions, one may suggest
> extending O'Caml with
> 
>  * either explicit sub-signature constraints, e.g.
> 
>    module d(X:sig
> 		 module type B < sig type t end
> 		 module F(a:A) : sig
> 		     module b:B
> 		     module c:C with type t = b.t
> 		   end
> 	       end) : ...

It looks like this would fit quite naturally within the OCaml module
system.  After all, the module language is explicitely typed, has
subtyping and a form of parametric polymorphism; bounded polymorphism
is the next step.  (I haven't checked the details, though.)

>  * or row variables in signatures, although I am not sure which form
>    this would take.

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.

- Xavier Leroy

Re: Parameterized signatures needed ?

[Pierre CREGUT - FT . BD/CNET/DTL/MSV]

> 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