## Description

## Programming Languages and Translators

1 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