11.6 Pairs

< Free Open Study >

Most programming languages provide a variety of ways of building compound data structures. The simplest of these is pairs, or more generally tuples, of values. We treat pairs in this section, then do the more general cases of tuples and labeled records in §11.7 and §11.8.^[4]

The formalization of pairs is almost too simple to be worth discussing-by this point in the book, it should be about as easy to read the rules in Figure 11-5 as to wade through a description in English conveying the same information. However, let's look briefly at the various parts of the definition to emphasize the common pattern.

Figure 11-5: Pairs

Adding pairs to the simply typed lambda-calculus involves adding two new forms of term-pairing, written {t₁,t₂}, and projection, written t.1 for the first projection from t and t.2 for the second projection-plus one new type constructor, T₁ × T₂, called the product (or sometimes the cartesian product) of T₁ and T₂. Pairs are written with curly braces^[5] to emphasize the connection to records in the §11.8.

For evaluation, we need several new rules specifying how pairs and projection behave. E-PAIRBETA1 and E-PAIRBETA2 specify that, when a fully evaluated pair meets a first or second projection, the result is the appropriate component. E-PROJ1 and E-PROJ2 allow reduction to proceed under projections, when the term being projected from has not yet been fully evaluated. E-PAIR1 and E-PAIR2 evaluate the parts of pairs: first the left part, and then-when a value appears on the left-the right part.

The ordering arising from the use of the metavariables v and t in these rules enforces a left-to-right evaluation strategy for pairs. For example, the compound term

   {pred 4, if true then false else false}.1

evaluates (only) as follows:

            {pred 4, if true then false else false}.1    →  {3, if true then false else false}.1    →  {3, false}.1    →  3

We also need to add a new clause to the definition of values, specifying that {v₁,v₂} is a value. The fact that the components of a pair value must themselves be values ensures that a pair passed as an argument to a function will be fully evaluated before the function body starts executing. For example:

            (λx:Nat × Nat. x.2) {pred 4, pred 5}    →  (λx:Nat × Nat. x.2) {3, pred 5}    →  (λx:Nat × Nat. x.2) {3,4}    →  {3,4}.2    →  4

The typing rules for pairs and projections are straightforward. The introduction rule, T-PAIR, says that {t₁,t₂} has type T₁ × T₂ if t₁ has type T₁ and t₂ has type T₂. Conversely, the elimination rules T-PROJ1 and T-PROJ2 tell us that, if t₁ has a product type T₁₁ × T₁₂ (i.e., if it will evaluate to a pair), then the types of the projections from this pair are T₁₁ and T₁₂.

^[4]The fullsimple implementation does not actually provide the pairing syntax described here, since tuples are more general anyway.

^[5]The curly brace notation is a little unfortunate for pairs and tuples, since it suggests the standard mathematical notation for sets. It is more common, both in popular languages like ML and in the research literature, to enclose pairs and tuples in parentheses. Other notations such as square or angle brackets are also used.

< Free Open Study >