Parameterized signatures needed ?

From: Pierre CREGUT - FT . BD/CNET/DTL/MSV (pierre.cregut@cnet.francetelecom.fr)
Date: Mon Sep 13 1999 - 12:25:32 MET DST

Date: Mon, 13 Sep 1999 12:25:32 +0200
From: "Pierre CREGUT - FT . BD/CNET/DTL/MSV" <pierre.cregut@cnet.francetelecom.fr>
To: caml-list@inria.fr
Subject: Parameterized signatures needed ?

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

This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:25 MET