Assignment 5

Trustful MinML interpreter (due 3/6)

In Assignments 2/3, the MinML interpreter had the following signature:

 interpret :: MLExp -> Env -> MLValue
 
 type Env = [(String,MLValue)]

 data MLValue = 
     MLVDivZero
   | MLVNum Int
   | MLVTrue
   | MLVFalse
   | MLVClosure MLExp Env

In the terminology of the Jbook, this interpreter is a defensive interpreter in the sense that all the runtime values it manipulates are tagged.In other words, when executing an operation like +, the interpreter can check that the two arguments are of the form MLVnum. This is unnecessary if we believe the proof of type safety.

In this assignment, we will write a trustful interpreter in which the runtime valus cannot be distinguished at all thus forcing us to completely trust the type checker. For this interpreter the type signatures above become:

 interpret :: MLExp -> Env -> Int
 
 type Env = [(String,Int)]

In other words, all the values must be just Ints which is close enough to what you would get in a low-level machine (sequences of bits).

You will clearly need to encode each value as an Int. For example, you can encode MLVNum 1 as 1 and MLVTrue as 1. When interpreting the operation +, if both arguments are 1, the operation returns 2. As far as the + is concerned, it doesn't matter whether the argument 1 is really the code for MLVNum 1 or MLVTrue but we trust the type checker never to allow a 1 which is the code for MLVTrue to ever appear as the argument to a +.

For encoding closures, here is a hint: change the signature of the interpreter by adding additional arguments.

Regarding MLVDivZero, it is more realistic not to encode it as an Int but rather to change the type of values to be:

  data MLValue = Proper Int | MLVDivZero

where the Int is used to encode all the proper values as before.