(*               CSE505 Homework 3 Sample Solutions             *)


(* 1. *)
(*
The list representation of trees requires the list to contain both
other lists (representing subtrees) as well as some kind of data
(representing leaves).  ML's strong type system requires that lists be
homogeneous, i.e., contain elements of a single type, so any function
which relies on the above tree representation will not typecheck.

Moreover, in Scheme we used both head and tail of a cons cell to keep
the two subtrees, while in ML head and tail cannot be of the same type.
This could be worked around, however, by using pairs instead of lists,
but then the problem discussed above arises.
*)


(* 2. *)

(* Because we have data at the internal nodes, we call the FUNC twice: once
   on the reduction of the left and right subtrees, and once on the value
   stored at the current node and the result of the first FUNC call.     *)
fun reduce_tree func base leaf_fn (Tree {tree=tr, eq=_, lt=_}) =
  (* a helper function *)
  let fun reduce_tr Empty = base
        | reduce_tr (Node(x, t1, t2)) =
	      func(leaf_fn x, func(reduce_tr t1, reduce_tr t2))
  in
      reduce_tr tr
  end;

(* SUM_TREE function in terms of REDUCE_TREE *)
fun sum_tree tree = reduce_tree (op+) 0 (fn x=>x) tree;

(* or use the fact that reduce_tree is curried *)
val sum_tree = reduce_tree (op+) 0 (fn x=>x);


(* 3 *)

fun compose_list nil elem = elem
  | compose_list (f::fs) elem = f (compose_list fs elem);



(* 4

1. REDUCE_TREE
   (*
    NOTE: this inference is performed for the following version of reduce_tree:
    fun reduce_tr func base leaf_fn Empty = base
      | reduce_tr func base leaf_fn (Node(x, t1, t2)) =
	    func(leaf_fn x,
	         func(reduce_tr func base leaf_fn t1,
		      reduce_tr func base leaf_fn t2));
    fun reduce_tree func base leaf_fn (Tree {tree=tr, eq=_, lt=_}) =
	    reduce_tr func base leaf_fn tr;
   * )

reduce_tr:
  parm1 : 'a
  parm2 : 'b
  parm3 : 'c
  parm4 : 'd
  result : 'e

constraints from line 1 of the function:
  func : 'f, so 'a = 'f
  base : 'g, so 'b = 'g
  leaf_fn : 'h, so 'c = 'h
  Empty : 'i tr, so 'd = 'i tr
  base : 'g, so 'e = 'g

constraints from line 2 of the function:
  func : 'j, so 'a = 'j
  base : 'k, so 'b = 'k
  leaf_fn : 'l, so 'c = 'l
  Node(x,t1,t2) : 'm tr, so 'd = 'm tr, x : 'm, t1 : 'm tr, t2 : 'm tr
  x : 'm, so leaf_fn : 'm ->'n, 'c = 'm->'n, (leaf_fn x) : 'n
  (reduce_tr func base leaf_fn t1) : 'e, so 'n = 'e
  (reduce_tr func base leaf_fn t2) : 'e, so
	(func ((reduce_tr func base leaf_fn t1),
	       (reduce_tr func base leaf_fn t2))) : 'e,
	func : ('e * 'e)->'e

Putting this all together, we find the following equivalences:

  'a = 'f = 'j = ('e * 'e)->'e
  'b = 'g = 'k = 'n = 'e
  'c = 'h = 'l = 'm->'n
  'd = 'i tr = 'm tr

so finally

  'a = ('e * 'e)->'e
  'b = 'e
  'c = 'm->'e
  'd = 'm tr
  'e = 'e

Rewriting 'e to 'a and 'm to 'b, we get the type of reduce_tr:
	('a*'a->'a)->'a->('b->'a)->'b tr->'a

Now deducing the type of reduce_tree is simple:

reduce_tree:
  parm1 : 'a
  parm2 : 'b
  parm3 : 'c
  parm4 : 'd
  result: 'e

constraints:
  Tree{...} : 'f tree, so 'd = 'f tree
  reduce_tr : ('g*g->'g)->'g->('h->'g)->'h tr->'g, so
	'a = 'g*g->'g
	'b = 'g
	'c = ('h->'g)
	tr : 'h tr, so Tree : 'h tree, so 'h = 'f
	'e = 'g

Renaming 'g to 'a and 'h to 'b, we find the type of reduce_tree:
	('a*'a->'a)->'a->('b->'a)->'b tree->'a


2. COMPOSE_LIST

compose_list:
  parm1 = 'a
  parm2 = 'b
  result= 'c

constraints from line 1 of the function:
  nil : 'd list, so 'a = 'd list
  elem : 'e, so 'b = 'e
  elem : 'e, so  'c = 'e

constraints from line 2 of the function:
  (h::t) : 'f list, so 'a = 'f list, h : 'f,
		t : 'f list
  elem : 'g, so 'b = 'g
  t : 'f list, so 'a = 'f list
  elem : 'g, so h : 'g->'h, 'f = 'g->'h
  (h elem) : 'h, so 'b = 'h

Putting this all together, we have the following equivalences:

  'a = 'd list = 'f list
  'b = 'e = 'g = 'h
  'c = 'e
  'f = 'g->'h

and finally

  'a = ('h->'h) list
  'b = 'h
  'c = 'h

Rewriting 'h to 'a, we get the type of compose_list:
('a->'a) list -> 'a -> 'a

*)


(* 5 *)

(*
First, lists in ML must be homogeneous, so the argument types of all
the functions to be composed must be the same, and so must be result
types.  In Scheme, it is sufficient that the result of each function
on the list be accepted by the preceeding function.  For example,
compose_list cannot be used to combine a function that parses a string
as an integer and then negates it.

A more subtle advantage of Scheme is that ML disallows binding
variables to polymorphic expressions, so if the result of compose_list
is a polymorphic value, it cannot be stored.  (It can be used right
away, however.)  Defining cddr as
	val cddr = compose_list [tl,tl];
is an example.
*)