7 Type Checker

This assignment has you implement a type checker for a Typed Paret.

7.1 Data Definitions

The syntax of Paret is extended to include types in some positions:

Some examples of Typed Paret programs are:

The abstract syntax of Paret is described by a few Pyret data definitions:

data Op:
  | op-plus
  | op-minus
  | op-times
  | op-divide
  | op-less
  | op-greater
  | op-equal
end

data UnOp:
  | op-first
  | op-rest
  | op-is-empty
end

data Type:
  | t-arrow(args :: List<Type>, ret :: Type)
  | t-num
  | t-bool
  | t-list(typ :: Type)
end

data Expr:
  | e-link(first :: Expr, rest :: Expr)
  | e-empty(typ :: Type)
  | e-unop(op :: UnOp, exp :: Expr)
  | e-num(n :: Number)
  | e-bool(b :: Boolean)
  | e-op(op :: Op, left :: Expr, right :: Expr)
  | e-if(cond :: Expr, consq :: Expr, els :: Expr)
  | e-let(binds :: List<Bind>, body :: Expr)
  | e-id(x :: String)
  | e-app(f-exp :: Expr, args :: List<Expr>)
  | e-lam(args :: List<Param>, body :: Expr)
end

data Bind:
  | bind(id :: String, expr :: Expr)
end

data Param:
  | param(id :: String, typ :: Type)
end

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

Type checking a Paret program can result in a type or raise an error:

data TypeError:
  | te-bad-arg
  | te-bad-link
  | te-non-fun
  | te-non-list
  | te-non-num
  | te-non-bool
  | te-bad-if
  | te-unbound-id
  | te-bad-equal
  | te-arity-mismatch
end

Your type-checker will also need a type environment:

type TypeEnv = SD.StringDict<Type>

7.2 Paret Semantics

You will define a a type-checker for Paret with a single function:

fun type-of(expr :: Expr, ty-env :: TypeEnv) -> Type:

7.2.1 Types and Their Meanings

Base Types

The base types, t-bool and t-num, correspond to the values v-bool and v-num, so if an expression would evaluate to the corresponding value, it has the corresponding type. So, for example, e-num(5) has type t-num, and (< 5 6) has type t-bool.

List Types

The List type corresponds to list values (both v-link and v-empty). A List type always comes with a type for its contents, even in the case of an empty list. The empty expression has been augmented to include the type of elements the list will contain. So, for example, this is invalid syntax:

(link 5 empty)

Instead, it should be written:

(link 5 (empty Num))

indicating that it contains a list of numbers.

In annotations, list types are written with surrounding parentheses and the element type:

(lam ((x : (List Num))) (first x))

Note that types can be nested, so you can have lists of lists and so on (what is the type of this example?):

(lam ((x : (List (List (List Num))))) (first x))

Arrow Types

Arrow types correspond to function values (v-clos). They have a list of argument types, and a return type. Syntactically, the arguments are written in a space separated list before an ASCII arrow, then the return type:

(lam ((f : (Num Bool -> Num))) (f 5 true))

A zero-argument function has nothing before the arrow:

(lam ((f : (-> Num))) (f))

7.2.2 Type-checking Expressions and Type Errors

• Binary Operators: The arithmetic operators check that their arguments are numbers (t-num), and have the resulting type t-num. The comparison operators are similar but result in t-bool. Both raise te-non-num if the arguments aren’t number-typed. The op-equal operator types to t-bool unless both arguments are functions, in which case it raises te-bad-equal.

• Unary Operators: All the unary operators raise t-non-list if the argument isn’t of list type. Then, first has the type of the elements of the list, rest has the same type as the list, and is-empty has type t-bool.

• Link and Empty: The (empty T) expression types to a list with elements of the provided type T. The link expression checks that the rest expression is of some list type T, and that the type of the first expression matches the type T. Link raises te-bad-link if the type of the first expression doesn’t match, and te-non-list if rest isn’t list-typed.

• If: If expressions raise te-non-bool if the conditional position isn’t boolean-typed. If both branches don’t match in type, it raises te-bad-if, and the whole expression has the matching type if they do match.

• Let: Let expressions calculate the type of each expression in their binds, and type-check their body in an environment with the names of bindings mapping to the corresponding types.

• Lam: Lambda expressions type-check their body in an environment with all the given names in params mapped to the corresponding types, and produce an appropriate t-arrow type.

• App: Application expressions raise te-non-fun if the funciton position isn’t arrow-typed. If it is, the application expression should check that the arguments match, and yield the appropriate return type.

7.3 Syntax Gotchas

Don’t forget that empty needs a type annotation. You will get an error that says "Bad use of keyword empty" if you do.

Don’t forget that lambdas now have an extra set of parens around each argument, and around the argument list as a whole.

7.4 Logistics

You have been provided two files:

• type-check-impl.arr, which contains your implementation of Paret.

• type-check-tests.arr, which will hold your external tests for the evaluator.

The files are at:

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

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

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

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

7.5 Testing and Submission Steps

By midnight Monday (March 2), you should submit 5-10 of what you think are the most interesting tests to Captain Teach at the cs91-type-check 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 Tuesday (March 3), 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.

On Tuesday, a set of different implementations will be released, with instructions for adding an import line to access and test the different implementations. The different implementations are available with:

import shared-gdrive("type-check-different-solutions.arr", "0B32bNEogmncOSTJyYWFKUlFLY1E") as S

The names are:

no-arity-mismatch
arrows-equal-ok
all-ops-num
ops-no-arg-check
heterogeneous-lists1
heterogeneous-lists2
heterogeneous-if
no-cond-check
arg-check-missing

By midnight Friday (March 6), 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. Keep in mind that there is a written assignment due at the same time, so manage your time appropriately.

7.6 Grading

Your grade will be in a few parts:

• 10% for submitting an interesting initial set of tests.

• 35% for the quality of your tests, based on the number of bad implementations they catch. As before, I reserve the right to grade based on additional bad implementations that I don’t release, so catching the ones that are out there does not guarantee a perfect testing score.

• 55% for the quality of your implementation, based on its correctness, clarity, and style.

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.