The idea of this exercise set is to give you lots of things to write using the fold functions for datatypes we have seen in class. Recall:
foldNat : b -> (b -> b) -> Nat -> b foldNat z s Z = z foldNat z s (S n) = s (foldNat z s n) foldList : (a -> b -> b) -> b -> List a -> b foldList = foldr data Tree : Type -> Type where Leaf : Tree a Node : Tree a -> a -> Tree a -> Tree a foldTree : b -> (b -> a -> b -> b) -> Tree a -> b foldTree l n Leaf = l foldTree l n (Node tl x tr) = n (foldTree l n tl) x (foldTree l n tr)
You should try to use these folds to solve the exercises. Note that it is often easier to write a solution that does not use a fold first, and then try again once you understand how to do it without one.
andList : List Bool -> Bool orList : List Bool -> Bool
(andList xs) is
True if and only if each element of
True and, dually,
(orList xs) is
False if and only if each element of
Now, write functions
multList : List Nat -> Nat addList : List Nat -> Nat
(multList xs) is the result of multiplying all the elements of
xs together, and
(addList xs) is the result of adding all the elements of
Do your answers to parts a and b suggest a relatoinship between logical conjunction / disjunctoin and arithmetic product / sum? What is the connection?
exp : Nat -> Nat -> Nat
(exp a b) is
a ^ b, that is,
a to the power of
flatten : List (List a) -> List a
such that, for example
> flatten [[1,2,3],,[4,5]] > [1,2,3,4,5]
filter : (a -> Bool) -> List a -> List a
The idea is that
(filter p xs) is the list consisting of those elements of
xs such that
p xs is
True, in the same order they occured in
xs. For example
> filter (<=5) [7,1,6,3,1,4] > [1,3,1,4]
reverseTree : Tree a -> Tree a
that reverses a tree in the following sense: (tilt head 45 degrees to the left to read trees)
4--5 4--2--1 | | | 2--3 |---reverseTree--> 5 3 | 1
andTree : Tree Bool -> Bool orTree : Tree Bool -> Bool addTree : Tree Nat -> Tree Nat multTree : Tree Nat -> Tree Nat
that do for
Trees what the functions you wrote in part 1 did for lists.
in-order : Tree a -> List a pre-order : Tree a -> List a post-order : Tree a -> List a
beadthFirst : Tree a -> List a
that returns the breadth-first traversal of the input tree.
That’s the end of the exercise set, but remember that you should try to do all of these using folds!