Please refer this link from page 81 to 85.

# From Unit to Finite Product

**Binary product** of two types consists of **ordered pairs** of values, one from each type in order specified.

**Nullary product** or **unit** type consists solely of unique “null tuple” of no value.

Associated elimination form of binary product is **projection**, which select first/second of the pair. No associated elimination form exists for nullary product.

Product types admits both **lazy** and **eager** dynamics:

- In
**lazy dynamics**, a pair is a value without regard to whether its components are values, they are not evaluated until (if ever) they are accessed and used in another computation. - In
**eager dynamics**, a pair is a value only if its components are values; they are evaluated when the pair is created.

**Finite product** with form $\langle \tau_i \rangle_{i\in I}$ is a more general form, indexed by a finite set of **indices** $I$.

The components are accessed by **$I$-indexed projection** operations, generalizing the binary case. Similar to binary product, finite products admit both an eager and a lazy interpretation.