You know the sum type terms (inl, inr, and scase) and their intended meaning.
You can derive and implement typing rules for sums.
You can implement call-by-value reduction rules for injections and sum case matching.
Introduction
Sum types, as you already know from chapter 1 are useful for lots of situations.
For example, when we want a variable to hold one of many different types, we could express that using sum types.
The dynamics of sum types are straight-forward.
We reduce injection terms until they are values.
Sum case matching reduces the scrutinee and once it’s an injection, it reduces to the corresponding branch.
The types in the injection are not used after type checking so we ignore them (by blanketing them with underscores) during the reduction rules.
The rules should seem familiar, because they are very closely related to natural numbers (compare with CaseNat for example).
Typing rules for sums are as follows.
Again, the CaseSum typing rule reminds us of the CaseNat rule.