►Fall 2019:
Programming Languages
►7 Assignments
▼7.3 Implementation
►7.3.5 A:   Type Inference
On this page:
7.3.5.1 Language
7.3.5.2 Terms
7.3.5.3 Types
7.3.5.4 Constraint Generation
7.3.5.5 Unification
7.3.5.6 Exceptions
7.3.5.7 Testing
7.3.5.8 Stencil Code
7.3.5.9 Submission
    ← prev  up  next → 
7.3.5 A: Type Inference

In this assignment, you will implement the type inference algorithm we studied in class. Concretely, you will implement the function
type-infer :: S-Exp -> Type
that implements type-inference for Paret. If the program does not have a type, the algorithm raises an exception.

7.3.5.1 Language

We will continue to use the Paret language from C: Type Checker except that the annotations on both lam and empty expressions have been removed: putting them back in is, after all, the job of type inference.

The parser we provide produces an LExpr, which is exactly the same as an Expr except that it has an additional label field and e-lams also have a param-label field. These labels are used to stand for program points in the type-inference algorithm.

You can keep track of the identifier labels using the provided LEnv, which maps Symbol to Label (where Label is an alias for Symbol). For convenience, we also provide a get-label function that consumes a LExpr and produces its label.

7.3.5.2 Terms

The language of terms is as follows:
(define-type Term
        (t-var [label : Label])
        (t-con [head : Symbol] [args : (Listof Term)]))
A term variable (t-var ’g123) can be read as “the type of the expression (or program position) labelled ’g123”. A term constructor (t-con head args) builds up a more complicated term from a list of subterms. For example, (t-con ’-> (list (t-var ’g123) (t-var ’g123))) is a representation of the more familiar ’a -> ’a. Primitives are also represented this way, e.g., (t-con ’Num empty) is a representation of the type Num.

For convenience, we provide helper functions to simulate the Type language of C: Type Checker in the language of Term. For example, (t-num) produces (t-con ’Num empty); t-num, t-bool, t-str, t-fun, and t-list are all provided. Note that because these are helper functions and not type variants, you will not be able to match against them in type-case.

7.3.5.3 Types

Observe that we now have type variables (represented as t-var) in our type language.

7.3.5.4 Constraint Generation

Constraints relate program subexpressions by stating how they work together in a successful execution.

The language of constraints is:
(define-type Constraint
        (eq [l : Term] [r : Term]))

Constraints equate two terms, often a type variable to the type of some other expression. For example, (eq (t-var ’g123) (t-num)) is a constraint that would be generated for the expression (e-num ’g123 5).

7.3.5.5 Unification

Given a consistent set of constraints, we try to unify them in such a way that every t-var gets assigned the correct type. It is important that unification always terminate, so you should perform an occurs check that fails given a circular constraint. Make sure you can construct a test case for this!

7.3.5.6 Exceptions

The full set of exceptions is as follows:
(define-type TypeInferenceError
  (ti-err-fails-occurs-check [replace : Term] [with : Term])
  (ti-err-constructor-mismatch [t1 : Term] [t2 : Term])
  (ti-err-unbound-id [name : Symbol]))

Given the constraint (eq replace with), you should (raise-error (ti-err-fails-occurs-check replace with)) if replace is a strict subterm of with.

Given the constraint (eq t1 t2), you should (raise-error (ti-err-constructor-mismatch t1 t2)) if t1 and t2 are t-cons with different head symbols.

7.3.5.7 Testing

Unlike C: Type Checker,

your type-inferencer can produce types with variables, e.g., the term (lam x x) might produce (t-fun (t-var ’g123) (t-var ’g123)). Since labels are random, writing tests for types with variables can be difficult.

For convenience, we provide a function
normalize :: Term -> Term
that consumes a term and renames all type variables to be lowercase letters in alphabetical order relative to how they appear in the term. For example, normalizing the type inferred for (lam x (lam y empty)) will produce
(t-fun (t-var 'a) (t-fun (t-var 'b) (t-list 'c)))

7.3.5.8 Stencil Code
7.3.5.9 Submission

Form

    ← prev  up  next →