Implementing Type-Checking, CSC430, Spring 2020
1 Goal
Extend the interpreter (no classes) to include mutation and a type system.
2 Guidelines
For this and all remaining assignments, every function you develop must come with the following things:
A commented header line that expresses the result of the function in terms of its inputs, written in English. Be as precise as you can within the space of a line or two.
A type declaration (possibly inline), specifying the input and output types.
Test cases. A function without test cases is incomplete. Write the test cases first, please.
For this assignment, you must develop your solutions using the typed/racket language. If you haven’t seen them, you might be interested in these Hints on Using Typed Racket in CPE 430.
Your test cases must use the check-equal?, check-=, or check-exn forms.
Your solution should take the form of a single file. Solve each problem separately, and make sure that each solution appears in a separate part of the file, with comments separating each problem’s solution.
Hand in your solution using the handin server. For help with the handin server, please see the course web page.
2.1 Handling Errors
All of your error messages must contain the string "AQSE". Essentially, this allows my test cases to distinguish errors correctly signaled by your implementation from errors in your implementation. To be more specific: any error message that doesn’t contain the string "AQSE" will be considered to be an error in your implementation.
2.2 Progress Toward Goal comment
Graders are happier when they know what to expect. Your final submission should start with a short one- or two-line comment indicating how far you got through the project. Ideally, this would just be: “Full project implemented.” But if you only implemented, say, squazz and blotz, and didn’t get to frob or dringo, please indicate this in the comment, so that we don’t spend all our time searching for bits that aren’t there.
3 The Assignment
This assignment will build on the previous assignment, assignment 3. In this assignment, we’ll be adding mutation (in a meta-circular way, the easiest way possible), and a simple type system.
4 Syntax of AQSE4
A AQSE4 program consists of a single expression.
The concrete syntax of the AQSE4 expressions with these additional features can be captured with the following EBNFs.
expr | = | num | ||
| | string | |||
| | id | |||
| | {if expr expr expr} | |||
| | {vars {{id : ty expr} ...} expr} | |||
| | {lam {[id : ty] ...} expr} | |||
| | {box expr} | |||
| | {unbox expr} | |||
| | {set-box! expr expr} | |||
| | {begin expr expr ...} | |||
| | {id <- expr} | |||
| | {expr expr ...} |
ty | = | num | ||
| | bool | |||
| | str | |||
| | {ty ... -> ty} | |||
| | {boxof ty} |
operator | = | + | ||
| | - | |||
| | * | |||
| | / | |||
| | num-eq? | |||
| | str-eq? | |||
| | <= | |||
| | substring |
... where an id is not vars, if, lam, :, <-, box, unbox, set-box!, or begin.
4.1 Primitives
procedure
(+ a b) → num
a : num b : num
procedure
(- a b) → num
a : num b : num
procedure
(* a b) → num
a : num b : num
procedure
(/ a b) → num
a : num b : num
procedure
(<= a b) → boolean
a : num b : num
procedure
(num-eq? a b) → boolean
a : num b : num
procedure
(str-eq? a b) → boolean
a : str b : str
procedure
(substring str begin end) → string
str : str begin : num end : num
value
true : boolean
value
false : boolean
4.2 Mutation
This assignment includes both mutation of variables and mutable boxes. We’ll be implementing it in a meta-circular way; that is, we’ll be using racket boxes to implement AQSE4 boxes, and to implement mutable variables, we’ll be adding mutation to our environments.
However, we want to be a bit careful; it turns out that it’s not a great idea to use, say, mutable hash tables; we want the cells to be mutable, but we still want the nice behavior of immutable hash tables (or, equivalently, lists of bindings). The way to have our cake and eat it too is to create an immutable mapping from names to mutable values. If, for instance, you’re using a Binding structure, you’ll probably want to update it to map a name to a boxed value, written (Boxof Value).
4.3 Type Checking
Implement a type checker for your language. Note that since functions must now come annotated with types for arguments, you will need to have a type parser that parses types. For Heaven’s sake, make a separate function for this.
Note that the types of functions are extended to handle multiple arguments. So, for instance, the type {num str -> bool} refers to a function that accepts two arguments, a number and a string, and returns a boolean.
All type rules are standard. It is illegal to mutate a variables or boxes to contain different types than they were created with.
Just as your interpreter starts with a top-env containing the values for all of the primitive functions and boolean names, your type-checker will need to start with a top-tenv that contains types for each of the primitive functions and boolean names.
4.3.1 Binops
Type-checking binops is more or less as you might expect. For instance, a + should receive two numbers, and will produce a number. The <= operator will take two numbers, and return a boolean.
The equal? operator is a bit different. Specifically, we don’t have subtyping, and we treat the equality operator as a function in the environment, so it must have a single type. In order to simplify our lives, we split it into two equality operators; one that only works for numbers, called num-eq?, with type {num num -> bool}, and one that only works for strings, called str-eq?, with type {str str -> bool}.
Also, note that begin is not a primitive in this language. Can you see why?
5 Suggested Implementation Strategy
Here are some of the steps that I followed. I wrote test cases for every step before implementing it.
5.1 Adding Type-Checking
Add a data definition for Types.
Add a parser for the language of types.
Develop a type checker that only works for constants.
Add a definition for Type Environments, mapping symbols to types.
Extend your type checker to handle variables and if expressions.
Extend your type checker to handle applications. (Since you don’t have types for LamC terms yet, your test cases should just use primitive functions.)
Extend your AST nodes for LamC nodes to include types with the parameters.
Extend your type checker to handle LamC terms.
Extend your parser and type checker to handle the modified vars term.
Add your type checker to top-interp. Type checking should happen after parsing and before interpretation.
5.2 Adding Mutation
Add a type for boxed values (this type should contain a type).
Add a value to represent boxed values (this value should contain a mutable box).
Extend serialization to handle boxed values. The serialization of a boxed value should simply be "#<box>".
Add a new ExprC for the box primitive. Oops, your code is broken.
Add a new rule to the Parser to allow you to parse the box form.
Add a new rule to the interpreter for the box form.
Add a new rule to the type-checker for the box form. Your code should work again!
Follow the same set of steps for unbox and set-box! forms.
Alter your (run-time) environment so that it maps names to boxed values. This will break your code again.
Repair your code by adding an unboxing step to your variable lookup and a boxing step to your environment extension.
Change your top-env declaration into a make-top-env function, so that mutating true to be false doesn’t affect later programs.
Finally, add a variable mutation form as a new ExprC, and add corresponding rules to the type-checker and interpreter.
Profit!
6 Interface
Make sure that you include the following functions, and that they match this interface:
procedure
(parse s) → ExprC
s : Sexp
procedure
(parse-type s) → Ty
s : Sexp
procedure
(type-check e env) → Ty
e : ExprC env : TEnv
value
base-tenv : TEnv
procedure
(interp e env) → Value
e : ExprC env : Environment
procedure
(top-interp s) → string
s : s-expression