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 . The expression is a pair literal expression.
Note that by combining pair types with other pair types, we can effectively construct an product type combining types for any .
To use a pair, we must be able to extract the values inside. For that, we add the projection expressions and . When 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 . 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.
Different languages call unit different things:
- C, C++, Java has
- Python has
- Ruby has
The unit value has unit type.
Given two expressions each with their own type, we can make a pair of those types by assembling the expressions together.
We can then project the left or right part out of the pair.
The unit is a value.
A pair is a value when both constituent expressions are values.
If the left expression in a pair can step, so can the entire pair.
After the left expression in a pair is a value, we may step the right expression if possible.
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.
The helper judgments must also be updated. We can update them rather mechanically.
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 . It has 2 values, and .
Now consider the type . It has values:
Consider also the type , the product of and unit. It has values:
This is why it makes sense that the unit type is written . It is the identity of the operation written .
For the integers, we have that for all integers ,
where denotes multiplication.
Then similarly, if we write to mean "the number of values in the type ", we have that for all types ,
where denotes a product type.
And more generally, for all types , we have
where on the left, denotes a product type, and on the right, it denotes multiplication.
The proofs are once again on GitHub.
In the next post, we'll add sum types, also known as tagged unions.