Type Checker For Paret

In this assignment, you will implement a type checker for Paret, which has been augmented with type annotations on function parameters.

1. Type Checker

You will write a function fun type-of(e :: Expr) -> Type that takes a Paret program and either returns the type of that program or -- if the program is not well-typed -- raises an exception.

Similar to how you passed an Env around in the interp-fun assignment that mapped identifiers to values, to type-check you will want to pass around a type environment (TEnv, defined below) that maps identifiers to types.

We have defined a function fun type-check(prog :: String) -> Type that calls parse and then type-of: you can use type-check in your test cases to avoid calling C.parse manually.

2. The Language

The language has been simplified in a few ways. Strings and records have been completely removed, functions are single-arity, and let expressions always bind exactly one identifier. There are also additions to the language: lists have been added, together with operations empty, link, is-empty, first, and rest for working with them. Type annotations are included on function parameters, as documentated in the grammar. This language does not have syntactic sugar, so it contains let expressions that your type-checker will handle.

2.1 Types

The type of numbers is written Num, and the type of booleans is written Bool. The type of a list is written like (List Num), which in this case is the type of a list of numbers. The type of a function is written like (Num -> Num), where the type before the arrow is the argument type and the type after the arrow is the result type. Both of these examples are simple, but types can be nested as well, e.g., (List (List Num)).

2.2 Annotations

Function definitions are now annotated with the types of their arguments. For instance, the function that adds one to its argument could be written,

(let ((one 1)) (lam (x : Num) (+ x one)))

See the grammar for reference.

2.3 List Operations

You will need to type-check the five list operations, empty, link, is-empty, first, and rest. Lists in this language are homogeneous: all of their elements must have the same type. Here are the rules for type-checking the list operations:

If any of the arguments to these functions have the wrong type, your type-checker should raise a tc-err-bad-arg-to-op exception. So for instance, (link 2 3) should raise a tc-err-bad-arg-to-op exception, as should (link 2 (empty : Bool)). If the type of the first argument to link doesn't match the element-type of its second argument, have the arg-type of the error be the type of the first argument.

2.4 If Statements

Your type-checker should require that both branches of an if statement have the same type. So, for instance, (if 3 "three") will not type-check. See "Type-Checking Exceptions" for the error to raise.

2.5 Subtyping

You do not need to implement function subtyping, and should not write test cases that assume it will be implemented. Thus when checking that a function or let argument has an expected type, and that type is a function type, you may reject any argument whose type is not an identical function type.

2.6 Type-Checking Exceptions

Most of the exceptions your type-checker can raise are just like interpreter errors from previous assignments, but store a type instead of a value. There are two new kinds of exceptions, though:

If a program has multiple type errors, you should raise the leftmost one. (So type-check subexpression from left to right.)

Here is the full list of exceptions:

data TypeCheckingError:
  | tc-err-if-got-non-boolean(cond-type :: Type)
  | tc-err-bad-arg-to-op(op, arg-type :: Type) # op is Operator or UnaryOperator
  | tc-err-unbound-id(name :: String)
  | tc-err-not-a-function(func-type :: Type)

  | tc-err-bad-arg-to-fun(func-type :: Type, arg-type :: Type)
  | tc-err-if-branches(then-type :: Type, else-type :: Type)
end

3. Grammar

Note: you must put spaces around ":" and "->" for them to parse correctly.

Here is the new grammar:

<expr> ::= <num>
         | <id>
         | true | false
         | (+ <expr> <expr>)
         | (num= <expr> <expr>)
         | (link <expr> <expr>)
         | (if <expr> <expr> <expr>)
         | (lam (<id> : <type>) <expr>)
         | (let ((<id> <expr>)) <expr>)
         | (<expr> <expr>)
         | (first <expr>)
         | (rest <expr>)
         | (is-empty <expr>)
         | (empty : <type>)

<type> ::= Num
         | Bool
         | (List <type>)
         | (<type> -> <type>)

4. Abstract Syntax

Here are the extended data definitions:

data Expr:
  | e-op(op :: Operator, left :: Expr, right :: Expr)
  | e-un-op(op :: UnaryOperator, expr :: Expr)
  | e-if(cond :: Expr, consq :: Expr, altern :: Expr)
  | e-let(name :: String, expr :: Expr, body :: Expr)
  | e-lam(param :: String, arg-type :: Type, body :: Expr)
  | e-app(func :: Expr, arg :: Expr)
  | e-id(name :: String)
  | e-num(value :: Number)
  | e-bool(value :: Boolean)
  | e-empty(elem-type :: Type)
end

data Operator:
  | op-plus
  | op-num-eq
  | op-link
end

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

data Type:
  | t-num
  | t-bool
  | t-fun(arg-type :: Type, return-type :: Type)
  | t-list(elem-type :: Type)
end

type TEnv = List<TypeCell>

data TypeCell:
  | type-cell(name :: String, var-type :: Type)
end

(For reference, feel free to look at the definitions file.)

5. Submission

To get started, open the

code stencil

and the

test stencil

For your final submission, upload a zip file containing both your test and code files to Captain Teach. Call the files "type-checker-tests.arr" and "type-checker-code.arr". Double-check the file names before submitting; for instance they should not be called ".arr.txt".

Submit at this link:

https://www.captain-teach.org/brown-cs173/assignments/