Re: Parameterized signatures needed ?

[Francois Pottier <Francois.Pottier@inria.fr>]

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/