Implementing Type-Checking, CSC430, Fall 2024🔗

1 Goal🔗

Extend the interpreter to include 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.

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 "AAQZ". 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 "AAQZ" will be considered to be an error in your implementation.

Additionally, your error messages should be actually helpful. Since you are the primary consumer of your own error messages, making these error messages good in the first place should reduce your overall development time. There are two parts to this: first, the error message should include text that actually indicates what the programmer did wrong. Second, include the text of the user’s program, so they (actually you) can figure out how to fix it. See lab 3 for an example of how to do this. (Apologies in advance if I renumber the labs and fail to update this paragraph....)

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 Assignment 4 interpeter, or on the Assignment 6 interpreter. As you’ll see below, starting with the 4 interpreter will require you to make a small additional modification, so if your Assignment 6 is in perfect working order, using it will save you a few minutes. Either should be fine.

4 Syntax of AAQZ7🔗

A AAQZ7 program consists of a single expression.

The concrete syntax of the AAQZ7 expressions with these additional features can be captured with the following EBNFs.

... where an id is not one of the keywords: if, bind, recbind, =>, =, or :

4.1 Primitives🔗

Note that there is no error primitive in this assignment. What would its type be?

4.2 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. You should definitely 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.

4.2.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}.

5 Recursion🔗

This assignment will add recursion, using a rec form. Implement the rec form as described in the book. Note that you will need some kind of mutation in order to create the closure as a cyclic data structure.

If you are starting with assignment 4, this means you will want to update your environment type to map names to boxed values (that is, (Boxof Value) ), adding the accompanying use of box when storing things in the environment and unbox when looking them up.

If you are starting with assignment 6, you’ve already made a related accommodation to support mutation, so this is not necessary.

Here’s an example of a simple program that defines a recursive function to compute perfect squares in a kind of silly way:

{recbind [square-helper

: {num -> num}

= {([n : num]) => {if {<= n 0} 0 {+ n {square-helper {- n 2}}}}}]

{bind [square

: {num -> num}

= {([n : num]) => {square-helper {- {* 2 n} 1}}}]

{square 13}}}

6 Suggested Implementation Strategy🔗

6.1 If Starting With Assignment 4🔗

• Change the type of environments to map names to (Boxof Value)

• Update the elements of the top-level environment, so e.g. (BoolV false) becomes (vbox (BoolV false)), if vbox is defined as a call to box that is specialized as described in the hints on using TR in CSC430.

• Update the interpreter’s IdC and AppC rules to do an additional unbox or vbox, respectively, when elements are looked up or added to the environment.

• Food for thought: in the previous assignment, we were careful to ensure that the mutable data structure was freshly created each time top-interp was called. Why don’t we need to do the same thing for the boxes in the environment in this assignment?

At this point, the existing interpreter should work exactly as before.

Finally, remove the error primitive, along with its tests.

6.2 If starting with Assignment 6🔗

Remove the array primitives completely, and also the variable mutation form. Also delete any tests that use these forms. Also the null value. Also the error primitive. Also the substring primitive. Hard-code a memory size of 2000 into your top-interp function, so that you can call it without specifying a memory size.

(EDIT:) Also remove the seq primitive!

6.3 Moving on🔗

Here are some of the steps that I followed. I wrote test cases for every step before implementing it. In order to facilitate testing of your type checker, you’ll probably want a function that calls the parser and then the type checker. If you

• Add a data definition for Types.

• Add a parser for the language of types.

• Add : to the set of keywords.

• 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 locals expression.

• Add your type checker to top-interp. Type checking should happen after parsing and before interpretation.

• Add the recbind form to the set of ExprCs.

• Fix breakage temporarily by signaling an error in interp on instances of RecC.

• Develop the parser clause for RecC. Test cases first!

• Develop the type-checking clause for RecC. Test cases first!

• Develop the interpreter clause for RecC. Test cases first!

7 Interface🔗

Make sure that you include the following functions, and that they match this interface:

note: The type of interp is not specified; it could include a store, if you are building on assignment 6, but if you are building on Assignment 4, it will not. Either one is fine.

8 Hint🔗

As on other assignments, uses of "cast" other than in the parser, when using a question-mark-pattern with ellipses, are likely to be bugs. The autograding framework highlights these as likely bug locations. It’s almost certainly not a good idea to use casting in your code.

9 Minimum Viable Product🔗

Some of you may be thinking about submitting your solution to assignment 4 for this assignment. Good idea! It won’t actually do any type checking, but it will certainly still pass some of the tests.

If you’re thinking of doing this, the most important change you’ll have to make to your code is to handle the presence of types in lamb and locals terms; update your parser to just ignore these extra pieces.