CS 336 Homework

Homework 1

Due 1/18/05.

1. Exercises 4.2.2, 5.3.7, 6.2.3, 6.3.1.
2. Solutions

Homework 2

Due 1/27/05.

1. Write a detailed proof of Theorem 9.3.9.
2. Modify the simplebool program to add arithmetic terms and a second primitive type Nat.
   • Add Nat, 0, succ, pred iszero tokens to the lexer and parser (modifying the .lex and .grm files).
   • Extend the definition of terms in the parser (simplebool.grm) with arithemetic term forms (see tyarith/tyarith.grm).
   • Add type and term constructors to the abstract syntax (syntax.sml), and modify print functions accordingly (see tyarith/syntax.sml).
   • Modify the eval and typeof functions in core.sml to handle arithmetic terms.
3. Exercise 11.8.2.

Homework 3

Due 2/10/05.

1. Modify the treatment of lists in Section 11.12 (Figure 11-13) to use a case expression in place of primitive functions head, tail, and isnil, and show that the Progress theorem holds for the result (in contrast to the original treatment, for which Progress does not hold (see the solution for Exercise 11.12.1)).
2. Give a term whose evaluation does not terminate in the CBV lambda calculus with Nat, Bool, and Ref, but no fix operator.
3. Do the inductive case for t = ref t1 in the proof of 13.5.3.
4. Do the inductive case for \empty | \Sigma |- t : Ref T in the proof of 13.5.7.
5. Do Exercise 15.5.2 (page 198).
6. Solutions

Homework 4

Due 2/24/05.

1. Do Exercise 18.6.2.
2. Redo the examples of Section 20.1 using the isorecursive types of Figure 20.1.
3. Redo the examples of the previous exercise in Standard ML.
4. Prove Theorem 23.5.1 (Preservation for the polymorphic lambda calculus, Figure 23.1). Give only the new cases involving the polymorphic constructs of the language.
5. Prove the Progress theorem for Existential types (Figure 24.1). Give only the new cases involving the existential type constructs.
6. Solutions

Homework 5

Due 3/10/05.

1. (a) Exercise 8.5.1. (Modules Chapter)
   (b) Exercise 8.5.2.
   
   
2. The description of signature ascription in Section 8.5 only treats a form of opaque ascription, also known as sealing and expressed using the notation M :> I. Standard ML also supports this opaque ascription (with the same notation), but it also has transparent ascription with the notation M : I. The difference is illustrated by the following example.

   I = sig type t
           val x : t
       end
   
   M = struct
           type t = int
           val x : t = 0
       end
   
   M1 = M : I
   M2 = M :> I
   
   M1.t == int
   M1.x : int
   
   M2.t is abstract
   M2.x : M2.t
   

   Describe a procedure for type checking an ascription of the form M : I, and discuss how the procedure differs from that for checking M :> I.
   
   
3. In Section 8.8 a functor dictFun is described but not defined.
   (a) Write out a complete definition of dictFun (e.g. representing dictionaries as association lists -- lists of key-value pairs).
   (b) Do Exercise 8.8.3.