Fall 99, CSE 520: Solution of Assignment 3

Exercise 1

False. If T is inhabited then there exists a term in normal form with type T, but in general it is not unique. In fact, if there exists N such that N:T, then N is typeable, hence it is (strongly) normalizing. However there can be several terms N with type T and different normal form. For instance, the Church numerals have all the same type (A -> A) -> A -> A, they are all in normal form, and they are all different.

Exercise 2

  1. Not typeable.
  2. Not typeable.
  3. (A -> B) -> A -> A -> B * B
  4. (A -> B -> C) -> A * B -> C
  5. (A + B -> C + D -> E) -> A -> D -> E
The complete solution of the exercise required the construction of the proof. See the instructor if you have questions about it.

Exercise 3

  1. \x. inl (fst x)
  2. Not inhabited. In fact, as a formula, it is not validally classically (for A = false and B = true, the result is false), hence it is not valid intuitionistically either.
  3. \f x. f (inl x)
  4. \f x. fst (f x)
  5. Not inhabited. In fact, for A = B = C = false the formula is classically false.

Exercise 4

  1. fun curry f x y = f (x,y);
  2. fun uncurry g (x,y) = g x y;
  3. fun swap f (x,y) = f (y,x);
  4. fun fst (x,y) = x;
    fun snd (x,y) = y;

Exercise 5

   type metric_weight = real;            (* Kilos *)
   type english_weight = int * int;      (* Pounds and ounces *)
   type weight = (metric_weight,english_weight) union;

   val difference : weight -> weight -> weight = fn w1 => fn w2 =>
       my_case(w1, fn x1 => inl (x1 - my_case(w2, fn x2 => x2, 
                                                  fn y2 => real (fst y2)*0.454 + real (snd y2)*0.028
                                             )
                                ), 
                   fn y1 => inl (real (fst y1)*0.454 + real (snd y1)*0.028 -
                                      my_case(w2, fn x2 => x2, 
                                                  fn y2 => real (fst y2)*0.454 + real (snd y2)*0.028
                                             )
                                )
              );
or equivalently, by using pattern-matching 
   fun difference ((inl x):weight) ((inl y):weight) = inl (x - y) : weight
     | difference (inl x) (inr (y1,y2)) = inl (x - (real y1 * 0.454 + real y2 * 0.028))
     | difference (inr (x1,x2)) (inl y) = inl ((real x1 * 0.454 + real x2 * 0.028) - y)
     | difference (inr (x1,x2)) (inr (y1,y2)) = inl ((real x1 * 0.454 + real x2 * 0.028) 
                                                    - (real y1 * 0.454 + real y2 * 0.028));
we can also define the type weight without making use of the defined type union, and use more meaningful names: 
   datatype weight = kilos of real | p_o of int * int;

   fun difference (kilos x) (kilos y) = kilos (x - y) 
     | difference (kilos x) (p_o (y1,y2)) = kilos (x - (real y1 * 0.454 + real y2 * 0.028))
     | difference (p_o (x1,x2)) (kilos y) = kilos ((real x1 * 0.454 + real x2 * 0.028) - y)
     | difference (p_o (x1,x2)) (p_o (y1,y2)) = kilos ((real x1 * 0.454 + real x2 * 0.028) 
                                                     - (real y1 * 0.454 + real y2 * 0.028));