Someone's Intermediate Representation

0%

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}}$$

$$\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}$$
$$\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}$$
$$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$$