Pairs and The Product Type
Learning Objectives
- You know the syntax, typing rules, and call-by-value dynamics for pairs and projections.
- You can implement pair typing and reduction rules in the Rust STLC evaluator.
- You know the Unit type and its single canonical value
unit.
Introduction
Pairs are a very useful data type for bundling together two pieces of data. The type of a pair is called the product type, or the product of types and , and is denoted or sometimes .
The type of products can be formed given any two types. Its formation rule is as follows.
Notice that the projection terms, like the ncase term from the previous chapter, are not functions in the lambda calculus sense.
Even if they were, simple types are not enough to express their types.
In a polymorphic language, the projections would have the types
The dynamics of pairs and projections are straight-forward. We reduce inner terms inside pairs so that they have a consistent canonical form. A pair is a value only if and only if both subterms are values (i.e. canonical forms).
Reducing the terms inside fst and snd lets them eventually become pairs so that FstPair and SndPair can be applied.
Typing rules for pairs and projections are not hard to guess:
- A pair of terms and has type .
- The first and second projections from a term have type and respectively.
Unit/Singleton Type
The singleton type with only one element is called Unit.
The element in Rust is written (), but we will just call it unit.
Implementing the unit type is left as an exercise for the reader. In the next chapter, we implement sum types.