Description

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: en.wikipedia.org/wiki/B-tree)!

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?