Define a PL: products

Translations: English • 日本語

In the previous post, we added functions to Hatsugen.

In this post, we’ll add product types. These are often called “structs”, “records”, or “tuples” in real programming languages.

A product type is a combination of multiple types. For instance, if we want to return multiple values from a function, we can have the function’s return type be a product type.

Syntax

A product type that combines two types is called “pair” and denoted with τ1×τ2\tau_1 \times \tau_2. The expression ⟨e1,e2⟩\langle e_1, e_2 \rangle is a pair literal expression.

Note that by combining pair types with other pair types, we can effectively construct an product type combining nn types for any n>2n > 2.

To use a pair, we must be able to extract the values inside. For that, we add the projection expressions e⋅Le \cdot \mathsf{L} and e⋅Re \cdot \mathsf{R}. When ee is a pair, these projections extract the left and right value out of the pair respectively.

We will also introduce a product type that combines no other types, called “unit” and denoted with 1\mathsf{1}. There is just 1 value of this type, also often called “unit”, and it is written ⟨⟩\langle \rangle.

Because the unit type has only one value, it may not seem very useful. However, it can be useful when we want to return “nothing” from a function.

For instance, in most programming languages, functions can perform side effects. Side effects are anything the function does other than return a value, like modify files or access the Internet.

In fact, sometimes functions are only useful because of the side effects they perform, and they don’t actually need to return anything useful. In these cases, it is convenient to have these functions return unit.

Different languages call unit different things:

τ::= …∣ 1∣ τ1×τ2e::= …∣ ⟨⟩∣ ⟨e1,e2⟩∣ e⋅L∣ e⋅R \begin{aligned} \tau ::= \ & \dots \\ | \ & \mathsf{1} \\ | \ & \tau_1 \times \tau_2 \\ \\ e ::= \ & \dots \\ | \ & \langle \rangle \\ | \ & \langle e_1, e_2 \rangle \\ | \ & e \cdot \mathsf{L} \\ | \ & e \cdot \mathsf{R} \end{aligned}

Statics

The unit value has unit type.

Γ⊢⟨⟩:1 \frac {} {\Gamma \vdash \langle \rangle: \mathsf{1}}

Given two expressions each with their own type, we can make a pair of those types by assembling the expressions together.

Γ⊢e1:τ1Γ⊢e2:τ2Γ⊢⟨e1,e2⟩:τ1×τ2 \frac { \Gamma \vdash e_1: \tau_1 \hspace{1em} \Gamma \vdash e_2: \tau_2 } {\Gamma \vdash \langle e_1, e_2 \rangle: \tau_1 \times \tau_2}

We can then project the left or right part out of the pair.

Γ⊢e:τ1×τ2Γ⊢e⋅L:τ1 \frac {\Gamma \vdash e: \tau_1 \times \tau_2} {\Gamma \vdash e \cdot \mathsf{L}: \tau_1} Γ⊢e:τ1×τ2Γ⊢e⋅R:τ2 \frac {\Gamma \vdash e: \tau_1 \times \tau_2} {\Gamma \vdash e \cdot \mathsf{R}: \tau_2}

Dynamics

The unit is a value.

⟨⟩ val \frac {} {\langle \rangle \ \mathsf{val}}

A pair is a value when both constituent expressions are values.

e1 vale2 val⟨e1,e2⟩ val \frac { e_1 \ \mathsf{val} \hspace{1em} e_2 \ \mathsf{val} } {\langle e_1, e_2 \rangle \ \mathsf{val}}

If the left expression in a pair can step, so can the entire pair.

e1↦e1′⟨e1,e2⟩↦⟨e1′,e2⟩ \frac {e_1 \mapsto e_1'} {\langle e_1, e_2 \rangle \mapsto \langle e_1', e_2 \rangle}

After the left expression in a pair is a value, we may step the right expression if possible.

e1 vale2↦e2′⟨e1,e2⟩↦⟨e1,e2′⟩ \frac { e_1 \ \mathsf{val} \hspace{1em} e_2 \mapsto e_2' } {\langle e_1, e_2 \rangle \mapsto \langle e_1, e_2' \rangle}

For the projections, we must first step the pair to a value. Then, once it is a value, it will be a pair literal, and we may step to either the left or right value in the pair.

e↦e′e⋅L↦e′⋅L \frac {e \mapsto e'} {e \cdot \mathsf{L} \mapsto e' \cdot \mathsf{L}} ⟨e1,e2⟩ val⟨e1,e2⟩⋅L↦e1 \frac {\langle e_1, e_2 \rangle \ \mathsf{val}} {\langle e_1, e_2 \rangle \cdot \mathsf{L} \mapsto e_1} e↦e′e⋅R↦e′⋅R \frac {e \mapsto e'} {e \cdot \mathsf{R} \mapsto e' \cdot \mathsf{R}} ⟨e1,e2⟩ val⟨e1,e2⟩⋅R↦e2 \frac {\langle e_1, e_2 \rangle \ \mathsf{val}} {\langle e_1, e_2 \rangle \cdot \mathsf{R} \mapsto e_2}

Helpers

The helper judgments must also be updated. We can update them rather mechanically.

Substitution

[x↦e]⟨⟩=⟨⟩ \frac {} {[x \mapsto e] \langle \rangle = \langle \rangle} [x↦e]e1=e1′[x↦e]e2=e2′[x↦e]⟨e1,e2⟩=⟨e1′,e2′⟩ \frac { [x \mapsto e] e_1 = e_1' \hspace{1em} [x \mapsto e] e_2 = e_2' } {[x \mapsto e] \langle e_1, e_2 \rangle = \langle e_1', e_2' \rangle} [x↦e]e1=e1′[x↦e]e1⋅L=e1′⋅L \frac {[x \mapsto e] e_1 = e_1'} {[x \mapsto e] e_1 \cdot \mathsf{L} = e_1' \cdot \mathsf{L}} [x↦e]e1=e1′[x↦e]e1⋅R=e1′⋅R \frac {[x \mapsto e] e_1 = e_1'} {[x \mapsto e] e_1 \cdot \mathsf{R} = e_1' \cdot \mathsf{R}}

Free variables

fv(⟨⟩)=∅ \frac {} {\mathsf{fv}(\langle \rangle) = \emptyset} fv(e1)=s1fv(e2)=s2fv(⟨e1,e2⟩)=s1∪s2 \frac { \mathsf{fv}(e_1) = s_1 \hspace{1em} \mathsf{fv}(e_2) = s_2 } {\mathsf{fv}(\langle e_1, e_2 \rangle) = s_1 \cup s_2} fv(e)=sfv(e⋅L)=s \frac {\mathsf{fv}(e) = s} {\mathsf{fv}(e \cdot \mathsf{L}) = s} fv(e)=sfv(e⋅R)=s \frac {\mathsf{fv}(e) = s} {\mathsf{fv}(e \cdot \mathsf{R}) = s}

Etymology

Before we conclude, let us consider the etymology of “product type”.

Product types are so named because the number of values in a product type is the product of the number of values in the constituent types.

For instance, consider the type Bool\mathsf{Bool}. It has 2 values, true\mathsf{true} and false\mathsf{false}.

Now consider the type Bool×Bool\mathsf{Bool} \times \mathsf{Bool}. It has 2×2=42 \times 2 = 4 values:

  1. ⟨true,true⟩\langle \mathsf{true}, \mathsf{true} \rangle
  2. ⟨true,false⟩\langle \mathsf{true}, \mathsf{false} \rangle
  3. ⟨false,true⟩\langle \mathsf{false}, \mathsf{true} \rangle
  4. ⟨false,false⟩\langle \mathsf{false}, \mathsf{false} \rangle

Consider also the type Bool×1\mathsf{Bool} \times \mathsf{1}, the product of Bool\mathsf{Bool} and unit. It has 2×1=22 \times 1 = 2 values:

  1. ⟨true,⟨⟩⟩\langle \mathsf{true}, \langle \rangle \rangle
  2. ⟨false,⟨⟩⟩\langle \mathsf{false}, \langle \rangle \rangle

This is why it makes sense that the unit type is written 1\mathsf{1}. It is the identity of the operation written ×\times.

For the integers, we have that for all integers aa,

a×1=aa \times 1 = a

where ×\times denotes multiplication.

Then similarly, if we write ∣τ∣|\tau| to mean “the number of values in the type τ\tau”, we have that for all types τ\tau,

∣τ×1∣=∣τ∣|\tau \times \mathsf{1}| = |\tau|

where ×\times denotes a product type.

And more generally, for all types τ1,τ2\tau_1, \tau_2, we have

∣τ1×τ2∣=∣τ1∣×∣τ2∣|\tau_1 \times \tau_2| = |\tau_1| \times |\tau_2|

where on the left, ×\times denotes a product type, and on the right, it denotes multiplication.

Conclusion

The proofs are once again on GitHub.

In the next post, we’ll add sum types, also known as tagged unions.