On this page:
7.1 Data Definitions
7.2 Paret Semantics
7.2.1 Types and Their Meanings
7.2.2 Type-checking Expressions and Type Errors
7.3 Syntax Gotchas
7.4 Logistics
7.5 Testing and Submission Steps
7.6 Grading
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:

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

    |  (let ((<id> <exp>) ...) <exp>)

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

    |  true

    |  false

    |  <number>

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

    |  (<unop> <exp>)

    |  (link <exp> <exp>)

 

    # now with types!

    |  (empty <type>)

    |  (lam ((<id> : <type>) ...) <exp>)

 

type := Num

     |  Bool

     |  (List <type>)

     |  (<type> ... -> <type>)

 

op   := + | - | * | / | < | > | ==

unop := first | rest | is-empty

id   := any symbol

Some examples of Typed Paret programs are:

(link 5 (link 6 (empty Num)))

 

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

  (lam ((x : Num))

    (g (f x))))

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
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:

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:

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.