In this assignment, you will implement a type checker for Paret, which has been augmented with type annotations on function parameters.
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.
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.
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))
.
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.
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:
(empty : t)
makes an empty list whose elements have type t
. For
instance, (empty : Num)
is an empty list of numbers. The type
declaration is important to be able to tell what the type of the list
is (otherwise this assignment would be much harder).(link x y)
appends the element x
to the front of the list y
; it
acts just like Pyret's link
. If x
has type t
and y
has type
(List t)
, then (link x y)
should have type (List t)
.(is-empty x)
checks to see whether x
is an empty list. If x
has
type (List t)
, then (is-empty x)
has type Bool
. (is-empty
should
produce a type error if its argument is not a list.)(rest x)
returns all of a list except for the first element. If x
has type (List t)
, then (rest x)
has type (List t)
. (rest
should
produce a type error if its argument is not a list.)(first x)
returns the first element of the list. If x
has type (List t)
, then (first x)
has type t
. (first
should
produce a type error if its argument is not a list.)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.
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.
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.
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:
tc-err-bad-arg-to-fun
when a function is applied to an argument
of the wrong type. func-type
is the type of the function being
applied, and arg-type
is the type of the argument it was applied to.tc-err-if-branches
when an if statement has branches that have
different types. then-type
is the type of the "then" branch, and
else-type
is the type of the "else" branch.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
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>)
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.)
To get started, open the
and the
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: