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.
A product type that combines two types is called “pair” and denoted with τ1×τ2. The expression ⟨e1,e2⟩ is a pair literal expression.
Note that by combining pair types with other pair types, we can effectively construct an product type combining n types for any n>2.
To use a pair, we must be able to extract the values inside. For that, we add the projection expressions e⋅L and e⋅R. When e 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. There is just 1 value of this type, also often called “unit”, and it is written ⟨⟩.
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.
A pair is a value when both constituent expressions are values.
⟨e1,e2⟩vale1vale2val
If the left expression in a pair can step, so can the entire pair.
⟨e1,e2⟩↦⟨e1′,e2⟩e1↦e1′
After the left expression in a pair is a value, we may step the right expression if possible.
⟨e1,e2⟩↦⟨e1,e2′⟩e1vale2↦e2′
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.