Machine Problem 8: Inferring Types

Out: Friday, 28 March 2008

Due: 5 PM Friday, 4 April 2008

Submission: Partners

This assignment is to be done in pairs. If you cannot find a partner, please contact your instructor.

Purpose

The main goal of this assignment is to give you some experience generating type constraints and inferring types for the SIMPLE programming language.

Tasks

All three tasks involve adding code to the infer.scm file provided by the instructors. Although you are given a complete interpreter for the SIMPLE language and a top.scm file that can be used to test that interpreter, you will use the top-infer.scm file instead for this assignment (because you are working with the static semantics of SIMPLE, not the dynamic semantics). The tests-infer.scm file includes a few tests, but you will probably want to write more.

1. [5pts] Define a procedure named bound-variables that takes the abstract syntax tree of a SIMPLE program and returns a list of the program's bound variables, including the three variables (true, false, and x) that are bound in the standard initial environment.
2. [10pts] Write a procedure named well-typed-expression? that takes the abstract syntax tree of a SIMPLE expression exp, always returns a boolean, and returns true if and only if (a-program '() exp) is well-typed.
   (Hint: Task 2 is trivial to implement by calling the well-typed? procedure that the instructors have provided for your use in task 3, and that is the best way to do task 2, but you will not receive credit for that implementation unless you are able to complete task 3. You can and should implement task 2 even if you are unable to complete task 3.)
3. [15pts] Using the abstract data types of types, type variables, and type constraints that have been provided by the instructors in types.scm, write a procedure named collect-constraints that takes the abstract syntax tree of a SIMPLE program and returns a list of type constraints that are satisfiable if and only if the program is well-typed. If you do this correctly, the well-typed? procedure provided by the instructors will become a decision procedure for well-typedness of SIMPLE programs.
4. [5pts] Consider the PROC program from EoPL exercise 3.23 (the one whose let expressions bind makemult and times4). Use the definitions Will gave in lecture 10 to answer both of the following questions:
   • Is this program type-safe? Use the definition of type safety to justify your answer.
   • Is this program well-typed? Use the definition of well-typedness to justify your answer.

Infrastructure

You are given an interpreter for the SIMPLE language together with:

• an incomplete implementation of a decision procedure for well-typedness of SIMPLE programs, missing only the part you will supply in task 3.
• implementations of types, type variables, and type constraints, including a unification-based solver for lists of type constraints.
• tests that can be run by requiring "top-infer.scm".

The easiest way to copy this code into one of your own directories is to use the cp command on a CCIS Solaris machine:

        cp -r /course/csg111/.www/interps/simple-lang .

Deliverables

1. A completed version of infer.scm with all of the code you wrote for tasks 1 through 3, not including tests.
2. A modified version of tests-infer.scm that contains the tests you added for testing tasks 1 through 3.
3. You should also submit top-infer.scm and all files needed to require that file, even though most of these files should be exactly the same as the files provided by the instructors.
4. A text file mp8.txt that contains your answers for task 4.
5. A Development Diary

Back to Machine Problems

Last modified: 31 March 2008