# CS 440 Homework 5 Types and Unification solution

\$30.00

Category:

5/5 - (4 votes)

## Programming Languages and Translators1 STLC

In this section, refer to the syntax and typing rules for the Simply-typed λ calculus, given in lecture.
Task 1.1 (Written, 12 points).
Give the STLC types of the following expressions:
(a) λx : unit.x
(b) ((), λx : unit.x)
(c) λx : unit.(x, x)
(d) snd ((),())
1
Task 1.2 (Written, 9 points).
Give a typing derivation for • ` λf : unit → (unit × unit).fst (f ()) : (unit → (unit × unit)) → unit.
Updated Apr. 16 : Resulting type was fixed

## 2 MiniCaml

Image Credit: Petr Kratochvil
In this section, we will be working with MiniCaml, a language with more features than MicrOCaml from
Homeworks 3 and 4, but still not quite all the features of OCaml.
The grammar of MiniCaml is shown below.
op → + | – | * | / | < | ≤ | > | ≥ | = | <> | && | || | ^
τ → int | string | bool | unit | τ list | τ -> τ | τ * τ
e → var | num | string | true | false | () | [] | e op e | fun var -> e | if e then e else e
| let pat optannot = e in e | let var pat optannot = e in e
| let rec var pat optannot = e in e | let (var , var ) = e in e | e e
| match e with [] -> e | var::var -> e | e, e | e::e | e : e
pat → var | (var : τ )
optannot →  | : τ
decl → let pat optannot = e;; | let var pat optannot = e;; | let rec var pat optannot = e;; | e;;
prog → decl | decl prog

You may notice that you can actually write a pretty large subset of OCaml in MiniCaml without making
any changes. In particular, we’ve gotten rid of MicrOCaml’s odd app e to e syntax and replaced it with
normal OCaml application. One nice result of this is that, while you can’t necessarily take any OCaml
program and run it in MiniCaml, you can run any MiniCaml program through OCaml (ocaml or TryOCaml)
to figure out what types it should have or what the result should be. A couple non-obvious restrictions present
in MiniCaml:
1. Pattern matching is limited to using let to break apart pairs and using match to match on a list (note
that we haven’t defined fst or snd: you have to break apart pairs with pattern matching; you can
define them yourself though).
2 CS 440

2. Functions (both lambdas and let-defined functions) can only take one argument. You can get around
this with currying (though that doesn’t work well for recursive functions) or having functions take
pairs (see map in examples/rec.ml).
3. As in OCaml, a program consists of one or more top-level declarations, where a declaration can be a
let declaration or an expression by itself. Unlike in OCaml, these declarations must be followed by
two semicolons (see the midterm for why this makes our lives easier writing the parser).
4. You can’t use type variables in annotations (e.g. let f (x: ’a) : ’a = x. MiniCaml can still
infer polymorphic types with type variables though.
The type definitions for MiniCaml are given in types.ml and described in the walkthrough video on
Blackboard.

The file unify.ml contains code to unify two types, which is used in type checking. Unification in
MiniCaml works very similarly to unification in STLC, with a couple of extensions. Recall that unification
takes two types τ1 and τ2, potentially with unification variables like ?1. These are “holes” that can be unified
with anything. Each instance of a particular variable must be filled with the same thing though (for example,
if ?1 appears in both types, you must replace ?1 with the same type in both). In class, we considered an
imperative version of unification that “magically” updates unification variables. On this homework, we’ll
consider a functional unification algorithm that instead returns a substitution, which is a list of pairs (?i
, τi)
meaning “replace ?i with τi” (Updated 4/14 : Typo fix). As with substituting values for variables, we can
write [τi/?i

]τ to mean “τ with all instances of ?i replaced by τi
.” For a substitution σ, we’ll write [σ]τ to
mean “τ with all the replacements in σ”. So, for example,
[[(?0, int); (?1, string)]](?0 -> ?1) = int -> string
and
[[(?0, ?1 list); (?1, int)]]?0 = int list
The OCaml definition for substitutions is given in unify.ml:
type substitution = (int * typ) list
In that definition, ?0 is represented as just the integer 0. We also include a function sub all :
substitution -> typ -> typ,where sub all s t computes [s]t.
Here’s the (recursive) unification algorithm:
Algorithm: Unify(τ1, τ2)

Returns a substitution or an error.
1. If τ1 and τ2 are both the same base type (int, string, bool or unit), return the empty list [].
2. If τ1 = τ2 =?i (i.e., they are the same unification variable), return [].
3. If τ1 =?i
, then:
(a) If ?i occurs in τ2, then error.
(b) Otherwise, return [(?i
, τ2)].
4. If τ2 =?i
, then:
(a) If ?i occurs in τ1, then error.
(b) Otherwise, return [(?i
, τ1)].

Updated 4/13 : the return values of these two cases were swapped
5. If τ1 = τ
0
1 list and τ2 = τ
0
2 list, then return Unify(τ
0
1
, τ
0
2
)
6. If τ1 = τ
0
1 -> τ
00
1 and τ2 = τ
0
2 -> τ
00
2

then let σ = Unify(τ
0
1
, τ
0
2
) and return σ concatenated with
Unify([σ]τ
00
1
, [σ]τ
00
2
).
3
7. Similar to above for if τ1 = τ
0
1 * τ
00
1 and τ2 = τ
0
2 * τ
00
2

8. Otherwise, error.
Case 6 above is worth discussing in more detail. When we unify τ
0
1 and τ
0
2
, we get a substitution σ, which
gives us several substitutions we need to perform. We need to perform those substitutions immediately
on τ
00
1 and τ
00
2 before unifying them, because σ might tell us something like “replace ?0 with unit”, and τ
00
1
might have ?0 in it. To make this clearer, suppose τ1 = int -> string and τ2 =?0 -> ?0. Then, we
have τ
0
1 = int, τ 00
2 =?0, τ 00
1 = string and τ
00

2 =?0. When we unify int and ?0, we get the substitution
[(?0, int)]. If we then go ahead and unify string and ?0, we’d get the substitution [(?0, string)]. Now,
we have to somehow reconcile these two substitutions, which of course isn’t possible because ?0 can’t be
both int and string. Instead, we unify [[(?0, int)]]string = string and [[(?0, int)]]?0 = int, which gives
us an error (which is what we want because these two types can’t be unified.)

## Task 2.1 (Written, 14 points).

For each of the following pairs of types, say whether or not the two types can be unified. If they can,
give the substitution that results. If not, briefly (in one sentence or so) describe why not.
(a) int * ?1 ?2
(b) int * ?1 ?2 * string
(c) int * ?1 ?1 * string
(d) int -> ?1 string -> ?2
(e) ?1 -> ?2 ?3 * ?4
(f) ?1 list ?2 list list
(g) ?1 list ?1
Task 2.2 (Programming, 15 points).
Implement the function unify : typ -> typ -> typ in unify.ml, following the algorithm above.
The file unify.ml also contains one other function you might want: new type : unit -> typ generates
a new type consisting of just a unification variable ?n where ?n hasn’t been used in the program before. This
is useful for when we need to “guess” types to unify later.
The file typecheck.ml includes code to typecheck MiniCaml programs. It uses the unification function
you wrote above. We did most of the work, you just need to implement one small function that infers the
types of constants.

## Task 2.3 (Programming, 5 points).

Implement the function type of const : const -> typ in typecheck.ml. The function should return the type of the given constant. You shouldn’t need to do any unification. In the case of Nil, which
represents the empty list [], the type is of course τ list for some τ . What’s τ? We have no way of
knowing at this point, so you’ll just have to take a guess…
You can use new type, as well as any other functions from unify.ml.
2.1 Testing
You can write tests using assert in the files you edited, as usual. When you’re done, you can also use
make
to compile all of the code we gave you, which together makes a typechecker and interpreter for MiniCaml.
You can run it using
./miniml
Where is a MiniCaml file. We’ve given you several examples in examples, as well as several
examples that should not typecheck in examples/error. MiniCaml will read in the file, typecheck all of the
declarations, print out their types, and then evaluate them and print out their values (as in the OCaml
toplevel, functions will not be printed). For example:
4 CS 440
\$./miniml examples/rec.ml
sum: int list -> int
length: ’a list -> int
map: (’d -> ’c * ’d list) -> ’c list
int_to_string: int -> string
onetwothree: string list
sum =
length =
map =
int_to_string =
onetwothree = (one)::((two)::((three)::([])))
\$
You can also use MiniCaml like the OCaml toplevel by giving no arguments:
\$ ./miniml
Welcome to MiniCaml. Type #quit;; to exit.
# 3;;
-: int
– = 3
# (3, “Hi!”);;
-: int * string
– = (3, “Hi!”)
# fun x -> x;;
-: ’b -> ’b
– =
# #quit;;
3 Standard Written Questions
Task 3.1 (Written, 0 points).
How long (approximately, in hours/minutes of actual working time) did you spend on this homework,
total? Your honest feedback will help us with future homeworks.
Task 3.2 (Written, 0 points).
Who, if anyone, did you collaborate with (and in what way), and what outside sources, if any, did you
consult in working on this homework?
5 CS 440 Homework 5