CMSC 22300
Homework 2, Due Wednesday 4/154/2010

1. [50] type checking

Manually typecheck the following definitions and expressions,
following the pattern on Script 4. These definitions are not
necessarily well-typed, so you may discover a type error, which
will manifest itself in a constraint equation that has no 
solution.

(a) [10] appending lists (similar to length):

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


(b) [10] another nested function example

    fun f x =
        let fun g y = x
         in g true + 1
        end


(c) [5] a curried function

    fun f x y = (x,y)

This is equivalent to 

    val f = fn x => (fn y => (x,y))


(d) [10] a function using the conditional (if .. then .. else ..)

    fun take(n, xs) = if n = 0 then nil else hd xs :: take(n-1, tl xs)

[hd and tl are the polymorphic operations returning the head and
tail, respectively, of a list (same as car, cdr in scheme).]

The rule for typing conditional expressions is

     C |- e1 : bool     C |- e2 : t     C |- e3 : t
   --------------------------------------------------
            C |- if e1 then e2 else e3 : t

that is, we must establish that e1 has type bool and that the
branch expressions e2 and e3 have the same type, which becomes
the type of the if expression.


(e) [15] doubly nested function definitions

    fun f x = 
        let fun h y =
                let fun g z = z :: y
                 in g x
                end
         in h x
        end


2. [40] Binary trees (Paulson p 141)

Binary trees are represented by the datatype

datatype 'a tree
  = Lf                               (* leaf node *)
  | Br of 'a * 'a tree * 'a tree     (* binary branch node labed with 'a value *)

(a) [20] Exercise 4.14 (p. 144): A binary tree is balanced (by size) if each node
Br(x,t1,t2) satisfies |size(t1) - size(t2)| <= 1. The obvious recursive 
function to test whether a tree is balanced applies size at every subtree,
performing much redundant computation. Write an efficient function to test
whether a tree is balanced.

(b) [20] Exercise 4.15. Write a function that determines whether two arbitrary trees 
t and u satisfy t = reflect u. The function should not build any new trees,
so it should not call reflect or Br, although it may use Br in patterns.

[reflect is defined earlier on page 114:

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


3. [20] Here is a different version of binary trees, with values labeling
the leaf nodes rather than the branch nodes.

datatype 'a tree
  = Lf of 'a
  | Br of 'a tree * 'a tree

We will call the fringe of such a tree the list of values at the
leaf nodes, going from left to right.

fun fringe (Lf v) = [v]
  | fringe (Br(t1, t2)) = fringe t1 @ fringe t2

This version of fringe is not very efficient.  Define a better
fringe function that only needs to use :: to build the fringe list. 

Hint: define a tail-recursive auxiliary function fringe1 with an
accumulator argument, and then define fringe in terms of fringe1
passing the appropriate initial value for the accumulator.

Example: to reverse a list

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

fun rev xs = rev1(xs,nil)


4. [25] (Hard) Define a function samefringe on the trees from Problem 3
that tests whether two trees have the same fringe, given an
equality function for the leaf label values. But do so without
actually computing the fringe for either tree!

  samefringe : ('a * 'a -> bool, 'a tree, 'a tree) -> bool

Hint: the idea is a bit like the solution of Problem 3. The function
has to do a kind of parallel depth first traversal of the two trees,
with auxiliary arguments keeping track of the parts of the trees yet
to be examined.