Semester 2, 2018

# Tute (Week 8)

## 1 Safety and Liveness

### 1.1 Decomposing Properties

For each of the following program properties, decompose it into the intersection of a safety property and a liveness property.

1. The program will allocate exactly 100MB of memory.
2. The program will not stack overflow.
3. The program will return the sum of its inputs.
4. The program will call the function foo.
1. The safety component is that the program will not allocate more than 100MB of memory. The liveness component is that the program will allocate at least 100MB of memory.
2. The safety component is that the program will not stack overflow. The liveness component is the set of all behaviours.
3. The liveness component is that the program will return. The safety component is that if the program returns, it will return the sum of its inputs.
4. The safety component is the set of all behaviours. The liveness component is that the function foo will be called.

### 1.2 Type Safety

Why is the handling of partial functions important for a type safe language? How does it impact progress and preservation?

In order to satisfy progress, we need a successor state for every well-typed expression, including invocations of partial functions. Thus, we must introduce an error state, that is a final state, that is the result of evaluating a partial function outside of its domain.

In order to satisfy preservation, we allow error to take on any type at all.

## 2 Data Types

### 2.1 Converting from Haskell

Use MinHS type constructors $$+$$, $$\times$$ and $$\mathbf{rec}$$ to describe types isomorphic to each of the following Haskell types. Give example terms for each type.

data Direction = East | West | North | South
data Foo = Foo Int Bool Int
data Tree = Node Tree Tree | Leaf

\begin{array}{lcllcl} \texttt{Direction} & \simeq & \mathbf{1} + (\mathbf{1} + (\mathbf{1} + \mathbf{1})) & \texttt{West} & \simeq & (\mathsf{InR}\ (\mathsf{InL}\ \texttt{()}))\\ \texttt{Foo} & \simeq & \mathtt{Int}\times(\mathtt{Bool}\times\mathtt{Int}) &\texttt{Foo}\ 3\ \texttt{True}\ 2 & \simeq & (3, (\mathsf{True}, 2))\\ \texttt{Tree} & \simeq & \mathbf{rec}\ t. (t \times t) + \mathbf{1}\\ \end{array}

$\texttt{Node}\ \texttt{Leaf}\ \texttt{Leaf} \simeq (\mathsf{roll}\ (\mathsf{InL}\ (\mathsf{roll}\ (\mathsf{InR}\ ()) , \mathsf{roll}\ (\mathsf{InR}\ ()) )))$

### 2.2 Recursive Types

Give an example MinHS term for each of the following types (if such a term exists), and derive the typing judgement for that term.

1. $$\mathbf{rec}\ t.\ (\mathtt{Int} + t)$$
2. $$\mathbf{rec}\ t.\ (\mathtt{Int} \times \mathtt{Bool})$$
3. $$\mathbf{rec}\ t.\ (\mathtt{Int} \times t)$$

1: $\dfrac{ \dfrac { \dfrac { \dfrac{ \dfrac{}{3 : \mathtt{Int} }} {\mathsf{InL}\ 3 : (\mathtt{Int} + (\mathbf{rec}\ t.\ (\mathtt{Int} + t)) )} } {\mathsf{roll}\ (\mathsf{InL}\ 3) : (\mathbf{rec}\ t.\ (\mathtt{Int} + t)) } } {\mathsf{InR}\ (\mathsf{roll}\ (\mathsf{InL}\ 3)) : (\mathtt{Int} + (\mathbf{rec}\ t.\ (\mathtt{Int} + t)) )} } {\mathsf{roll}\ (\mathsf{InR}\ (\mathsf{roll}\ (\mathsf{InL}\ 3))) : \mathbf{rec}\ t.\ (\mathtt{Int} + t)}$ 2: $\dfrac{ \dfrac{ \dfrac{}{3 : \mathtt{Int}} \quad \dfrac{}{\mathsf{True} : \mathtt{Bool}} } {(3, \mathsf{True}) : (\mathtt{Int} \times \mathtt{Bool})}} {\mathsf{roll}\ (3, \mathsf{True}) : \mathbf{rec}\ t.\ (\mathtt{Int} \times \mathtt{Bool})}$ 3: There is no finite term of this type, but we can make one with recfun: $\textbf{recfun}\ f\ x = \mathsf{roll}\ (x, f\ x)$

### 2.3 Typing Terms

For each of the following terms, give a possible type for the term (there may be more than one type).

1. $$(\mathsf{InL}\ \mathsf{True})$$
2. $$(\mathsf{InR}\ \mathsf{True})$$
3. $$(\mathsf{InL}\ (\mathsf{InL}\ \mathsf{True}))$$
4. $$(\mathsf{roll}\ (\mathsf{InR}\ \mathsf{True}))$$
5. $$(\texttt{()}, (\mathsf{InL}\ \texttt{()}))$$

In these answers, I've opted for the smallest possible type.

1. $$\texttt{Bool} + \mathbf{0}$$
2. $$\mathbf{0} + \texttt{Bool}$$
3. $$(\texttt{Bool} + \mathbf{0}) + \mathbf{0}$$
4. $$\mathbf{rec}\ t.\ (\mathbf{0} + \texttt{Bool})$$
5. $$\mathbf{1} \times (\mathbf{1} + \mathbf{0})$$

### 2.4 Curry-Howard

#### 2.4.1 Proof Witnesses

For which of the following types can you write a terminating, total (i.e., not returning error, undefined or causing other runtime errors, but a value of the result type) MinHs function? Try to answer this question without trying to implement the function.

1. $$(a \rightarrow b) \rightarrow (b \rightarrow c) \rightarrow (a \rightarrow c)$$
2. $$((a \times b) \rightarrow c) \rightarrow (a \rightarrow c)$$
3. $$(a \rightarrow c) \rightarrow ((a \times b) \rightarrow c)$$

What proposition does each of these types correspond to?

1. Corresponds to the transitivity of implication which is constructively provable, therefore a program can be written in MinHS.
2. Corresponds to the proposition $$((a \land b) \rightarrow c) \rightarrow (a \rightarrow c)$$ which is not constructively provable and therefore such a program cannot be written.
3. Corresponds to the proposition $$(a \rightarrow c) \rightarrow ((a \land b) \rightarrow c)$$, which is constructively provable. Therefore such a program can be written.

2018-11-16 Fri 19:37