# Tute (Week 10)

## Table of Contents

## 1 Type Inference

In Assignment 2, you must make use of a
`TC`

monad, which contains the source of fresh names. Acquiring a fresh name
requires use of the `fresh`

action:

fresh :: TC Var

If we were to avoid using monads here, `fresh`

could instead be given a source
of fresh names `Source`

, and return a new `Source`

as the output.

fresh :: Source -> (Source, Var)

Sketch an implementation of the *function application* rule in the assignment spec,
but without using the `TC`

monad and instead using an explicit `Source`

:

tyInf :: Gamma -> Exp -> Source -> (Source, Exp, Type, Subst)

You may assume the existence of a `unify`

function that crashes if there is no unifier^{1},
and that all the substitution functions from the assignment are available: Substitutions may
be combined with `(<>)`

, created with `(=:)`

, and applied to environments with `substGamma`

and
to types with `substitute`

.

tyInf g (App e1 e2) s = let (s',t,e1',tau1) = tyInf g e1 s (s'',t',e2',tau2) = tyInf (substGamma t g) e2 s' (s''',alpha) = fresh s'' u = unify (substitute t' tau1) (Arrow tau2 alpha) in (s''', App e1' e2', substitute u alpha, u <> t <> t')

### 1.1 State Monads

Now sketch the same case (function application) but using a state monad:

fresh :: State Source Var tyInf :: Gamma -> Exp -> State Source (Exp, Type, Subst)

tyInf g (App e1 e2) = do (t,e1',tau1) <- tyInf g e1 (t',e2',tau2) <- tyInf (substGamma t g) e2 alpha <- fresh let u = unify (substitute t' tau1) (Arrow tau2 alpha) return (App e1' e2', substitute u alpha, u <> t <> t')

### 1.2 Linear Types

What does the state monad approach ensure in the previous question? How can we ensure
the same thing with *linear types*? Which types would be linear, and which would not?

The state monad hides the source of fresh names and prevents the same source from being used twice and thus ensures that all names are truly fresh.

Linear types could be used to achieve the same effect by making the `Source`

type
in the original, non-monadic code linear. As this would make it impossible to use
the same source twice, the same fresh names property is ensured.

## 2 Existential Types

Existential types are often over-used in langauges that support them. For each of the following existential types, propose a non-existential type that could be used instead:

- \(\exists t.\ t \times (t \rightarrow \texttt{String})\)
- \(\exists t.\ t \times (\texttt{Int} \times t \rightarrow t)\)
- \(\exists t.\ (t \rightarrow t \times t) \times (t \times t \rightarrow t)\)

- \(\texttt{String}\), seeing as consumers of the data type can only produce one string from a value of that type.
- \(\mathbf{1}\), seeing as there is no way to extract any information from that data type.
- \(\mathbf{1}\), seeing as there is no way to extract any information or indeed to construct an instance of the abstract data type.

## Footnotes:

^{1}

: Note that this differs from your assignment, where unify must raise type errors
and errors are also handled in the `TC`

monad.