Part 3 - Product and Sum types

Product Types

Product types, typically $\tau_1 \times \tau_2$, or colloquially a tuple, are an obviously useful construct, so it'd be nice if we can show some notion of type-safety for product types.

We give tuples as such:

$$ \text{Typ } \tau ::= \texttt{unit} | \texttt{prod}(\tau_1; \tau_2) $$

$$ \text{Exp } e ::= \texttt{triv} | \texttt{pair}(e_1;e_2) | \texttt{pr}[l](e) | \texttt{pr}[r](e) $$

The $\texttt{pair}$ expression is known as the introduction form, and the $\texttt{pr}$ expressions the elimination form. The terms "constructor" and "destructor" apply here as well.

We won't reproduce the statics nor dynamics for product types, but we'll note that 10.2g and h require that despite only the left and right projections being used, we still need "the other side" to be valid. This is weird considering tuples of invalid types "on the other side" seem to work just fine in language practice. This seems to be something about divering computations? (if-then-else)

We show preservation and progress on the pair type:

Preservation: If $e: \tau$ and $e \rightarrow e'$ then $e': \tau$

• Case 1: $e.l: \tau \Rightarrow e.l \rightarrow e'$

  Really, this is $e.l : \tau \land e.l \rightarrow e.l' \Rightarrow e.l': \tau$

  We have the typing rule $\frac{\Gamma \vdash e: \tau_1 \times \tau_2}{\Gamma \vdash e.l: \tau_1}$

  Remember the IH: Preservation holds for the top part of the rule.

  We assume $e.l \rightarrow e.l'$

  and then we have the rule $\frac{e \rightarrow e'}{e.l \rightarrow e.l'}$

  which gives us $e: \tau_1 \times \tau_2$, and the by typing rule $\frac{\Gamma \vdash e': \tau_1 \times \tau_2}{\Gamma \vdash e.l': \tau_1}$ and thus the statement holds

• Case 2: $e.r: \tau \Rightarrow e.r \rightarrow e'$

  Same as case 1 really.

• Case 3: Extraction, $$ (TODO: Finish this part)

Progress: Progress: If $e: \tau$, then either $e \text{ val}$ or there exists $e'$ such that $e \rightarrow e'$

(TODO: Finish this part)

Sum Types

Hoare's Billion Dollar Mistake is an example of the sum type. But so is the Option type. We can all kind of agree that the Option type is "the way to do things" when dealing with pointer-y stuff. The reason being is that rather than hiding semantic meaning in NULL, the Option type provides us a good way of reasoning about it's value. Incidentally, we can also show some notion of type safety over sum types (which is why we should roll this stuff into the type system)

$$ \text{Typ } \tau ::= \texttt{void} | \texttt{sum}(\tau_1; \tau_2) $$

$$ \text{Exp } e ::= \texttt{abort}{\tau}(e) | \texttt{case}(e;x_1.e_1;x_2.e_2) | \texttt{in}{\tau_1; \tau_2}[l](e) | \texttt{in}{\tau_1; \tau_2}[r](e) $$

Once again, we'll omit reproducing the statics and dynamics for sum types, just go get the textbook PDF.

Preservation: If $e: \tau$ and $e \rightarrow e'$ then $e': \tau$

• Case 1: $l.e \rightarrow l.e'$

  Really, this is $l.e: \tau_1 \land l.e \rightarrow l.e' \Rightarrow l.e': \tau_1$

  We have the typing rule $\frac{\Gamma \vdash e: \tau_1}{\Gamma \vdash l.e: \tau_1 + \tau_2 }$.

  Assume $l.e \rightarrow l.e'$

  Then we have the rule $[\frac{e \rightarrow e'}{l.e \rightarrow l.e'}]$ (this only really makes sense under eagar eval, anyways..), which gives us $e \rightarrow e'$ as a consequence of the IH

  For which we have the rule 11.1b again, this time on $e'$ and $l.e'$ which gives us $\frac{\Gamma \vdash e': \tau_1}{\Gamma \vdash l.e': \tau_1 + \tau_2 }$ and thus we've proven this case.

• Case 2: $l.e \rightarrow l.e'$ :%s/l.e/r.e/g on case 1.

• Case 3: $ \texttt{case} l.e {l.x_1 \hookrightarrow e_1 | r.x_2 \hookrightarrow e_2} \rightarrow [e/x_1]e_1$

  (TODO)

Progress: (TODO)