Elements of Programming Languages Assignment 3: Type Inference Version 1.2 (October 31)
Due: November 22, 12pm
November 1, 2023
1 Introduction
This assignment is due November 22, at 12pm.
Please read over this handout carefully and look over the code before beginning work, as some of your ques- tions may be answered later. Please let us know if there are any apparent errors or bugs. We will try to update this handout to fix any major problems and such updates will be announced to the course mailing list. The handout is versioned and the most recent version should always be available from the course web page.
2 Background
In this assignment you will implement the main components for a small, but realistic, language with parametric polymorphism, and type inference, called Fish. The syntax of Fish is similar to that of Giraffe from Assignment 2, but type annotations are not required on function arguments and recursive function results. Instead, we will implement a form of Hindley-Milner type inference for Fish. In addition, Fish supports records and references. These features complicate type inference slightly, as discussed below.
Any valid Giraffe program from assignment 2 is a valid Fish program if we simply drop type annotations. In fact, type annotations are not allowed in Fish. As a simple example,
let fun id(x) = x in (id(true),id(42))
typechecks and infers a polymorphic type ∀A.A → A for id. Recursive functions are also allowed and do not need either argument type annotations or result type annotations:
let rec fact(n) = if (n == 0) then 1 else n*fact(n-1) in fact(4)
Fish includes records and record field access constructs along the lines discussed in class, and also allows a form of let-binding that pattern-matches a record against a record pattern. For example,
let <a=x,b=y> = <a=1,b=2> in x+y
typechecks and evaluates to 1 + 2 = 3.
Finally, since Fish supports references we need to be careful to avoid a well-known problem when polymor- phism and references are mixed. In brief, if we are not careful it is possible to infer types that are too general in the presence of references. A simple example is as follows:
let f = ref(\ x . x) in
(f := \ x . x + 1);
!f(true)
What is going on here is that we create a reference to the identity function, bound to variable f , and its type is generalized to be ∀A.re f (A → A)). Then we assign f to be another function λx.x + 1 which has a type int → int which is an instance of f’s type. Finally we dereference f and apply it to true. If this program is
allowed then it results in a run-time type error because when ! f is called on true, it has been updated to be a function on integers.
This problem has been studied in many ways, and among the most popular solutions is to restrict well-formed programs further so that generalization of polymorphic types during let-binding only takes place when the let- bound expression is a value (typically this includes the usual value forms as well as variables). This is called the value restriction. We will implement a simple form of the value restriction that rules out problematic programs like the above.
Implementing type inference both efficiently and correctly is challenging. In this assignment we focus on correctness and provide an implementation of many of the ingredients of type inference, in particular util- ity functions involving type substitutions, which you will need to use to implement the full type inference algorithm.
You will also implement substitution, some desugaring rules, and an evaluator for Fish. Because types are inferred and not even present in the syntax of expressions, evaluation is largely similar to evaluation for Giraffe. The main new features are to deal with records and references. For references we will adopt a slightly different approach than that taken in lectures, specifically we will use mutable references in Scala to implement mutable references in Fish.
3 Getting started
Assn3.zip contains a number of starting files; use the unzip command to extract them. We provide the following Scala files.
• Syntax.scala containing the abstract syntax of Fish and some additional useful code for reference cells, substitution.
• Parser.scala containing a parser using the Scala parser combinators library for parsing Fish code.
• Typer.scala containing supporting code for exercises 1–3 where you will need to implement type
substitution, unification of type expressions, and type inference.
• Fish.scala containing supporting code for exercises 4–6 where you will need to implement substitu- tion, desugaring and evaluation, along with a main class/function for executing a read-eval-print loop or running Fish programs.
Although you only need to make changes to the Typer.scala and Fish.scala files, it is recommended to read through the other files (especially Syntax.scala).
We include several example programs in a directory examples.
We also provide several scripts (which should work on a DICE, Linux or MacOS system):
• compile.sh compiles the code and pakcages it as a jar file (in a place where the remaining scripts will assume they can find it).
• run.sh <file> runs your standalone interpreter on a Fish file. If the filename is omitted then the read-eval-print interactive loop is started.
• run_sample.sh <file> works like run.sh but runs using a sample solution.
In addition a JAR file Assn3Solution.jar containing a working implementation is provided. The script
sample.sh uses this.
If you are using a non-DICE system, such as Windows, these scripts may not work, but you can look at the
contents to work out what you need to do instead.
3.1 Objectives
The rest of this handout defines exercises for you to complete, building on the partial implementation in the provided files. You may add your own function definitions or other code if necessary, but please use the existing definitions/types for the functions we ask you to write in the exercises, to simplify automated testing we may do. You should not need to change any existing code other than filling in definitions of functions as stated in the exercises below.
Values
