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
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
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 you 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
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
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,
Now consider the type . It has 4 values:
Consider also the type , the product of
and unit. Like , it only has 2 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
The proofs are once again on GitHub.
In the next post, we'll add sum types, also known as tagged unions.