Re: [Caml-list] Extensible tuple types

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

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