►Introduction to Programming Languages
►Labs and Assignments
▼Labs
►9 Type Inference
On this page:
9.1 Data Definitions
9.1.1 Constraints
9.2 To Do
9.3 Testing
9.4 Logistics
9.5 Testing and Submission Steps
9.6 Grading
    ← prev  up  next → 
9 Type Inference

This assignment has you implement a type inferencer.

9.1 Data Definitions

The syntax of Paret is a bit more restricted, to only single-argument functions and fewer operations:

exp := (<op> <exp> <exp>)

    |  true

    |  false

    |  <number>

 

    |  (if <exp> <exp> <exp>)

 

    |  (lam (x) <exp>)

    |  (<exp> <exp> ...)

 

    |  (first <exp>)

    |  (rest <exp>)

    |  empty

    |  (link <exp> <exp>)

 

op   := + | <

id   := Any non-keyword symbol

The abstract syntax is:

data Expr:
  | e-link(first :: Expr, rest :: Expr)
  | e-first(val :: Expr)
  | e-rest(val :: Expr)
  | e-empty()
  | e-num(n :: Number)
  | e-bool(b :: Boolean)
  | e-plus(left :: Expr, right :: Expr)
  | e-less(left :: Expr, right :: Expr)
  | e-if(cond :: Expr, consq :: Expr, els :: Expr)
  | e-app(f :: Expr, arg :: Expr)
  | e-lam(arg :: String, body :: Expr)
  | e-id(x :: String)
end

This mostly maps one-to-one with the pieces of concrete syntax.

There are only two kinds of errors in inference:

data InferenceError:
  | type-mismatch
  | occurs-check
end
9.1.1 Constraints

There are a few data definitions for representing constraints:

data Constraint:
  | tyeq(left :: TyCS, right :: TyCS)
end

data TyCS:
  | t-id(x :: String)
  | t-expr(e :: Expr)
  | t-con(name :: String, args :: List<TyCS>)
end

In class we discussed 4 kinds of constraint components; this leaves out base types, which are represented by t-cons with no arguments. These conveniences are also defined to make constructing types easier:

fun t-arrow(args, ret):
  t-con("Arrow", [list: args, ret])
end
fun t-list(typ):
  t-con("List", [list: typ])
end
t-num = t-con("Num", empty)
t-bool = t-con("Bool", empty)

Note: We’re making an important assumption in this algorithm. This only works with the given representation of t-ids if there is no overlap between binding positions. That is, if an identifier is shadowed, or even appears bound in two different places, it confuses the algorithm. This isn’t a fundamental limitation (we could always rename the variables first), but it does mean that you shouldn’t bother testing cases where the same identifier is bound in two different places.

Do test things where an identifier is used more than once, like

"(lam (x) (+ x x))"

Don’t test things where it is bound more than once, like

"(lam (x) (lam (x) x))"

9.2 To Do

The high-level goal is to implement

infer-type :: String -> TyCS

Where the return is the simplest possible type (possibly underconstrained) for the provided expression.

Along the way, you’ll implement

generate-constraints :: # contract up to you
unify :: # contract up to you

The support code is set up with calls to these functions, but no signatures filled in. You should fill them in with the implementation from class and the book.

9.3 Testing

Type inference is a relation rather than a function: there are many ways and orderings for representing the constraints. In particular, the type output from infer-type could contain differently-named identifiers depending on how you handle lists, and a few other cases.

The assignment provides a function called normalize-type that takes a TyCS and produces a normalized version of it with all t-exprs and t-ids replaced consistently with type variables of the same name, starting with a. You should use normalize-type for testing against the reference solution (it can also be handy in the return of infer-type, but it’s not strictly necessary).

9.4 Logistics

You have been provided two files:

The files are at:

Code: https://code.pyret.org/editor#share=0B32bNEogmncOTFVOQ2ZnRGN0UlU&v=v0.5r852

Tests: https://code.pyret.org/editor#share=0B32bNEogmncOUGtmTEVGSHk3Q28&v=v0.5r852

Both files import the module type-infer-definitions.arr, which defines the data definitions and the helper function used by type-infer to parse strings to ASTs:

https://code.pyret.org/editor#share=0B32bNEogmncOMWp3YzZfRWVZcms&v=v0.5r852

9.5 Testing and Submission Steps

You can work with a partner on this assignment. You should do test submission and review separately, and then work together subsequently. Feel free to start working together before the Thursday test deadline, but do submit separate test suites. This is better for you: it forces you to see more diversity in tests.

Report to me by email by Thursday midnight if you’re working with a partner, and who; CC your partner. If you want to be randomly assigned a partner, I’ll try to accommodate, but since partners are optional, no promises.

By midnight Thursday (March 19), you should submit 5-10 of what you think are the most interesting tests to Captain Teach at the cs91-type-infer link from:

https://www.captain-teach.org/swarthmore-cs091/assignments/

Submit a single Pyret file with your test cases filled into the check block in the template file. If you’re budgeting your time over the weekend, you shouldn’t need to spend more than about an hour playing with the interpreter to come up with some interesting cases.

By midnight Friday (March 20), you should submit any reviews you were assigned. You should feel free to complete the reviews at any time before then, and they will be assigned as submissions come in.

Bad solutions have been released, their names are

heterogeneous-if
no-nested-arg-constraints
empty-has-any-type
lam-uses-expr-for-arg
link-equal
occurs-is-mismatch
forget-t-con-rest
underconstrained
no-apply-subst-in-right
overeager-occurs

They can be imported with:

import shared-gdrive("type-infer-different-solutions.arr", "0B32bNEogmncOYTY5ekotYV9GaG8") as B

By midnight Monday (March 30), you should submit a completed implementation of the interpreter, and a final test suite. Use the same submission link as above, but submit to the code step, which will unlock after you complete your reviews. Only one partner needs to submit.

9.6 Grading

Your grade will be in a few parts:

Peer reviews will not factor into your grade, though you are free to copy tests from others that you see during review. Please don’t share tests with one another outside of what’s provided during test review.

    ← prev  up  next →