Tute - Completed (Week 8)

1. Data Types
2. Polymorphism
- 2.1. Quantifier Positions
- 2.2. Parametricity

1. Data Types

1.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}\ ()) ))) \]

1.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.

\(\mathbf{rec}\ t.\ (\mathtt{Int} + t)\)
\(\mathbf{rec}\ t.\ (\mathtt{Int} \times \mathtt{Bool})\)
\(\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:

\[ \mathbf{recfun}\ f\ x = \mathsf{roll}\ (x, f\ x) \]

1.3. Type Isomorphisms

Which of the following types are isomorphic to each other (assuming a strict semantics)?

\(\textbf{rec}\ t.\ t \times t\)
\(\textbf{0}\)
\(\textbf{1}\)
\(\textbf{1} \times \textbf{0}\)
\(\textbf{rec}\ t.\ t \times \textbf{1}\)
\(\textbf{rec}\ t.\ t + \textbf{1}\)

1, 2, 4, 5 are all isomorphic. 3 and 6 are in their own isomorphism equivalence classes.

1.4. Typing Terms

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

\((\mathsf{InL}\ \mathsf{True})\)
\((\mathsf{InR}\ \mathsf{True})\)
\((\mathsf{InL}\ (\mathsf{InL}\ \mathsf{True}))\)
\((\mathsf{roll}\ (\mathsf{InR}\ \mathsf{True}))\)
\((\texttt{()}, (\mathsf{InL}\ \texttt{()}))\)

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

\(\texttt{Bool} + \mathbf{0}\)
\(\mathbf{0} + \texttt{Bool}\)
\((\texttt{Bool} + \mathbf{0}) + \mathbf{0}\)
\(\mathbf{rec}\ t.\ (\mathbf{0} + \texttt{Bool})\)
\(\mathbf{1} \times (\mathbf{1} + \mathbf{0})\)

1.5. Curry-Howard

1.5.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.

\((a \rightarrow b) \rightarrow (b \rightarrow c) \rightarrow (a \rightarrow c)\)
\(((a \times b) \rightarrow c) \rightarrow (a \rightarrow c)\)
\((a \rightarrow c) \rightarrow ((a \times b) \rightarrow c)\)

What proposition does each of these types correspond to?

Corresponds to the transitivity of implication which is constructively provable, therefore a program can be written in MinHS.
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.
Corresponds to the proposition \((a \rightarrow c) \rightarrow ((a \land b) \rightarrow c)\), which is constructively provable. Therefore such a program can be written.

1.5.2. Proving a proposition

Write a program which is a proof of the symmetry of disjunction, i.e. \[A \lor B \Rightarrow B \lor A\].

proof = (recfun x = case x of InL a -> InR a; InR b -> InL b)

1.5.3. Constructivity

Lambda calculus is said to correspond to constructive logic. What is meant by constructive here?

Constructive logics require proofs to present evidence. Therefore, they do not accept principles like the law of the excluded middle and double negation elimination.

Trying to write a typed λ calculus program with a type that corresponds to \(\neg (\neg A) \rightarrow A\) is indeed rather impossible.

2. Polymorphism

2.1. Quantifier Positions

Explain the difference between a function of type \(\forall a.\ a \rightarrow a\) and \((\forall a.\ a) \rightarrow (\forall a.\ a)\).

The first function allows the caller to specify a type, and then the caller must provide a value of that type. As the function does not know what type the caller will specify, the only thing it can do to that value is return it.

The second function requires the caller to provide a value that the function could instantiate to any type, and will then return a value that the caller can instantiate to any type. As there is no way to construct a value of type \(\forall a.\ a\), this function is impossible to actually execute dynamically.

2.2. Parametricity

What can we conclude about the following functions solely from looking at their type signature?

\(f_1 : \forall a.\ [a] \rightarrow a\)
\(f_2 : \forall a.\ \forall b.\ [a] \rightarrow [b]\)
\(f_3 : \forall a.\ \forall b.\ [a] \rightarrow b\)
\(f_4 : [\texttt{Int}] \rightarrow [\texttt{Int}]\)

If the function returns at all, the output value must be one of the elements of the input list.
If the function returns at all, the output list is empty.
The function does not return.
Only that the output will be a list of integers, if the function returns at all.