HW#7 Type Inference Solution

1 Instructions




Begin by downloading the file hw7-base.ml from the course website and renaming it to hw7.ml. This file contains the functions that you will use and modify in the homework. You will need to add cases to gather constraints, but you should not need to modify any of the other predefined functions. Submit your completed hw7.ml via Gradescope. As always, please don’t hesitate to ask for help on Piazza (https://piazza.com/class/ jkh8q52qrh06v).







2 Type Inference for a Functional Language




The file hw7-base.ml defines a type exp of expressions for a simple OCaml-like language. It also defines a function get constraints that performs (the first half of ) type inference for this language: get constraints gamma e returns either None, if e fails to typecheck, or Some (t, c), where t is a type with type variables, and c is a list of constraints (pairs of types with variables) that must be satisfied for t to be a correct type for e. The following problems will ask you to extend the get constraints function to handle the rest of the language.

You can test your code using the infer type function, which takes an exp and infers its type using your get constraints function and a pre-written unify function. The inferred type may have variables in it, if there is more than one possible type for the expression: for instance, infer type (Fun ("x", Var "x")) might return something like Some (Tarrow (Tvar 3, Tvar 3)), indicating that fun x - x could have type a

- a for any type a.







3 Problems




1. (2 points) Extend the provided get constraints function to handle integer and boolean literals, according to the following rules:







(i is an integer) Γ ` i : int | {}

(b is a boolean) Γ ` b : bool | {}






Once you have completed this problem, infer type (Int 3) should return Some

Tint.




2. (5 points) Extend the provided get constraints function to handle addition and comparison, according to the following rules:







Γ ` e1 : τ1 | C1 Γ ` e2 : τ2 | C2

Γ ` e1 + e2 : int | {τ1 = int, τ2 = int} ∪ C1 ∪ C2

Γ ` e1 : τ1 | C1 Γ ` e2 : τ2 | C2

Γ ` e1 = e2 : bool | {τ1 = τ2} ∪ C1 ∪ C2




Once you have completed this problem, infer type (Fun ("x", Fun ("y", Add

(Var "x", Var "y")))) should return Some (Tarrow (Tint, Tarrow (Tint, Tint))).




3. (5 points) Extend the provided get constraints function to handle if-then-else expressions, according to the following rule:







Γ ` e : τ | C Γ ` e1 : τ1 | C1 Γ ` e2 : τ2 | C2

Γ ` if e then e1 else e2 : τ1 | {τ = bool, τ1 = τ2} ∪ C ∪ C1 ∪ C2




Once you have completed this problem, infer type (Fun ("x", Fun ("y", If

(Eq (Var "x", Var "y"), Var "x", Int 3)))) should return Some (Tarrow (Tint, Tarrow (Tint, Tint))).




4. (6 points) Extend the provided get constraints function to handle expressions involving tuples, according to the following rules:







Γ ` e1 : τ1 | C1 Γ ` e2 : τ2 | C2

Γ ` (e1, e2) : τ1 ∗ τ2 | C1 ∪ C2




Γ ` e : τ | C τ1 , τ2 fresh

Γ ` fst e : τ1 | {τ = τ1 ∗ τ2} ∪ C

Γ ` e : τ | C τ1, τ2 fresh

Γ ` snd e : τ2 | {τ = τ1 ∗ τ2 } ∪ C



You can use the function fresh tident : unit - tident to create a new fresh type variable. Once you have completed this problem, infer type (Fun ("x", Add (Fst (Var "x"), Snd (Var "x")))) should return Some (Tarrow (Ttuple (Tint, Tint), Tint)).




5. (7 points) Extend the provided get constraints function to handle expressions involving sum types and pattern matching, according to the following rules:












Γ ` e : τ | C τ2 fresh

Γ ` inl e : τ + τ2 | C

Γ ` e : τ | C τ1 fresh

Γ ` inr e : τ1 + τ | C



Γ ` e : τ | C Γ[x1 7→ τl ] ` e1 : τ1 | C1 Γ[x2 7→ τr ] ` e2 : τ2 | C2 τl , τr fresh

Γ ` (match e with inl x1 → e1 | inr x2 → e2) : τ1 | {τ = τl + τr , τ1 = τ2 } ∪ C ∪ C1 ∪ C2




Once you have completed this problem, infer type (Fun ("x", Match (Var "x", "a", Eq (Var "a", Int 3), "b", Var "b"))) should return Some (Tarrow (Tsum (Tint, Tbool), Tbool)).