Semester 2, 2018

# Tute (Week 10)

## 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 unifier1, 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')


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:

1. $$\exists t.\ t \times (t \rightarrow \texttt{String})$$
2. $$\exists t.\ t \times (\texttt{Int} \times t \rightarrow t)$$
3. $$\exists t.\ (t \rightarrow t \times t) \times (t \times t \rightarrow t)$$
1. $$\texttt{String}$$, seeing as consumers of the data type can only produce one string from a value of that type.
2. $$\mathbf{1}$$, seeing as there is no way to extract any information from that data type.
3. $$\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.

2018-11-16 Fri 19:37