CS223 Spring 2012
Midterm Exam
4/30/2012, 11:30am-12:20pm, Ryerson 276

[NOTE: This file contains UTF-8 Unicode characters. Use editor that
displays such characters, or set browser encoding accordingly.]

1. [20] Consider the following let expression (using ML surface
syntax, but this translates easily to the toy language of
typecheck2/syntax.sml):

  let val r = ref(fn x => x)
   in r := (fn y => y + 1);
      (!r) true
  end;

We assume ref, :=, and ! have the usual polymorphic types in
the base context:

  ref : 'a -> 'a ref
  :=  : 'a ref * 'a -> unit
  !   : 'a ref -> 'a

(a) Using the typechecking algorithm from typecheck2, does this
expression type check? If so, what is it's type (you do not need
to do a detailed derivation of the type).

ANS: the let expr has type Bool (r gets the polymorphic type
∀α.(α → α) ref, then the occurrence r in (!r)true gets instantiated
to (Bool → Bool) ref). This is wrong, because the dynamic contents
of r when that expression is evaluated will be of type Int → Int.

(b) Does it type check in SML? Explain why or why not.

ANS: No, it does not type check because the value restriction
prevents the type of r at the let binding from being generalized
to a polymorphic type, leaving r : (R → R) ref, which cannot unify
with the contexts of both occurrences of r in the body of the let.


2. [15] Define a function

  interleave : 'a list -> 'a list -> 'a list

that interleaves two lists. I.e.

  interleave [1,2,3] [4,5,6,7,8] ==> [1,4,2,5,3,6,7,8]

ANS: 
  fun interleave nil x = x
    | interleave x nil = x
    | interleave (x::xs) (y::ys) = x::y::(interleave xs ys)


3. [15] Explain in detail how to type check the following
variable declaration:

   f = fn x => if null x then 1 else hd x + 1

As usual, use capital letters in the range P .. Z for the unification
type variables. The list functions null and hd have their usual
polymorphic types.

ANS: Assume a base context Cbase that assigns the usual types to
null, hd, and +.  Assign x the initial type variable X:

   C0 = F(x, X, Cbase)

Use this as the context to type the body:

a. C0 ⊦ (null x) : ?
   null : U list -> Bool  (lookup in C0, instantiate polytype)
   x: X   (lookup in C0)
   X = U list  ==> substitution: s0 = X ↦ U list
   null x : Bool   (App rule)
   ==> C1 = F(x, U list, cBase)  (subContext(s,cBase) = cBase)

b. C1 ⊦ 1 : Int  (Int rule)
   (no unifications, so no change in context)

c. C1 ⊦ hd x : ?
   hd : V list -> V  (lookup in C1, instantiate polytype)
   x : U list        (lookup in C1)
   U list = V list   (App rule -- unify domain, arg types)
   U = V  ==>  s1 = U ↦ V  (unify, producing subst s1)
   hd x : V          (App rule -- function range type)
   ==> C2 = F(x, v list, cBase)  (subContext(s1,cBase) = cBase)
  
d. C2 ⊦ 1 : Int  (int constant rule)

e. C2 : hd x + 1 : ?
   + : Int * Int -> Int   (lookup in C2)
   (hd x, 1) : V * Int    (Pair rule)
   Int * Int = V * Int    (App rule -- unify domain, arg types)
   V = Int  ==>  s2 = V ↦ Int  (unify, producing subst s2)
   hd x + 1 : Int         (App rule -- function range type)
   ==> C3 = F(x, Int list, cBase)  (subContext(s2,cBase) = cBase)

f. C3 ⊦ if null x then 1 else hd x + 1 : Int  (If rule, given a,d,e)
  
g. Cbase ⊦ fn x => if null x then 1 else hd x + 1 : Int list → Int  (Fun rule)

h. Cbase ⊦ f = ... : L(f, Int list → Int, [], Cbase)
   because Int → Int has no free type variables, generalizeTy(Int →
   Int) produces no polymorphically quantified type variables.


4. [10] Give the type of the function h in the context of the
following definition (this type will involve types of other variables
in the declaration of f). Just the type is required, not a full
derivation of it.

  fun f x =
      let val y = x::nil
	  fun g z = (rev z, x) :: nil
	  fun h u = tl (g u)
       in h [1,2] end;

ANS: h : 'a list -> ('a list * X) list,
     where X is the type of x (eventually generalized to 'a in
     the type f : 'a -> (Int list * 'a) list


5. [15] (a) What is the type of the following function f?  (b) What
does it do?  (c) Redefine it using one of the list fold functions
(foldl or foldr).

  fun f (nil, ys) = ys
    | f (x::xs, ys) = f (xs, x::ys)


ANS: (a) f : 'a list * 'a list -> 'a list
  (b) It appends the reverse of its first argument onto its second.
  (c) fun f(l,m) = foldl (op ::) m l


6. [25] Represent a labeled binary tree using the datatype:

  datatype 'a tree
    = Lf                             (* leaf node *)
    | Br of 'a * 'a tree * 'a tree   (* branch node labeled by 'a *)
 
Write a function that determines whether two arbitrary trees 
t and u satisfy t = reflect u, where reflect is defined by:

  (* reflect : 'a tree -> 'a tree *)
  fun reflect Lf = Lf
    | reflect (Br(v,t1,t2)) = Br(v, reflect t2, reflect t1)

It relects a tree horizontally into a "mirror image" of itself.

The function specification will be:

   val mirror : ''a tree * ''a tree -> bool

It has an equality polymorphic type because generic equality will
have to be used to compare labels having the type ''a.

ANS:

   fun mirror (Lf, Lf) = true
     | mirror (Br(x,t1,t2), Br(y,u1,u2)) =
       (x = y) andalso mirror(t1,u2) andalso mirror(t2,u1)
     | mirror _ = false