5 A5: Type System
Due: May 7, 2025
You are given a file on Canvas types.rkt with a starter code for the assignment.
The goal of this assignment is to extend the type system we discussed in class to the language with state. With this change, you will extend your type system to go from a functional language to an imperative one.
More concretely, the type checker implemented in the starter code is for the language from Lambda: First-class Functions. Extend this type checker to support the language from Program State. Specifically, you have to extend the type checker to support the seq, ways to allocate, access, deallocate, and update state via new, free, deref, and set! respectively by adding references to the type system. Your goal in this assignment is add support for references in the type system.
References in this type system is denoted by the Ref type. However, just denoting references with a base type Ref does not tell was anything about the underlying data type that the reference points to. For example, if x is a reference we have no idea what kind of value (deref x) will return. This can cause unsoundness in the type system! To mitigate this we have to track what type of values references point to. To use this we will use parametric polymorphism where the base type will be Ref, parametrized by the type of value it is referencing. For example, (new 5) will have a type (Ref Int), (new #t) will have a type (Ref Bool). Dereferencing will then give us back the expected type: (deref (new 5)) will be of type Int.
These parameterized Ref types are represented using our familiar list notation:
'(Ref Int)
5.1 Type seq
seq is used to define a sequence of expressions in the program. When a sequence of expressions are type checked, all expressions are individually type checked, but the entire sequence has the type of the last expression. For example, the following expression has the type 'Bool.
(seq (let ((x : Int (+ 5 4))) (+ x 2)) #t)
5.2 Type new
new is used to allocate a value on to the program state. The type of a (new e) is the reference to the type of e. For example, the following expression has the type '(Ref (-> Int Int)).
5.3 Type deref
deref is used to dereference a reference to the program state. The type of a (deref e) is the dereferenced type of e. It is a type error is ‘e‘ is not a reference. The following expression has the type '(-> Int Int).
5.4 Type set
set is used to mutate value in the program state and returns the updated value. The type of a (set e1 e2) is the type e2 if e1 has a refers to the same type as e2. This means once a location has been created in the state with a particular type of value, it can only store values of the same type in future.
For example, the following has the type 'Int. The (new 4) expression has type '(Ref Int), so set will allow update of '(Ref Int) with an 'Int.
However, the following results in a type error. set should now allow update of location of type '(Ref Int) with a 'Bool value.
set is also type error if e1 does not have a reference type.
5.5 Type free
free is used to free a value stored in a location and returns the location. The type of a (free e) is the type e. It is a type error if e does not have a reference type. The following expression has the type '(Ref Int).
(free (new 4))
5.6 Testing
You should test your code by writing test cases and adding them to relevant files. The starter code is available in types.rkt on Canvas. Use the command raco test [filename] to test your code. Alternatively, pressing “Run” in Dr. Racket will also run your test cases.
For grading, your submitted type checker will be tested on multiple programs drawn from this language. Writing your own test cases will give you confidence that your type checker can handle previously unseen programs.
5.7 Submitting
You should submit on Gradescope. You should submit the file types.rkt for grading, so make sure all your work is contained there! You may add any function you need to these files, but do not rename the file or the tc function.