Semester 2, 2018

# Tute (Week 9)

## 1 Polymorphism

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

### 1.2 Parametricity

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

1. $$f_1 : \forall a.\ [a] \rightarrow a$$
2. $$f_2 : \forall a.\ \forall b.\ [a] \rightarrow [b]$$
3. $$f_3 : \forall a.\ \forall b.\ [a] \rightarrow b$$
4. $$f_4 : [\texttt{Int}] \rightarrow [\texttt{Int}]$$
1. If the function returns at all, the output value must be one of the elements of the input list.
2. If the function returns at all, the output list is empty.
3. The function does not return.
4. Only that the output will be a list of integers, if the function returns at all.

## 2 Type Inference

### 2.1 Examples

What is the most general type of the following implicitly-typed MinHs expressions?

1. recfun f x = ((fst x) + 1)
2. InL (InR True)
3. recfun f x = if (fst x) then (snd x) else f x
4. recfun f x = if (fst x) then (InL x) else (InR x)

What would their explicitly-typed equivalents be?

1. $$\forall a.\ \texttt{Int} \times a \rightarrow \texttt{Int}$$
2. $$\forall a.\ \forall b.\ (b + \texttt{Bool}) + a$$
3. $$\forall b.\ (\texttt{Bool} \times b) \rightarrow b$$
4. $$\forall b.\ (\texttt{Bool} \times b) \rightarrow ((\texttt{Bool} \times b) + (\texttt{Bool} \times b))$$

The explicitly typed versions are:

1. type a. recfun f :: (Int * a -> Int) x = ((fst@Int@a x) + 1)
2. type a. type b. InL@(b + Bool)@a (InR@b@Bool True)
3. type b. recfun f x = if (fst@Bool@b x) then (snd@Bool@b x) else f x
4. type b. recfun f x = if (fst@Bool@b x) then (InL@(Bool * b)@(Bool * b) x) else (InR@(Bool * b)@(Bool * b) x)

### 2.2 Inference Algorithm

In the lecture, we introduced two sets of typing rules for an implicitly typed variant of MinHs. Explain the difference between these rules.

Derive the type of $$\mathtt{Apply}\ (\mathtt{Recfun}\ (f.x.\ \texttt{Pair}\ x\ x))\ 5)$$ using both sets of inference rules.

The first set of rules don't specify an algorithm, as several rules require us to guess what types to put in the context, and several other rules (forall introduction and elimination) can be applied at any time.

The second set of rules fixed that problem by allowing unification variables to occur inside types, standing for types that are not yet known. As we do type checking, whenever we want two types to be equal, we find a substitution to the unification variables such that the types become the same. In this way, as we complete type checking, we will generate a substitution that, when applied to the types, will produce the most general type for a given term.

I (Liam) did the derivation using the algorithmic rules here:

2018-11-16 Fri 19:37