PFPL Chapter 10 Product Types

Posted on In Disqus:

Please refer this link from page 81 to 85.

From Unit to Finite Product

Binary product of two types consists of ordered pairs of values, one from each type in order specified.

Nullary product or unit type consists solely of unique “null tuple” of no value.

Associated elimination form of binary product is projection, which select first/second of the pair. No associated elimination form exists for nullary product.

Product types admits both lazy and eager dynamics:

  • In lazy dynamics, a pair is a value without regard to whether its components are values, they are not evaluated until (if ever) they are accessed and used in another computation.
  • In eager dynamics, a pair is a value only if its components are values; they are evaluated when the pair is created.

Finite product with form $\langle \tau_i \rangle_{i\in I}$ is a more general form, indexed by a finite set of indices $I$.

The components are accessed by $I$-indexed projection operations, generalizing the binary case. Similar to binary product, finite products admit both an eager and a lazy interpretation.

Nullary and Binary Products

$$
\begin{align}
\text{Typ}&&\tau&&::=&&\text{unit}&&\text{unit}&&\text{nullary product}\\
&&&&&&\times(\tau_1;\tau_2)&&\tau_1 \times \tau_2&&\text{binary product}\\
\text{Exp}&&e&&::=&&\text{triv}&&\langle \rangle&&\text{null tuple}\\
&&&&&&\text{pair}(e_1;e_2)&&\langle e_1,e_2\rangle&&\text{ordered pair}\\
&&&&&&\text{pr}\lbrack l \rbrack (e)&&e \cdot l&&\text{left projection}\\
&&&&&&\text{pr}\lbrack r\rbrack(e)&&e \cdot r&&\text{right projection}\\
\end{align}
$$

Statics

$$
\dfrac{}{\Gamma \vdash \langle \rangle :\text{unit}}\\
\dfrac{\Gamma \vdash e_1 :\tau_1 \phantom{“”}\Gamma \vdash e_2 : \tau_2}{\Gamma \vdash \langle e_1,e_2\rangle :\tau_1 \times \tau_2}\\
\dfrac{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash e \cdot l : \tau_1}\\
\dfrac{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash e \cdot r : \tau_2}
$$

Dynamics

$$
\dfrac{}{\langle \rangle \text{ val}}\\
\dfrac{[e_1 \text{ val}] \phantom{“”}[e_2 \text{ val}]}{\langle e_1,e_2 \rangle \text{ val}}\\
\left[\dfrac{e_1 \longmapsto e_1’}{\langle e_1,e_2\rangle \longmapsto \langle e_1’,e_2\rangle}\right]\\
\left[\dfrac{e_1 \text{ val}\phantom{“”}e_2 \longmapsto e_2’}{\langle e_1,e_2\rangle \longmapsto \langle e_1,e_2’\rangle} \right]\\
\dfrac{e \longmapsto e’}{e \cdot l \longmapsto e’\cdot l}\\
\dfrac{e \longmapsto e’}{e \cdot r \longmapsto e’\cdot r}\\
\dfrac{[e_1 \text{ val}]\phantom{“”}[e_2 \text{ val}]}{\langle e_1,e_2\rangle \cdot l\longmapsto e_1}\\
\dfrac{[e_1 \text{ val}]\phantom{“”}[e_2 \text{ val}]}{\langle e_1,e_2\rangle \cdot r\longmapsto e_2}
$$

The rules and premises which are bracketed are omitted for a lazy dynamics and included for an eager dynamics.

Safety Theorem

Preservation

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

Progress

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

Finite Products

$$
\begin{align}
\text{Typ}&&\tau&&::=&&\text{prod}(\lbrace i \hookrightarrow \tau_i\rbrace_{i\in I}) &&\langle \tau_i \rangle_{i\in I}&&\text{product}\\
\text{Exp}&&e&&::=&&\text{tpl}(\lbrace i \hookrightarrow e_i\rbrace_{i\in I})&&\langle e_i\rangle_{i\in I}&&\text{tuple}\\
&&&&&&\text{pr}\lbrack i\rbrack(e)&&e \cdot i &&\text{projection}\\
\end{align}
$$

Type $\text{prod}(\lbrace i \hookrightarrow \tau_i\rbrace_{i\in I})$ can be written as $\prod_{i\in I} \tau_i$ is the type for $I$-tuple of expression $e_i$ of $\tau_i$ where $i \in I$.

Finite product generalize empty and binary products by choosing $I$ to be $\varnothing$ or $\lbrace l,r\rbrace$.

Statics

$$
\dfrac{\Gamma \vdash e_1 :\tau_1\phantom{“”}\dots\phantom{“”}\Gamma \vdash e_n : \tau_n}{\Gamma \vdash \langle i_1 \hookrightarrow e_1,\dots,i_n\hookrightarrow e_n\rangle :\langle i_1 \hookrightarrow \tau_1,\dots,i_n\hookrightarrow \tau_n\rangle}\\
\dfrac{\Gamma \vdash e:\langle i_1 \hookrightarrow \tau_1,\dots,i_n\hookrightarrow \tau_n\rangle\phantom{“”}(1 \leq k \leq n)}{\Gamma \vdash e\cdot i_k : \tau_k}
$$

Dynamics

$$
\dfrac{[e_1\text{ val}\phantom{“”}\dots\phantom{“”}e_n\text{ val}]}{\langle i_1 \hookrightarrow e_1,\dots,i_n\hookrightarrow e_n\rangle \text{ val}}\\
\left[\dfrac{\lbrace e_1\text{ val}\phantom{a}\dots\phantom{a}e_n\text{ val} \phantom{aaa} e_1’=e_1\phantom{a}\dots\phantom{a}e_{j-1}’=e_{j-1} \phantom{aaa}e_j\longmapsto e_j’ \phantom{aaa}e_{j+1}’=e_{j+1}\phantom{a}\dots\phantom{a}e_n’=e_n \rbrace}{\langle i_1 \hookrightarrow e_1,\dots,i_n\hookrightarrow e_n\rangle \longmapsto \langle i_1 \hookrightarrow e_1’,\dots,i_n\hookrightarrow e_n’\rangle}\right]\\
\dfrac{e\longmapsto e’}{e\cdot i \longmapsto e’\cdot i}\\
\dfrac{[\langle i\hookrightarrow e_1,\dots,i_n\hookrightarrow e_n\rangle \text{ val}]}{\langle i\hookrightarrow e_1,\dots,i_n\hookrightarrow e_n\rangle \cdot i_k \longmapsto e_k}
$$

Safety Theorem

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

Primitive Mutual Recursion

Primitive Recursion Rewrite

Using product types we can simplify the primitive recursion in T so that only recursive result on the predecessor, not the predecessor itself, is passed to the successor branch.

In this way we can redefine $\text{rec}\lbrace e_0;x.y.e_1 \rbrace(e)$ with $\text{iter}\lbrace e_0;x.e_1\rbrace(e)$ in the following form
$$
\text{iter}\lbrace \langle z,e_0\rangle;x’.\langle s(x’\cdot l),[x’\cdot l, x’\cdot r/x,y]e_1 \rangle \rbrace(e)
$$

Mutual Primitive Recursion

Example, see the definition on natural numbers
$$
\begin{align}
e(0) &= 1\\
o(0) &= 0\\
e(n+1) &= o(n) \\
o(n+1) &= e(n)
\end{align}
$$
First define function $e_{eo}$ of type $\text{nat}\to(\text{nat}\times \text{nat})\to(\text{nat}\times \text{nat})$ that computes both results simultaneously
$$
\lambda(x : \text{num})(\text{iter } \langle x, \text{id} \rangle \lbrace \langle z, e \rangle \hookrightarrow \langle z, e \rangle \shortmid \langle s(k), f \rangle \hookrightarrow \langle k, \text{swap} \circ f \rangle \rbrace) \cdot r
$$

We may define $e_e$ and $e_o$ as follows:
$$
e_e \triangleq \lambda(n: \text{num}) (e_{eo} (n)\langle 1,0\rangle)\cdot l\\
e_o \triangleq \lambda(n: \text{num}) (e_{eo} (n)\langle 1,0\rangle)\cdot r
$$
Or we can follow book definition that $e_{eo}$ has $\text{nat}\to(\text{nat}\times\text{nat})$ with expression
$$
\lambda(n : \text{num}) \text{ iter }n\lbrace z \hookrightarrow \langle 1,0\rangle \shortmid s(b) \hookrightarrow \langle b \cdot r,b\cdot l\rangle \rbrace
$$
(since he said $b$ is the previous result), then $e_e$ and $e_o$ follow that $e_{eo}$.

Exercise

10.1

Define the database schema to be $\prod_{i \in I}\tau_i$ as $\varepsilon$, then we can define the database as type $\text{nat}\times(\text{nat}\to \varepsilon)$.

The database type $\langle n,seq \rangle$ is defined with:

  • $n$ limits the range of the sequence, indicating the largest capacity.
  • $seq$ is defined on index $0 \le k < n$.

The project function can be done on index range $0 \leq k < n$ that each instance of schema is $\langle s(k) \cdot i \rangle_{i \in I’}$.

Thus the project on each instance of schema is $\lambda(k :\text{nat})\langle s(k) \cdot i \rangle_{i \in I’}$.

10.2

To bypass the eager dynamics of positive product, one can wrap the expression like $\lambda(\underline{}:\text{unit})e$, then we can see that

  • $\langle e_1,e_2\rangle \triangleq (\lambda(\underline{}:\text{unit})e_1) \otimes (\lambda(\underline{} :\text{unit})e_2)$
  • $e \cdot l \triangleq \text{split }e \text{ as }x_1 \otimes \underline{} \text{ in }x_1(\langle \rangle)$
  • $e \cdot r \triangleq \text{split }e \text{ as } \underline{} \otimes x_2 \text{ in }x_2(\langle \rangle)$

Negative product in terms of positive product

  • $e_1 \otimes e_2 \triangleq \text{let }x_1 \text{ be }e_1\text{ in let }x_2\text{ be }e_2\text{ in }x_1\otimes x_2$
  • $\text{split }e_0\text{ as }x_1\otimes x_2\text{ in }e\triangleq \text{let }x_1 \text{ be }e_0 \cdot l \text{ in let }x_2\text{ be }e_0 \cdot r \text{ in }e$

10.3

$$
\dfrac{\Gamma \vdash e_0 :\langle \rangle\phantom{“”}\Gamma \vdash e : \tau}{\Gamma \vdash \text{check}(e_0;e):\tau}
$$

$e_0$ will always be evaluated and will only be evaluated as $\langle \rangle$. Thus both sides conditions satisfied.