11.7 Tuples

---

11.7 Tuples

It is easy to generalize the binary products of the previous section to n-ary products, often called tuples. For example, {1,2,true} is a 3-tuple containing two numbers and a boolean. Its type is written {Nat,Nat,Bool}.

The only cost of this generalization is that, to formalize the system, we need to invent notations for uniformly describing structures of arbitrary arity; such notations are always a bit problematic, as there is some inevitable tension between rigor and readability. We write {t_i ^iÎ1..n} for a tuple of n terms, t₁ through t_n, and {T_i^iÎ1..n} for its type. Note that n here is allowed to be 0; in this case, the range 1..n is empty and {t_i^iÎ1..n} is {}, the empty tuple. Also, note the difference between a bare value like 5 and a one-element tuple like {5}: the only operation we may legally perform on the latter is projecting its first component.

Figure 11-6 formalizes tuples. The definition is similar to the definition of products (Figure 11-5), except that each rule for pairing has been generalized to the n-ary case, and each pair of rules for first and second projections has become a single rule for an arbitrary projection from a tuple. The only rule that deserves special comment is E-TUPLE, which combines and generalizes the rules E-PAIR1 and E-PAIR2 from Figure 11-5. In English, it says that, if we have a tuple in which all the fields to the left of field j have already been reduced to values, then that field can be evaluated one step, from t_j to t′_j. Again, the use of metavariables enforces a left-to-right evaluation strategy.

Figure 11-6: Tuples

---