$29
Assignment 5: Nano Types Solution
Overview
The overall objective of this assignment is to
better understand the notions of type checking, type inference, and polymorphism
by implementing a type inference algorithm for Nano.
The assignment is in the file:
+ [TypeCheck.hs](/src/Language/Nano/TypeCheck.hs)
and
+ [tests/Test.hs](/tests/Test.hs) has some sample tests,
and testing code that you will use to check your
assignments before submitting.
You should only need to modify the parts of the files which say:
```haskell
error "TBD: ..."
```
with suitable Haskell implementations.
**Note:** Start early! Type inference has many subtle points that can take a while to get right.
## Assignment Testing and Evaluation
Most of the points, will be awarded automatically, by
**evaluating your functions against a given test suite**.
[Tests.hs](/tests/Test.hs) contains a very small suite
of tests which gives you a flavor of of these tests.
When you run
```shell
$ stack test
```
Your last lines should have
```
All N tests passed (...)
OVERALL SCORE = ... / ...
```
**or**
```
K out of N tests failed
OVERALL SCORE = ... / ...
```
**If your output does not have one of the above your code will receive a zero**
If for some problem, you cannot get the code to compile,
leave it as is with the `error ...` with your partial
solution enclosed below as a comment.
The other lines will give you a readout for each test.
You are encouraged to try to understand the testing code,
but you will not be graded on this.
## Submission Instructions
Please commit all your code to gitlab, and indicate in your canvas submission your commit ID and your partner. We will be grading the code from gitlab, so ensure what you add to gitlab is what you want graded.
## Data Structures and Overview
This assignment builds upon our previous implementation of Nano from HW4,
so most data types in `Types.hs` are the same.
We have added the following definitions to support type inference.
Types
We will use the following Haskell datatypes to represent Nano's types and poly-types:
```haskell
data Type
= TInt -- Int
| TBool -- Bool
| Type := Type -- function type: T1 - T2
| TVar TVar -- type variable: a, b, c
| TList Type -- list type: [T]
data Poly = Mono Type -- mono-type
| Forall TVar Poly -- polymorphic type
```
where `TVar` is just a type alias for `String` used to represent type variable names:
```haskell
type Id = String
```
For example, a Nano type `Int - Int` is represented inside your type checker as:
```haskell
TInt := TInt
```
whereas a polymorphic Nano type `forall a . List a - a` is represented as:
```haskell
Forall "a" (Mono (TList (TVar "a") := TVar "a"))
```
(or simply `forall "a" (list "a" := "a")` using convenience functions `forall` and `list`, also defined in `Types.hs`).
Type Environment
A **type environment** is simply a dictionary that maps program variables to poly-types.
As before, the dictionary is implemented as a list of pairs:
```haskell
type TypeEnv = [(Id, Poly)]
```
Type Substitution
A **type substitution** is also a dictionary, but it maps *type variables* to *types* they should be replaced with:
```haskell
type Subst = [(TVar, Type)]
```
Throughout the assignment, make sure that the keys (type variables) in the substitution are *unique*.
You also get to *assume* this property when you implement operations on substitutions.
## Problem 1: Warm-up (70 points)
In this problem, you will implement some helper functions for your type-checker
which you will need later on.
(a) Free type variables: 20 points
First implement two functions that compute the list of *free type variables*
in a type and in a poly-type.
Note: to enable overloading (using a function with the same name for types and poly-types),
this function is defined as part of a type class `HasTVars`.
```haskell
instance HasTVars Type where
freeTVars t = error "TBD: ..."
instance HasTVars Poly where
freeTVars s = error "TBD: ..."
```
As always, you are allowed (and encouraged) to replace `freeTVars t` and `freeTVars s` with multiple equations for different patterns.
Throughout this assignment, you are allowed to use any library functions,
as long as you don't add new `import` statements.
In particular, some useful functions from the `List` library include `delete`, `nub`, and `\\` (look them up on Hoogle).
Note: the `List` library is imported *qualified*:
```haskell
import qualified Data.List as L
```
So whenever you want to use a function from that library, you have to prefix its name with `L.` (e.g. `L.delete`).
When you are done you should get the following behavior:
```haskell
freeTVars TInt
[]
freeTVars (TVar "a")
["a"]
freeTVars (forall "a" (list "a" := "a"))
[]
```
(b) Substitutions: 50 points
Implement a function to lookup what a type variable maps to in a substitution:
```haskell
lookupTVar :: TVar - Subst - Type
```
and a function to remove the mapping for a given type variable from a substitution
(recall that all variables in a substitution are supposed to be unique):
```haskell
removeTVar :: TVar - Subst - Subst
```
When you are done you should get the following behavior:
```haskell
lookupTVar "a" [("a", TInt)]
Int
lookupTVar "a" [("b", TInt)]
a
removeTVar "a" [("a", TInt)]
[]
removeTVar "a" [("b", TInt)]
[("b",Int)]
```
Next, use `lookupTVar` and `removeTVar` to write
two functions that *apply a substitution*
to a type and to a poly-type
(both named `apply`):
```haskell
instance Substitutable Type where
apply sub t = error "TBD: ..."
instance Substitutable Poly where
apply sub p = error "TBD: ..."
```
Once you have implemented this functionality and
recompiled, you should get the following behavior:
```haskell
apply [("a",TInt)] (list "a")
[Int]
apply [("a",TInt)] (forall "a" $ list "a")
forall a . [a]
```
Finally, use `apply` to implement the function `extendSubst`,
which extends a substitution with a new type assignment:
```haskell
extendSubst :: Subst - TVar - Type - Subst
```
When you are done you should get the following behavior:
```haskell
extendSubst [("a", TInt)] "b" TBool
[("b",Bool), ("a",Int)]
extendSubst [("a", list "b")] "b" TBool
[("b",Bool), ("a",[Bool])]
```
## Problem 2: Unification (50 points)
Unification is a crucial part of type inference.
In a nutshell, the inference algorithm works by:
* recursively traversing the program, assembling expression types from the types of their sub-expressions;
* when some type is not yet known, it picks a **fresh type variable** to represent this type;
* whenever two types must be the same, the algorithm tries to **unify** them and figure out what these type variables actually stand for.
A *fresh type variable* is a type variable that is distinct from all type variables the algorithm has generated before.
Our implementation will name the fresh type variables `a0, a1, ...`.
In order to remember the index of the first unused fresh varaible,
we introduce a new datatype:
```haskell
data InferState = InferState {
stSub :: Subst -- ^ current substitution
, stCnt :: Int -- ^ number of fresh type variables generated so far
}
```
which represents the "current state" of the unification and inference algorithms.
It remembers how many fresh type variables the algorithm has generated so far,
alongside the "current substitution".
(a) Unification for type variables: 20 points
Implement a function `unifyTVar st a t`
that tries to unify a type variable `a` with a type `t`.
If it succeeds, it records the new type assignment by extending the state `st`.
If it fails, it throws an exception.
```haskell
unifyTVar :: InferState - TVar - Type - InferState
```
You can use a helper function `extendState` to extend a substitution inside a state.
**Assumption:**
You can *assume* that `a` does not appear in the *domain* of `stSub st`
(i.e. among the type variables it maps);
remember to *guarantee* this property whenever you call `unifyTVar`.
When you are done you should get the following behavior:
```haskell
stSub $ unifyTVar initInferState "a" (list "b")
[("a",[b])]
stSub $ unifyTVar initInferState "a" "a"
[]
stSub $ unifyTVar initInferState "a" (list "a")
*** Exception: Error {errMsg = "type error: cannot unify a and [a] (occurs check)"}
```
(b) Unification for types: 30 points
Implement a function `unify st t1 t2`
that tries to unify the types `t1` and `t2`.
If it succeeds, it records the new type assignment by extending the state `st`.
If it fails, it throws an exception.
```haskell
unify :: InferState - Type - Type - InferState
```
**Assumption:**
You can *assume* that any type variables in `t1` and `t2` do not appear in the domain of `stSub st`;
remember to *guarantee* this property whenever you call `unify`.
When you are done you should get the following behavior:
```haskell
stSub $ unify initInferState TInt TInt
[]
stSub $ unify initInferState TInt TBool
*** Exception: Error {errMsg = "type error: cannot unify Int and Bool"}
stSub $ unify initInferState ("a" := TInt) (TBool := "b")
[("b",Int),("a",Bool)]
stSub $ unify initInferState (list "a") (list $ list "a")
*** Exception: Error {errMsg = "type error: cannot unify a and [a] (occurs check)"}
```
## Problem 3: Type Inference (120 points)
Now we have everything in place to implement type inference!
(a) Mono-types: 20 points
Let's first consider the fragment of the language without:
* binary operators
* conditionals
* let polymorphism
* recursion
* lists
Implement the function `infer st gamma e` for this fragment.
This function attempts to infer the type of `e` in type environment `gamma`
given that the current state is `st`.
If `e` imposes constraints on the types of its sub-expressions,
`infer` calls `unify` to enforce these constraints.
If all unification steps succeed, `infer` returns the inferred type of `e` and a new state
(possibly extended with new type assignments generated during unification).
In this part, you can assume that the type environment maps all variables to mono-types, i.e. `Mono t`.
When you are done, and replace `Lexer.x` and `Parser.y` with a working lexer and parser from HW4,
your code should pass the first 5 test cases.
In particular, you should observe the following behavior:
```haskell
typeOfString "True"
Bool
typeOfString "1"
Int
typeOfString "(\\x - x) 5"
Int
typeOfString "(\\x - x + 1) True"
*** Exception: Error {errMsg = "type error: cannot unify Int and Bool"}
```
**Note:** if you don't have a working Nano parser yet, use the function `typeOfExpr` instead and write ASTs by hand.
(b) Polymorphism: 50 points
Now let's add support for polymorphism!
* In this version, variables in the type environment can have polymorphic types, like `forall a . a - a`.
* Whenever we use a variable, we have to **instantiate** its poly-type,
i.e. replace all bound type variable with *fresh free type variables*.
* Whenever we define a variable using a `let`,
we have to **generalize** its type into a poly-type.
First implement the function `generalize gamma t` that generalizes `t` into a poly-type,
i.e. binds all its type variables that are *not free* in `gamma` with a `Forall`:
```haskell
generalize :: TypeEnv - Type - Poly
```
When you are done you should observe the following behavior:
```haskell
generalize [] ("a" := "a")
forall a . (a) - a
generalize [("x", Mono "a")] ("a" := "a")
(a) - a
```
Next implement the function `instantiate n s` that instantiates a poly-type `s`
by replacing its bound type variables with fresh type variables.
Here `n` is the index of the first unused fresh type variable.
```haskell
instantiate :: Int - Poly - (Int, Type)
```
**Assumption:**
In `instantiate n s`, you can assume that bound type variables in `s`
cannot clash with `ai` where `i = n`.
Remember to *guarantee* this property whenever you construct your own polymorphic types.
When you are done you should observe the following behavior:
```haskell
instantiate 0 (Forall "a" (Forall "b" ("a" := "b")))
(2,(a0) - a1)
```
Finally, modify the function `infer` to support polymorphism.
When you are done, your implementation should be able to
type-check the "double identity" example from the lecture:
```haskell
typeOfString "let id = \\x - x in let y = id 5 in id (\\z - z + y)"
(Int) - Int
```
(c) Built-in functions: 20 points
Instead of implementing separate type inference for binary operators, conditionals, and list,
we decided to represent them as **built-in functions**
and reuse the type inference for variables and function application.
Fill in the types of built-in functions inside `preludeTypes`
(we have pre-filled the one for `+`).
Remember that you are not allowed to use `a0, a1, ...` as bound type variables,
since those are reserved for use as free type variables by the algorithm.
At this point the first 18 tests should pass.
(d) Recursion: 30 points
Modify your implementation of `infer` to support recursive function definitions.
Once you are done, all tests should pass.
