Assignment #6: References

This assignment has 15 points. 

1.  [2 points]  Write a well-typed, non-terminating program in a typed lambda calculus that only has unit, non-recursive functions (ie:  \x:t.e) and references (ie: operations ref e, e1 := e2 and !e). 

2.  [6 points]  Prove the type preservation lemma for a language with unit, non-recursive functions and references.  In other words, prove that:

If |- (M,e) : t and (M,e) --> (M', e') then (M', e') : t

The syntax of types and expressions are:

t ::= unit | t1 -> t2 | t ref

e ::= x | () | e1; e2 | \x:t.e | e1 e2 | ref e | e1 := e2 | !e | l

v ::= () | \x:t.e | l

M ::= . | M,l -> v          (treat as a function from locations l to values v)

Psi ::= . | Psi, l:t            (treat as a function from locations l to types t)

You may assume the following lemmas have already been proven:

Lemma 1:  If |- M : Psi and l not in Dom(M) and Psi; . |- v : t then |- (M,l->v) : (Psi,l:t)

Lemma 2:  If |- M : Psi and Psi(l) = t and Psi; . |- v : t then |- M[l->v] : Psi

Lemma 3:  If |- M : Psi and l in Dom(M) then Psi; . |- M(l) : Psi(l)

Lemma 4:  If Psi;G |- e : t and l not in Dom(Psi) then Psi,l:t';G |- e : t

Only do the proof for the three cases involving these operational rules:

 

(l not in Dom(M))

--------------------------- (E-ref)

(M;ref v)  --> (M,l-> v; l)

 

(l in Dom(M))

------------------------------- (E-assign)

(M; l := v) --> (M[l -> v]; ())

 

(l in Dom(M))

------------------------------- (E-deref)

(M; !l ) --> (M; M(l))

 

3.  [7 points]  Implement the operational semantics of (ie: an interpreter for) a language that only has references and unit in SML.  The expressions of your language should be:

e ::= v | e1; e2 | ref e | e1 := e2 | !e

v ::= () | l

M ::= . | M,l -> v  

You should define the syntax of expressions using a datatype. You may implement locations using integers. eg:

 

datatype val =

  Unit

| Loc of int

 

datatype exp =

  Val of val

| Seq of exp * exp           (* this is semicolon *)

| ...

 

You should also define a type for memories:

 

type memory = ...

 

Your main job will be to define:

The evaluation functions may assume that all expressions and memories are well-typed.  You may raise the exception Bad if you run in to a situation you

cannot implement (because, for instance, a memory reference is out of bounds):

 

exception Bad

fun eval : (memory * exp) -> (memory * exp)         (* may raise exception Bad *)

fun printval : val -> unit                                         

fun printmemory : memory -> unit                                         

fun evalstar : (memory * exp) -> unit                       (* may raise exception Bad *)