This problem set will be graded out of 20.
1. [12 Points] Perhaps you have seen the wooden dolls made in Russia that nest
within each other. Create an abstract data type (ADT) using a signature and
structure in ML to model a wooden-doll factory. You will need a type
doll and a type box. There will be the following operations on
Note: A baby doll weighs 10 grams. A doll shell(baby) weighs 30 grams: 20 for the shell, 10 for the baby. The doll shell(shell(baby)) weighs 60 grams: 30 for the outer shell, 20 for the inner shell, 10 for the baby.
If I create
a = baby b = shell(a) c = baby d = shell(c) e = shell(d)Then I can create a box with the list [b,e].
bx = box([b,e])
2. [8 points] In class, we defined an extension of MinML with exceptions. Here is the syntax:
t ::= int | bool | t -> t | t cont
e ::= x | n | b | if e then e else e | fun f(x:t) : t = e | e e | try e with e | fail
v ::= n | b | fun(x:t) : t = e
evaluation contexts (for call-by-value, left-to-right evaluation)
E ::=  | if E then e else e | E e | v E | try E with e
See the class note for the operational semantics and type system.
Notice that the operational semantics is defined by two judgments: top
level evaluation (e --> e) and beta reduction/ instruction rules (e -->i e).
The only rules for top-level evaluation are these:
e -->i e'
E[e] --> E[e']
(try E' with e) not in E
E[fail] --> fail
Let's think about how to prove type safety -- the statements of the lemmas
involved will obviously change slightly from our previous proofs since the
structure of the operational semantics has changed. Let's specifically
consider proving a type preservation lemma. Our goal is to prove that the
top-level operational relation is sound:
Theorem: Preservation of Top-level Evaluation: If |-- e : t and e --> e' then |-- e' : t.
In order to do this, we will have to reason about the beta-reduction rules. The beta-reduction rules and their typing are not substantially different from any of the systems we have looked at in the past, so we can prove the following lemma in the ordinary way:
Lemma: Preservation of Instruction Rules: If |-- e : t and e -->i e' then |-- e' : t.
Proof: By induction on the operational relation e -->i e'.
[8 points] Your job: assuming you have already proven the Preservation of Instruction Rules Lemma + any Lemmas concerning Substitution, Weakening, Exchange, Inversion of Typing, Canonical Forms that you would like, prove the Preservation of Top-level Evaluation Lemma. Hint: define a typing judgement (via a collection of inference rules) for contexts E and prove a lemma about the typing relation for contexts.