EECS 321:   Programming Languages — Homework 9
1 True, False, equals, and if
2 Typed Lists
3 Typing Rules
4 Datatypes
5 Errors
6 Handin Instructions
7.0.0.11

EECS 321: Programming Languages — Homework 9

Install the plai-typed language via DrRacket’s File | Install Package ... menu item. Type plai-typed into the "Package Source" box and click "OK".

You can find documentation for PLAI Typed by going to the main documentation page for your installation (type F1 in DrRacket and then click the "Up" links until there aren’t any more) and following the "PLAI Typed Language" link you find there.

Start your program with: #lang plai-typed

1 True, False, equals, and if

Add support for true, false, {= ... ...}, and {if ... ... ...} expressions to the TFAE language we saw in lecture.

You don’t need to write a parser; testing directly on abstract syntax is fine.

2 Typed Lists

Add support for lists to the language by extending it with the following expressions:

<TFAE> = ...

       | {cons <TFAE> <TFAE>}

       | {first <TFAE>}

       | {rest <TFAE>}

       | {nil <type>}

       | {empty? <TFAE>}

 

<type> = number

       | boolean

       | {<type> -> <type>}

       | {listof <type>}

All of which work as they do in Racket, with the exception of nil, which is just the empty list, but must be annotated with a type. For example, the type of {nil number} is {listof number}.

Require that all elements of a list have the same type, which you can ensure when type-checking cons.

It might seem unusual that nil must come with a type. Since the empty list can have many types, the programmer has to explicitly pick the one that agrees with the rest of the list.

Again, you don’t need to bother with a parser and may just use the abstract syntax directly.

3 Typing Rules

Here are the precise typing rules for the new constructs. The part in square brackets on the right of the rule is the name of the rule, for your convenience. It does not carry any semantic meaning.

image

4 Datatypes

You must use the following definitions of types and expressions (you are free to make other types that you use internally).

(define-type TFAE
  [num (n : number)]
  [bool (b : boolean)]
  [add (l : TFAE) (r : TFAE)]
  [sub (l : TFAE) (r : TFAE)]
  [eql (l : TFAE) (r : TFAE)]
  [id (name : symbol)]
  [ifthenelse (tst : TFAE) (thn : TFAE) (els : TFAE)]
  [fun (arg : symbol) (typ : Type) (body : TFAE)]
  [app (rator : TFAE) (rand : TFAE)]
  [consl (fst : TFAE) (rst : TFAE)]
  [firstl (lst : TFAE)]
  [restl (lst : TFAE)]
  [nil (typ : Type)]
  [mtl? (lst : TFAE)])
 
(define-type Type
  [numberT]
  [booleanT]
  [arrowT (dom : Type) (codom : Type)]
  [listT (typ : Type)])

5 Errors

If type-check-expr is passed an expression that isn’t well-typed, then it should fail with an exception containing the string: "type error". Note that free identifiers count as type errors, and so must also raise errors with the string "type error".

6 Handin Instructions

Provide a definition of type-check-expr : TFAE -> Type, as above.

You must use the datatype definitions for TFAE and Type provided above.

Have the 8 rules from the Provost’s website (see the homework 1 for more details).

Submit your code using the Handin button in DrRacket.