Tyyppi-käsite?

• mitä eri näkemyksiä (eriäviä mielipiteitä) löytyy?
• mikä on samaa?
• mihin päädyt itse?

\[ \lambda x : \mathbf{Num} \to \mathbf{Bool}\cdot x \,3 \]

Sample solution to Exercise 9

Question: Does \(\lambda x : \mathbf{Num} \cdot x\,3\) have the type \(\mathbf{Num}\to\mathbf{Num}\)?

Since the term in question does not have free variables, we can use an empty type environment. Thus, we will build an inference tree for the following type judgment:

\[ \begin{gathered} \vdash (\lambda x : \mathbf{Num} \cdot x \, 3) : \mathbf{Num} \to \mathbf{Num} \end{gathered} \]

This is an abstraction and thus we can use rule (3), mutatis mutandis:

\[ \begin{gathered} x : \mathbf{Num} \vdash x\,3 : \mathbf{Num} \\ \hline \vdash (\lambda x : \mathbf{Num} \cdot x \, 3) : \mathbf{Num} \to \mathbf{Num} \end{gathered} \]

The topmost judgment matches rule (2):

\[ \begin{gathered} \begin{gathered} x : \mathbf{Num} \vdash x : \mathbf{Num} \to \mathbf{Num} \qquad x : \mathbf{Num} \vdash 3 : \mathbf{Num}\\ \hline x : \mathbf{Num} \vdash x\,3 : \mathbf{Num} \end{gathered}\\ \hline \vdash (\lambda x : \mathbf{Num} \cdot x \, 3) : \mathbf{Num} \to \mathbf{Num} \end{gathered} \]

The judgment \(x : \mathbf{Num} \vdash 3 : \mathbf{Num}\) matches axiom (1) and thus earns a line above it:

\[ \begin{gathered} \begin{gathered} x : \mathbf{Num} \vdash x : \mathbf{Num} \to \mathbf{Num} \qquad \begin{gathered} \hline x : \mathbf{Num} \vdash 3 : \mathbf{Num} \end{gathered}\\ \hline x : \mathbf{Num} \vdash x\,3 : \mathbf{Num} \end{gathered}\\ \hline \vdash (\lambda x : \mathbf{Num} \cdot x \, 3) : \mathbf{Num} \to \mathbf{Num} \end{gathered} \]

But the judgment \(x : \mathbf{Num} \vdash x : \mathbf{Num} \to \mathbf{Num}\) matches no rule: the only possible choice is axiom (1), but the types given for \(x\) on both sides of the \(\vdash\) do not match. Thus, we must answer the question in the negative:

Answer: No, \(\lambda x : \mathbf{Num} \cdot x\,3\) does not have the type \(\mathbf{Num}\to\mathbf{Num}\).

Sample solution to Exercise 10

Question: What is the type of \(\lambda x \cdot x\,3\)?

Answering this question requires us to discover some type to give to the bound variable \(x\) that makes the term well-typed. We will start by inventing a type variable for it and for the term's type; as before, we can start with an empty type environment.

\[\vdash (\lambda x \colon \alpha \cdot x\,3) : \beta\]

This matches rule (3). Let us choose \(\gamma\) so that \(\beta = \alpha \to \gamma\).

\[ \begin{gathered} x \colon \alpha \vdash x\,3 : \gamma \\ \hline \vdash (\lambda x \colon \alpha \cdot x\,3) : \beta \end{gathered} \]

The new judgment is an application and matches rule (2); let us choose \(\delta\) for the "U" type.

\[ \begin{gathered} \begin{gathered} x : \alpha \vdash x : \delta \to \gamma \qquad x : \alpha \vdash 3 : \delta \\ \hline x : \alpha \vdash x\,3 : \gamma \end{gathered}\\ \hline \vdash (\lambda x : \alpha \cdot x\,3) : \beta \end{gathered} \]

The topmost leftmost judgment matches (1), if \(\alpha = \delta \to \gamma\) and the topmost rightmost judgment matches (4), if \(\delta = \mathbf{Num}\):

\[ \begin{gathered} \begin{gathered} \begin{gathered} \hline x : \alpha \vdash x : \delta \to \gamma \end{gathered} \qquad \begin{gathered} \hline x : \alpha \vdash 3 : \delta \end{gathered}\\ \hline x : \alpha \vdash x\,3 : \gamma \end{gathered}\\ \hline \vdash (\lambda x : \alpha \cdot x\,3) : \beta \end{gathered} \]

Let us collect the equations we have amassed:

\[ \begin{aligned} \beta &= \alpha \to \gamma \\ \alpha &= \delta \to \gamma \\ \delta &= \mathbf{Num} \end{aligned} \]

It is obvious, then, that \(\alpha = \mathbf{Num} \to \gamma\) and \(\beta = (\mathbf{Num} \to \gamma) \to \gamma\). But we are unable to eliminate the type variable \(\gamma\); it means that the term has an infinite number of possible types, determined by the type chosen for the bound variable.

Answer: The term \(\lambda x \cdot x\,3\) can be completed into a simply-typed term by giving \(x\) any function type whose parameter type is \(\mathbf{Num}\); the term's type is a function from that function type to the result type of that function type; in other words, whatever type is chosen for \(\alpha\), the type of \(\lambda x : \mathbf{Num} \to \alpha \cdot x\,3\) is \((\mathbf{Num} \to \alpha) \to \alpha\).