Computer Science 510
Programming Languages
Problem Set 6

Fall 2003
Due Wednesday November 26

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:

The client of a factory can ask for the creation of a "baby" doll, one that is solid wood and contains no other doll.
The client can return any doll d to the factory and ask for a "shell" doll, a new, hollow doll d' that contains d.
The client can pass a list of dolls back to the factory and ask for a shipping carton (box) containing them all.
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.

  1. Write the ML signature that models a doll factory.

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

  3. Write a structure 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.

  4. Prove the equivalence of your two implementations. Please show the simulation relation ~ as precisely as you can.

    Hint: Instead of defining ~ in closed form the way the Queue relation R in lecture was defined, you may give an inductive definition.

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