Date: Tue, 14 Sep 1999 11:46:00 +0200
From: Francois Pottier <Francois.Pottier@inria.fr>
To: "Pierre CREGUT - FT . BD/CNET/DTL/MSV" <pierre.cregut@cnet.francetelecom.fr>,
Subject: Re: Parameterized signatures needed ?
In-Reply-To: <19990913122532.A4032@lsun605>; from Pierre CREGUT - FT . BD/CNET/DTL/MSV on Mon, Sep 13, 1999 at 12:25:32PM +0200
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/
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:25 MET