PFPL Chapter 11 Sum Types

Posted on In Disqus:

Please refer this link from page 87 to 94.

From Product to Sum

The binary sum type offers a choice of two types, and the nullary sum offers a choice of no things.

Finite sums generalize binary and nullary sums to allow an arbitrary number of cases indexed by a finite index set.

As with products, sums comes in with both eager and lazy variants, differs in how values of sum types are defined.

Nullary and Binary Sums

$$
\begin{align}
\text{Typ }\tau&&::=&&\text{void}&&\text{void}&&\text{nullary sum}\\
&&&&+(\tau_1;\tau_2)&&\tau_1 + \tau_2&&\text{binary sum}\\
\text{Exp }e&&::=&&\text{case}\lbrace \tau\rbrace(e)&&\text{case }e\lbrace \rbrace&&\text{case null}\\
&&&&\text{in}\lbrack l\rbrack\lbrace\tau_1;\tau_2\rbrace(e)&&l \cdot e&&\text{left injection}\\
&&&&\text{in}\lbrack r \rbrack\lbrace \tau_1;\tau_2\rbrace (e)&&r \cdot e&&\text{right injection}\\
&&&&\text{case}\lbrace x_1.e_1;x_2.e_2 \rbrace(e)&&\text{case }e\lbrace l\cdot x_1 \hookrightarrow e_1\shortmid r\cdot x_2 \hookrightarrow e_2 \rbrace&&\text{case analysis}\\
\end{align}
$$

Statics

The nullary sum represents a choice of zero alternative, and hence admits no introduction form. The elimination form, case e { }, expresses the contradiction that $e​$ is a value of type void.

A value of sum type is eliminated by case analysis.
$$
\dfrac{\Gamma \vdash e:\text{void}}{\Gamma \vdash \text{case }e\lbrace \rbrace:\tau}\\
\dfrac{\Gamma \vdash e:\tau_1}{\Gamma \vdash l\cdot e :\tau_1 + \tau_2}\\
\dfrac{\Gamma \vdash e:\tau_2}{\Gamma \vdash r\cdot e :\tau_1 + \tau_2}\\
\dfrac{\Gamma \vdash e:\tau_1 + \tau_2 \phantom{“”}\Gamma,x_1:\tau_1\vdash e_1:\tau\phantom{“”}\Gamma,x_2:\tau_2\vdash e_2:\tau}{\Gamma\vdash \text{case }e\lbrace l\cdot x_1 \hookrightarrow e_1\shortmid r \cdot x_2 \hookrightarrow e_2 \rbrace :\tau}
$$

Since an expression of sum type could evaluate to either form at run-time, we must insist that both branches on case analysis yield the same type.

Dynamics

$$
\dfrac{e \longmapsto e’}{\text{case }e \lbrace \rbrace \longmapsto \text{case }e’\lbrace\rbrace}\\
\dfrac{[e \text{ val}]}{l\cdot e\text{ val}}\\
\dfrac{[e \text{ val}]}{r \cdot e \text{ val}}\\
\Big\lbrack \dfrac{e \longmapsto e’}{l\cdot e \longmapsto l \cdot e’}\Big\rbrack\\
\Big\lbrack \dfrac{e \longmapsto e’}{r\cdot e \longmapsto r \cdot e’}\Big\rbrack\\
\dfrac{e \longmapsto e’}{\text{case }e\lbrace l\cdot x_1 \hookrightarrow e_1\shortmid r \cdot x_2 \hookrightarrow e_2 \rbrace \longmapsto \text{case }e’\lbrace l\cdot x_1 \hookrightarrow e_1\shortmid r \cdot x_2 \hookrightarrow e_2 \rbrace}\\
\dfrac{[e\text{ val}]}{\text{case }l\cdot e\lbrace l\cdot x_1 \hookrightarrow e_1\shortmid r \cdot x_2 \hookrightarrow e_2 \rbrace \longmapsto [e/x_1]e_1}\\
\dfrac{[e\text{ val}]}{\text{case }r\cdot e\lbrace l\cdot x_1 \hookrightarrow e_1\shortmid r \cdot x_2 \hookrightarrow e_2 \rbrace \longmapsto [e/x_2]e_2}
$$

Safety Theorem

Preservation

If $e : \tau$ and $e\longmapsto e’$, then $e’:\tau$.

Progress

If $e:\tau$, then either $e :\text{val}$ or $\exists e’,e\longmapsto e’$.

Finite Sums

$$
\begin{align}
\text{Typ}&&\tau&&::=&&\text{sum}(\lbrace i\hookrightarrow \tau_i \rbrace_{i \in I})&&\lbrack\tau_i\rbrack_{i\in I}&&\text{sum}\\
\text{Exp}&&e&&::=&&\text{in}\lbrack i \rbrack\lbrace \vec{\tau}\rbrace (e)&&i \cdot e &&\text{injection}\\
&&&&&&\text{case}(e;\lbrace i \hookrightarrow x_i.e_i \rbrace_{i \in I})&& \text{case }e\lbrace i\cdot x_i \hookrightarrow e_i \rbrace_{i \in I} &&\text{case analysis}\\
\end{align}
$$

Notation $\vec{\tau}$ stands for a finite function $\lbrace i \hookrightarrow \tau_i \rbrace_{i \in I}$ for some index set $I$. Type $\text{sum}(\lbrace i\hookrightarrow \tau_i \rbrace_{i \in I})$ or $\sum_{i\in I}\tau_i$ is the type of $I-$classified values of form $i \cdot e_i$ where $e_i : \tau_i$.

When $I = \lbrace i_1,\dots,i_n\rbrace​$, the type of $I-​$classified values may be written $\lbrack i_1\hookrightarrow \tau_1,\dots,i_n\hookrightarrow \tau_n \rbrack​$.

Statics

$$
\dfrac{\Gamma \vdash e :\tau_k\phantom{“”}(1 \leq k \le n)}{\Gamma \vdash i_k\cdot e:\lbrack i_1\hookrightarrow \tau_1,\dots,i_n\hookrightarrow \tau_n \rbrack}\\
\dfrac{\Gamma \vdash e :\lbrack i_1\hookrightarrow \tau_1,\dots,i_n\hookrightarrow \tau_n \rbrack\phantom{“”}\Gamma,x_1:\tau_1\vdash e_1:\tau\phantom{a}\dots\phantom{a}\Gamma,x_n:\tau_n\vdash e_n:\tau}{\Gamma \vdash \text{case }e\lbrace i_1\cdot x_1 \hookrightarrow e_1\shortmid\dots\shortmid i_n \cdot x_n \hookrightarrow e_n \rbrace : \tau}
$$

Dynamics

$$
\dfrac{[e \text{ val}]}{i \cdot e: \text{val}}\\
\Big\lbrack\dfrac{e \longmapsto e’}{i\cdot e \longmapsto i \cdot e’} \Big\rbrack\\
\dfrac{e \longmapsto e’}{\text{case }e\lbrace i\cdot x_i \hookrightarrow e_i \rbrace_{i \in I} \longmapsto \text{case }e’\lbrace i\cdot x_i \hookrightarrow e_i \rbrace_{i \in I}}\\
\dfrac{i\cdot e\text{ val}}{\text{case } i\cdot e\lbrace i\cdot x_i \hookrightarrow e_i \rbrace_{i \in I} \longmapsto [e/x_i]e_i}
$$

Safety Theorem

If $e :\tau$, then either $e\text{ val}$ or $\exists e’ : \tau, e \longmapsto e’$.

Applications of Sum Types

Void and Unit

The type unit has exactly one element $\langle \rangle$, whereas the type void has no elements at all.

Consequently, if $e :\text{unit}$, then $e$ evaluates to a value $\langle \rangle$. In another word, $e$ has no interesting value.

On the other hand, if $e:\text{void}$, then $e$ must not yield a value.

Booleans

$$
\begin{align}
\text{Typ}&&\tau&&::=&&\text{bool}&&\text{bool}&&\text{booleans}\\
\text{Exp}&&e&&::=&&\text{true}&&\text{true}&&\text{truth}\\
&&&&&&\text{false}&&\text{false}&&\text{falsity}\\
&&&&&&\text{if}(e;e_1;e_2)&& \text{if }e\text{ then } e_1 \text{ else }e_2 &&\text{conditional}
\end{align}
$$

Statics

$$
\dfrac{}{\Gamma \vdash \text{true}:\text{bool}}\\
\dfrac{}{\Gamma \vdash \text{false}:\text{bool}}\\
\dfrac{\Gamma \vdash e :\text{bool}\phantom{“”}\Gamma \vdash e_1 :\tau\phantom{“”}\Gamma \vdash e_2:\tau}{\Gamma \vdash \text{if }e\text{ then }e_1\text{ else }e_2:\tau}\\
$$

Dynamics

$$
\dfrac{}{\text{true}:\text{val}}\\
\dfrac{}{\text{false}:\text{val}}\\
\dfrac{}{\text{if true then }e_1\text{ else }e_2 \longmapsto e_1}\\
\dfrac{}{\text{if false then }e_1\text{ else }e_2 \longmapsto e_2}\\
\dfrac{e \longmapsto e’}{\text{if }e\text{ then }e_1\text{ else }e_2 \longmapsto \text{if }e’\text{ then }e_1\text{ else }e_2}
$$

In Form of Sum and Product Types

$$
\begin{align}
\text{bool}&=\text{unit}+\text{unit}\\
\text{true}&=l\cdot \langle\rangle\\
\text{false}&=r\cdot \langle\rangle\\
\text{if }e\text{ then }e_1\text{ else }e_2&=\text{case }e\lbrace l\cdot x_1 \hookrightarrow e_1 \shortmid r\cdot x_2 \hookrightarrow e_2 \rbrace
\end{align}
$$

Enumerations

Example, consider card suit, we define a type suit by showing $\text{suit} =\lbrack \text{unit} \rbrack_{\underline{}\in I}​$ where $I = \lbrace\diamondsuit, \spadesuit,\heartsuit,\clubsuit \rbrace​$.

The elimination form the case analysis $\text{case }e \lbrace \clubsuit \hookrightarrow e_0 \shortmid\diamondsuit \hookrightarrow e_1 \shortmid \heartsuit\hookrightarrow e_2\shortmid\spadesuit \hookrightarrow e_3 \rbrace​$.
$$
\begin{align}
\text{Typ }\tau::=&&\text{suit}&&\text{suit}&&\text{card suits}\\
\text{Exp }e::=&&\spadesuit&&\text{spade}&&\text{spade suit}\\
&&\diamondsuit&&\text{diamond}&&\text{diamond suit}\\
&&\heartsuit&&\text{heart}&&\text{heart suit}\\
&&\clubsuit&&\text{club}&&\text{club suit}\\
&&\text{suitElim}(e;\lbrace i\hookrightarrow x_i.e_i \rbrace_{i\in I})&& \text{suitElim }e\lbrace i \cdot x_i\hookrightarrow e_i \rbrace_{i\in I} &&\text{suit analysis}
\end{align}
$$

Statics

$$
\dfrac{}{\Gamma \vdash \text{spade}:\text{suit}}\\
\dfrac{}{\Gamma \vdash \text{diamond}:\text{suit}}\\
\dfrac{}{\Gamma \vdash \text{heart}:\text{suit}}\\
\dfrac{}{\Gamma \vdash \text{club}:\text{suit}}\\
\dfrac{\Gamma \vdash e :\text{suit}\phantom{“”}\Gamma \vdash e_i :\tau\phantom{“”}(i \in I)}{\Gamma \vdash \text{suitElim }e\lbrace i \cdot x_i \hookrightarrow e_i \rbrace_{i \in I} :\tau}
$$

Dynamics

$$
\dfrac{}{\text{spade} :\text{val}}\\
\dfrac{}{\text{diamond} :\text{val}}\\
\dfrac{}{\text{heart} :\text{val}}\\
\dfrac{}{\text{club} :\text{val}}\\
\dfrac{}{\text{suitElim spade}\lbrace i\cdot x_i\hookrightarrow e_i \rbrace_{i \in I} \longmapsto e_{spade}}\\
\dfrac{}{\text{suitElim diamond}\lbrace i\cdot x_i\hookrightarrow e_i \rbrace_{i \in I} \longmapsto e_{diamond}}\\
\dfrac{}{\text{suitElim heart}\lbrace i\cdot x_i\hookrightarrow e_i \rbrace_{i \in I} \longmapsto e_{heart}}\\
\dfrac{}{\text{suitElim club}\lbrace i\cdot x_i\hookrightarrow e_i \rbrace_{i \in I} \longmapsto e_{club}}\\
\dfrac{e \longmapsto e’}{\text{suitElim }e\lbrace i\cdot x_i\hookrightarrow e_i \rbrace_{i \in I} \longmapsto \text{suitElim }e’\lbrace i\cdot x_i\hookrightarrow e_i \rbrace_{i \in I}}
$$

In Form of Sum and Product Types

$$
\begin{align}
\text{suit}&=\sum_{i\in I}\text{unit}\\
\text{spade}&=\spadesuit \cdot \langle \rangle\\
\text{diamond}&=\diamondsuit \cdot \langle \rangle\\
\text{heart}&=\heartsuit \cdot \langle \rangle\\
\text{club}&=\clubsuit \cdot \langle \rangle\\
\text{suitElim }e \lbrace i\cdot x_i \hookrightarrow e_i \rbrace_{i\in I}&=\text{case }e\lbrace i\cdot x_i \hookrightarrow e_i\rbrace_{i \in I}
\end{align}
$$

Options

$$
\begin{align}
\text{Typ }\tau::=&&\text{opt}(\tau)&&\text{opt }\tau&&\text{option}\\
\text{Exp }e::=&&\text{null}&&\text{null}&&\text{nothing}\\
&&\text{just}(e)&&\text{just}(e)&&\text{something}\\
&&\text{ifnull}\lbrace\tau\rbrace\lbrace e_1;x.e_2\rbrace(e)&&\text{ifnull }e\lbrace \text{null} \hookrightarrow e_1\shortmid \text{just}(x) \hookrightarrow e_2 \rbrace&&\text{null test}\\
\end{align}
$$

If we want to see how it is defined by sum and nullary products, we can see
$$
\begin{align}
\tau\text{ opt}&=\text{unit}+\tau\\
\text{null}&=l \cdot \langle \rangle\\
\text{just}(e)&=r \cdot \tau\\
\text{ifnull }e \lbrace\text{null}\hookrightarrow e_1 \shortmid \text{just}(x_2) \hookrightarrow e_2 \rbrace&= \text{case }e \lbrace l\cdot \underline{}\hookrightarrow e_1 \shortmid r\cdot x_2\hookrightarrow e_2 \rbrace
\end{align}
$$

In practical environment we can define $\text{ifnull }e\lbrace \text{null} \hookrightarrow e_{error}\shortmid \text{just}(x) \hookrightarrow e_2 \rbrace$.

Exercise

11.2

$$
\begin{align}
\text{null}&\triangleq \langle \text{false}, \text{null}\rangle\\
\text{just}(e)&\triangleq \langle \text{true}, e \rangle\\
\text{ifnull }e \lbrace \text{null}\hookrightarrow e_1 \shortmid \text{just}(x)\hookrightarrow e_2 \rbrace &\triangleq \text{if } e\cdot l\text{ then }[e \cdot r/x]e_2\text{ else }e_1
\end{align}
$$

But this kind of design will arise 2 problems:

  • The design makes use of null inherit from each type, but this causes contradiction with empty type such as void which does not really have a value.
  • The second part is always accessible in computation, which is absolutely not safe.

11.3

We can extend the schema from product types to product of sums of atomic types.

11.4

NOR and NAND

NOR

$$
\dfrac{}{\text{NOR true true}\longmapsto \text{false}}\\
\dfrac{}{\text{NOR true false}\longmapsto \text{false}}\\
\dfrac{}{\text{NOR false false}\longmapsto \text{true}}\\
\dfrac{}{\text{NOR false true}\longmapsto \text{false}}
$$

NAND

$$
\dfrac{}{\text{NAND true true} \longmapsto \text{false}}\\
\dfrac{}{\text{NAND true false} \longmapsto \text{true}}\\
\dfrac{}{\text{NAND false true} \longmapsto \text{true}}\\
\dfrac{}{\text{NAND false false} \longmapsto \text{true}}
$$

Adder

Half Adder

$$
\dfrac{}{\text{half-adder }\langle e_1,e_2\rangle\longmapsto \langle \text{AND }\langle e_1, e_2 \rangle, \text{XOR }\langle e_1, e_2 \rangle \rangle}
$$

Full Adder

$$
\dfrac{\text{half-adder}\langle e_1,e_2\rangle \longmapsto \langle e_{c1},e_{s1}\rangle\phantom{“”}\text{half-adder}\langle e_{s1},e_c\rangle \longmapsto \langle e_{c2},e_{s}\rangle}{\text{full-adder }\langle e_1,e_2,e_c\rangle \longmapsto \langle \text{OR }\langle e_{c1},e_{c2} \rangle, e_s \rangle}
$$

11.5

$$
e_{RS} \triangleq \lambda(\langle r,s\rangle :\text{signal}\times\text{signal})\lambda(t :\text{nat})e_{RS}’\\
e’_{RS}\triangleq \text{rec }t\lbrace z\hookrightarrow \langle \text{true},\text{false}\rangle \shortmid s(t’) \text{ with }\langle r’,s’\rangle \hookrightarrow \langle \text{NOR }\langle r,s’\rangle, \text{NOR }\langle r’,s\rangle \rangle \rbrace
$$