Lab #6 Solution




1    Introduction


The goal for this lab is to make you more familiar with higher-order functions, polymorphism, and currying in Standard ML.

Please take advantage of this opportunity to practice  writing functions and proofs with the assistance of the TAs and your classmates.  You are, as always, encouraged to collaborate with your classmates and to ask the TAs for help.



1.1     Getting Started


Update your clone of the git repository to get the files for this weeks lab as usual by running


git pull


from the top level directory  (probably  named 15150).



1.2     Methodology


You must  use the  five step methodology  for writing  functions  for every function  you write on this  assignment.   In particular, every function  you write  should have REQUIRES  and ENSURES clauses and tests.


2    Higher Order Functions with Polymorphism



Task 2.1  For each of the following expressions, what  is its most general type?  Recall that map has type (’a -> ’b) -> ’a list -> ’b list. If you think the expression is not well- typed, say so.


(a)  (fn x => x+1.0)


(b)  map (fn x => x ^ “Hello”)


(c)  map (fn x => x + 1) [41]


(d)  map (fn l => map (fn x => x) l)


(e)  map map



3    Folding a List


The foldr function was defined in class. Here is its type and definition:


foldr : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b



fun foldr g z []    = z

| foldr g z (x::L) = g(x, foldr g z L);


foldr can be used in place of recursive functions.  For instance, take a look at the function

sum that  takes an int list and computes the sum of its elements:


fun sum (L : int list) : int =

case L of

[]   => 0

| x::xs => x + (sum xs)


We can rewrite this function using foldr without  recursion as:


fun sum’ (xs : int list) : int = foldr (fn (x,y) => x + y) 0 xs


3.1     Proving with Higher-Order-Functions



Task 3.1  Prove  that  the  two  implementations of sum are equivalent.   That  is, prove the theorem


Theorem:  For any L : int list, sum L = sum’ L.


Your proof should use structural induction  and equational  reasoning.




3.2     Quantifiers



Task 3.2 Using foldr, write


exists : (’a -> bool) -> ’a list -> bool forall : (’a -> bool) -> ’a list -> bool


such that  when p is a total  function of type t -> bool, and L is a list of type t list:


  • exists p L =⇒∗ true if there is an x in L such that p x = true;

exists p L =⇒∗ false otherwise


  • forall p L =⇒∗ true if p x = true for every item x in L;

forall p L =⇒∗ false otherwise.


Hint: Write these functions recursively at first, and then convert them to use foldr as was done with sum.


4    Higher Order Trees


Recall our definition of binary  trees:


datatype ’a tree = Empty

| Node of ’a tree * ’a * ’a tree




4.1     Implementation


We will be working with some higher-order  functions on these trees.


Task 4.1 Define a recursive ML function


treeFilter : (’a -> bool) -> ’a tree -> ’a option tree


such that  treeFilter p t keeps tree  elements  that  satisfy  p by wrapping  them  in SOME

while replacing those elements that  fail with NONE.


Task 4.2 Define a recursive ML function


treexists : (’a -> bool) -> ’a tree -> ’a option


such that  treexists p t evaluates  to SOME e where e is any element of t that  satisfies p

and NONE if no such element exists.


Task 4.3 Define a recursive ML function


treeAll : (’a -> bool) -> ’a tree -> bool


such that  treeAll p t evaluates to true if and only if every element of t satisfies p. Please do not use treexists.


Task 4.4 Define an ML function


treeAll’ : (’a -> bool) -> ’a tree -> bool


that  is non-recursive but  works identically  to treeAll. You may use treexists.



4.2     Polymorphism



Task 4.5


(a)  What  is the most general type of the following function?


fun foo t = treeFilter (fn [] => false | x::L => true) t


(b)  What  does it do?


4.3     Trees on  trees



Task 4.6 Please define an ML function


onlyEvenTrees : (int tree) tree => (int tree option) tree


such that  onlyEvenTrees t evaluates  to a tree  that  has NONE wherever t had a tree  con- taining  any odd number  and SOME e wherever t had a tree e containing  no odd numbers.



4.4     Do  the safetree dance



Task 4.7 We were perfectly happy with our tree implementation until some c hax0rs mu- tated  our trees.  Please write a non-recursive function:


safetree : int tree -> int option tree


which transforms  each Leaf(n) to Leaf(NONE) if n = 0, and Leaf(SOME n) otherwise.


5    More Trees


Oftentimes  we want  a tree  with  more than  two  branches  at  any  node.   For  example,  the B-trees used to implement your filesystem have arbitrary branching  factor (post-lab  reading for the curious:!

We can extend our definition of binary  trees to trees with an arbitrary branching  factor with the following datatype:


datatype ’a narytree = Emp

| Bud of ’a

| Branch of ’a narytree list


Notice how we already  have an Emp type  in the  tree  – to avoid being redundant, we will impose an invariant requiring the ’a narytree list in Branch to be non-empty.


Task 5.1 Remember making ”full” rtrees with geometricTree on HW 4? Note that  it can only make a tree with 2n  leaves for a given n – it’s pretty  boring.  Define an ML function


fuller : (int * int) -> int narytree


that  for some non negative n and positive a, returns  an n-ary tree of depth a, with na leaves each containing  your favorite number.



5.1     Higher-Order Functions (again)


If you haven’t  already  guessed, we can extend  the  same higher  order  functions  on binary trees to n-ary trees!


Task 5.2 Define an ML function


narytreemap : (’a -> ’b) -> (’a narytree -> ’b narytree)


for applying a function to every leaf in an n-ary tree.


Task 5.3 Define an ML function


narytreereduce : (’a * ’a -> ’a) -> ’a -> ’a narytree -> ’a


for combining the items at the leaves of an n-ary tree with some base value.


Task 5.4 Define an ML function


narytreemapreduce : (’a -> ’b) -> (’b * ’b -> ’b) -> ’b -> ’b narytree -> ’b


for mapping a function to every leaf in an n-ary tree and then combining the resulting leaves with a base value.  (This should be non-recursive.)

Note:  There  is at  least  one implementation of mapreduce  which  stores  a  tree-sized intermediate result.  You should probably  try  this first!  Challenge:  can we do without  this intermediary?