On this page:
5.1 Introduction
5.2 Reading
5.3 Assignment
5.4 Features to Implement
5.4.1 Type Environment
5.4.2 Lists
5.4.3 Exceptions
5.5 Grammar
5.5.1 Abstract Syntax
5.6 Testing Guidelines
5.7 Starter Code
5.8 What To Hand In
5 Type Checker

    5.1 Introduction

    5.2 Reading

    5.3 Assignment

    5.4 Features to Implement

      5.4.1 Type Environment

      5.4.2 Lists

      5.4.3 Exceptions

    5.5 Grammar

      5.5.1 Abstract Syntax

    5.6 Testing Guidelines

    5.7 Starter Code

    5.8 What To Hand In

5.1 Introduction

In this assignment, you will implement a static type checker for an extension of the Paret language, Typed Paret.

5.2 Reading

Chapter 15.1—15.2 of PLAI 2/e.

5.3 Assignment

As in Interpreter, we have provided a function parse, which consumes an expression in Typed Paret’s concrete syntax and returns the abstract syntax representation (Expr) of that expression.
You will implement one function called type-of:

type-of :: Expr -> Type

that consumes a Paret program in abstract syntax form. If the program is well-typed, type-of returns the Type of that program; otherwise, it raises an exception.
Once you have implemented type-of, you should use the provided type-check function (analogous to eval from Interpreter) to write test cases for your type checker in your testing file.
For simplicity, Typed Paret does not have syntactic sugar. let has been converted into a non-sugar expression (so type-of will handle let expressions directly), and and and or have been removed from the language.

5.4 Features to Implement
5.4.1 Type Environment

The type language you will work with is

(define-type Type

  (t-num)

  (t-bool)

  (t-str)

  (t-fun [arg-type : Type]

         [return-type : Type])

  (t-list [elem-type : Type]))

which, respectively, represent the types of numbers, Booleans, strings, (one-argument) functions, and (homogenous) lists.
Just as how Interpreter had an Env for mapping identifiers to values, your interpreter should use a type environment (TEnv) to keep track of the types of identifiers in scope.

(define-type-alias TEnv (Hashof Symbol Type))

In type-of, if the program binds an identifier that is already bound, the new binding should take precedence. This is known as identifier shadowing. The new binding shadows the existing binding.

5.4.2 Lists

Paret now contains support for lists via the constant empty and the operations link, is-empty, first, and rest. Lists in Paret are homogeneous: all elements in the list must have the same type.
A question to briefly consider: What is the Type of the empty list? It’s polymorphic: it can be a list of any type at all! Because it has no elements, there’s nothing to constrain its type. However, because our type checker is not polymorphic, we handle this with a simple expedient: we require that every empty list be annotated with a type for the elements (that will eventually be linked to it). Naturally, the elements that eventually are linked to it must be consistent with that annotated type.
Thus, our typed list semantics are as follows:
  • empty
    (empty : t) makes an empty list whose elements have type t.

  • link :: t, (List t) -> (List t)
    (link x y) prepends the element x to the list y.

  • first :: (List t) -> t
    (first x) returns the first element of x.

  • rest :: (List t) -> (List t)
    (rest x) returns the list x except for the first element of x.

  • is-empty :: (List t) -> Bool
    (is-empty x) returns true if x is empty; otherwise, it returns false.

Whenever these type signatures are violated, the type checker should raise a tc-err-bad-arg-to-op exception.
Error-checking link should occur in the following manner: If the type of the second argument to link isn’t a (List t), the arg-type of tc-err-bad-arg-to-op should be the type of the second argument. If the second argument to link is a (List t) but the type of the first argument is not t, then the arg-type of tc-err-bad-arg-to-op should be the type of the first argument. For example,

(link "hello" 3)

(link 2 (empty : Bool))

should all raise (tc-err-bad-arg-to-op (op-link) (t-num)).

5.4.3 Exceptions

Most of the exceptions your type-checker can raise are just like the errors from Interpreter, but with a type instead of a value.
There are two new kinds of exceptions, though:
  • tc-err-bad-arg-to-fun should be raised 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 should be raised 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. For instance,

    (if true 3 "three")

    should raise (tc-err-if-branches (t-num) (t-str)).
    However, tc-err-if-got-non-boolean takes precedence over tc-err-if-branches. For example,

    (if "non-bool" 5 "five")

    should raise (tc-err-if-got-non-boolean (t-str)) rather than (tc-err-if-branches (t-num) (t-str)).

Thus, the full set of exceptions is as follows:

(define-type TypeCheckingError

  (tc-err-if-got-non-boolean [cond-type : Type])

  (tc-err-bad-arg-to-op [op : Operator]

                        [arg-type : Type])

  (tc-err-bad-arg-to-un-op [op : UnaryOperator]

                           [arg-type : Type])

  (tc-err-unbound-id [name : Symbol])

  (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]))

For tc-err-bad-arg-to-op, argument types to Operators should be checked from left to right. For example,

(+ true "string")

should raise (tc-err-bad-arg-to-op (op-plus) (t-bool)).
Finally, your type-checker should type-check by performing a post-order traversal of the AST: first, traverse all of the children of an expression from left to right, then check the expression itself. This makes it unambiguous which error to raise if there are multiple errors in the AST. For example,

(str= (+ 1 "bad") (++ 1 "bad"))

(++ false (+ "bad" 2))

("not function" (+ 3 "bad"))

(if true (+ 4 "bad") (++ 4 "bad"))

should all raise (tc-err-bad-arg-to-op (op-plus) (t-str)).

5.5 Grammar

The grammar of Typed Paret is as follows:

<expr> ::= <num>

         | <string>

         | true

         | false

         | (+ <expr> <expr>)

         | (++ <expr> <expr>)

         | (num= <expr> <expr>)

         | (str= <expr> <expr>)

         | (if <expr> <expr> <expr>)

         | <id>

         | (<expr> <expr>)

 

         | (lam (<id> : <type>) <expr>)

         | (let (<id> <expr>) <expr>)

         | (link <expr> <expr>)

         | (first <expr>)

         | (rest <expr>)

         | (is-empty <expr>)

         | (empty : <type>)

 

<type> ::= Num

         | Str

         | Bool

         | (List <type>)

         | (<type> -> <type>)

Our parse function expects and enforces spaces around : and ->, so keep that in mind when you’re writing test cases.

5.5.1 Abstract Syntax

Refer to Type Environment for the definitions of TEnv and Type.

(define-type Expr

  (e-num [x : Number])

  (e-bool [x : Boolean])

  (e-str [x : String])

  (e-op [op : Operator]

        [left : Expr]

        [right : Expr])

  (e-un-op [op : UnaryOperator]

           [expr : Expr])

  (e-if [cond : Expr]

        [consq : Expr]

        [altern : Expr])

  (e-lam [param : Symbol]

         [arg-type : Type]

         [body : Expr])

  (e-app [func : Expr]

         [arg : Expr])

  (e-id [name : Symbol])

  (e-let [id : Symbol]

         [value : Expr]

         [body : Expr])

  (e-empty [elem-type : Type]))

 

(define-type Operator

  (op-plus)

  (op-append)

  (op-num-eq)

  (op-str-eq)

  (op-link))

 

(define-type UnaryOperator

  (op-first)

  (op-rest)

  (op-is-empty))

5.6 Testing Guidelines

For the purposes of testing, we have defined a type-check function that calls parse and type-of for you. type-check consumes an expression in Paret’s concrete syntax (S-Exp) and returns a Paret Type:

type-check :: S-Exp -> Type

You should use type-check in your testing file when writing test cases. You should not directly test type-of in your testing file.
In addition to the testing forms documented in the Testing Guidelines, we provide the following testing form:
  • (test-raises-type-checker-error? name expr type-checker-error)
    Tests that the given expr raises the given type-checker-error. (Example usage can be found in the testing stencil.)

5.7 Starter Code

We’ve provided starter code for your implementation at type-checker.rkt and support code at support.rkt. You are not allowed to change the signature of type-check and type-of, but you are welcome to add any helper functions that you need for your implementation.
We’ve also provided a stencil for your type-check test cases at type-checker-tests.rkt and testing support code at test-support.rkt. You should check that you can run your type-checker-tests.rkt file successfully in DrRacket before submitting—if you can’t, it means that a definition is missing or you’re trying to test a function that you shouldn’t be testing.

5.8 What To Hand In

You will submit two files for this assignment:
  • type-checker.rkt, which should be uploaded to the “Code” drop on Gradescope.

  • type-checker-tests.rkt, which should be uploaded to the “Tests” drop on Gradescope.

You can update your submissions as many times as you want before the deadline.