Computer Science 441
Programming Languages
Problem Set 6

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 the ADT:

baby
The client of a factory can ask for the creation of a "baby" doll, one that is solid wood and contains no other doll.
shell
The client can return any doll d to the factory and ask for a "shell" doll, a new, hollow doll d' that contains d.
box
The client can pass a list of dolls back to the factory and ask for a shipping carton (box) containing them all.
weight
The weight of a baby doll is 10 grams. The weight of a shell doll containing n dolls 10(n+1) plus the weight of all the dolls contained. The weight of a box is 1000 grams plus the weight of the dolls contained. The client can ask for the weight of any box.
There are no other operations on dolls and boxes.

  • [2 Points] Write the ML signature that models a doll factory.

  • [2 Points] Write a reference implementation: that is, an ML structure that implements this signature as straightforwardly as possible. In your reference implementation, creation of a doll or construction of a box should just be the application of a data constructor.

  • [2 Points] Write a candidate implementation that implements this signature more efficiently. For each type in the signature, use as efficient a representation as possible, given the set of operations required.  If you can't think of a particularly efficient representation than at least come up with one that is significantly structurally different from your reference implementation.

  • [4 Points] Define two simulation relations Rdoll and Rbox, one for each abstract type (doll and box) as precisely as you can.  Instead of defining Rbox and Rdoll in closed form the way the Queue relation R in lecture was defined, you may give an inductive definition via a collection of inference rules if you want.
    •
  • [2 Points] Explain exactly what you must prove in order to show the candidate implementation as a whole is indistinguishable from the reference implementation.  You don't have to do the proof, just clearly write down the complete formal statement of what must be proven.
    •

    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:

    types
    t ::= int | bool | t -> t | t cont

    expressions
    e ::= x | n | b | if e then e else e | fun f(x:t) : t = e | e e | try e with e | fail

    values
    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.

    Proof:  ??

    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.