From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA29117; Thu, 2 May 2002 09:34:37 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 JAA29113 for ; Thu, 2 May 2002 09:34:36 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g427YaD06874 for ; Thu, 2 May 2002 09:34:36 +0200 (MET DST) Received: (from fpottier@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA29109 for caml-list@inria.fr; Thu, 2 May 2002 09:34:35 +0200 (MET DST) Date: Thu, 2 May 2002 09:34:35 +0200 From: Francois Pottier To: caml-list@inria.fr Subject: Re: [Caml-list] Extensible tuple types Message-ID: <20020502093435.C27687@pauillac.inria.fr> Reply-To: Francois.Pottier@inria.fr References: <4.1.20020430114454.009caaf0@127.0.0.1> <6ECF4649-5C48-11D6-AC27-0003934491C2@lasmea.univ-bpclermont.fr> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Mailer: Mutt 1.0i In-Reply-To: <6ECF4649-5C48-11D6-AC27-0003934491C2@lasmea.univ-bpclermont.fr>; from jserot@lasmea.univ-bpclermont.fr on Tue, Apr 30, 2002 at 04:42:01PM +0200 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Tue, Apr 30, 2002 at 04:42:01PM +0200, Jocelyn Sérot wrote: > > Sorry to jump in the middle of this discussion, but your last remark on > "extensible > n-tuples" drew my attention (i use to need this kind of thing in a > completely different > context). Can you provide references on these extensions of ML type > systems ? Tuples can be viewed as records whose field labels are integers, rather than names. (In particular, this means that tuple fields do not commute, contrary to record fields.) Records can be typed in a flexible way using rows; see Didier Rémy's papers, for instance ``Type Inference for Records in a Natural Extension of ML''. In the case of tuples, it's possible to use a variant of rows -- I'll call them ``sequences'' -- to describe an infinite sequence of types. Their syntax is given by s ::= 's | t; s | all(t) where t stands for a type. 's is a ``sequence variable''. t; s is a sequence whose first component is t and whose other components are listed by s. all(t) is the sequence where every component is t. As in the case of records, we introduce type constructors Absent (0-ary) and Present (unary) to tell which components are present/absent in a tuple. We also introduce a ``tuple'' type constructor, whose argument is a sequence; that is, (s) is the type of tuples whose contents is described by the sequence s. Then, you can give types to the basic operations on tuples, as follows. The empty tuple has type (all(Absent)), for it has no components. The operation which accepts any tuple, of length at least k, and returns its k-th component, has type forall 'a_1, ..., 'a_k, 's. ('a_1; ...; 'a_{k-1}; Present('a_k); 's) -> 'a_k The operation which accepts any tuple and adds a new component in front of it has type forall 'a, 's. 'a -> ('s) -> (Present('a); 's) Now, for the whole thing to work out in an extension of ML, you need to make sure that unification of sequences is decidable. This seems straightforward; the cases of interest are decomposition: t1;s1 = t2; s2 reduces to t1 = t2 and s1 = s2 and expansion of uniform sequences: all(t1) = t2; s2 reduces to t1 = t2 and all(t1) = s2 One slightly inelegant aspect of this approach is the fact that there are empty types, such as (Absent;Present(int);all(Absent)). It's impossible, given the operations above, to build a value of this type. However, I can imagine situations where such types could actually be of some use, e.g. if you add coercions of type forall 'a_1, ..., 'a_k, 's. ('a_1; ...; 'a_{k-1}; 'a_k; 's) -> ('a_1; ...; 'a_{k-1}; Absent; 's) then you gain the ability to forbid access to certain fields within a tuple. After writing this far, I realize that it's possible to simplify further by considering *finite* sequences and replacing the form all(t) with a simple ``nil'' sequence constructor, representing an empty sequence. Then, you can suppress Absent and Present, and you no longer have ``tuples with holes'' as above. My original presentation was biased because I started from rows, which represent infinite collections. These ``sequences'' haven't been widely used in the literature; the only instance I know of is the use of finite sequences to describe the structure of stacks in Morrisett et al's STAL (stack-based assembly language). In their setting, the key point is the ability to universally quantify over sequence variables, making all but a portion of the stack abstract. I hope this helps, -- François Pottier Francois.Pottier@inria.fr http://pauillac.inria.fr/~fpottier/ ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners