From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id QAA30863 for caml-redistribution; Tue, 14 Sep 1999 16:46:28 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA17908 for ; Tue, 14 Sep 1999 11:46:03 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id LAA10994; Tue, 14 Sep 1999 11:46:00 +0200 (MET DST) Received: (from fpottier@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA20546; Tue, 14 Sep 1999 11:46:00 +0200 (MET DST) Message-ID: <19990914114600.57679@pauillac.inria.fr> Date: Tue, 14 Sep 1999 11:46:00 +0200 From: Francois Pottier To: "Pierre CREGUT - FT . BD/CNET/DTL/MSV" , caml-list@inria.fr Cc: =?iso-8859-1?Q?Fran=E7ois_Pottier?= Subject: Re: Parameterized signatures needed ? References: <19990913122532.A4032@lsun605> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Mailer: Mutt 0.89.1 In-Reply-To: <19990913122532.A4032@lsun605>; from Pierre CREGUT - FT . BD/CNET/DTL/MSV on Mon, Sep 13, 1999 at 12:25:32PM +0200 Sender: weis 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/