Functional Programming Exercise Session 5

Write two functions:

tabulate : List a -> (Nat -> Maybe a)

and

recover : (Nat -> Maybe a) -> List a

such that (recover . tabulate) : List a -> List a does the same thing as the identity function id : List a -> List a, as in:

> recover (tabulate [1,2,3])
> [1,2,3]

The idea is that functions like

zero_to_nine : (Nat -> Maybe Nat)
zero_to_nine n = if n < 10 then Just n else Nothing

denote lists, as in:

> recover zero_to_nine
> [0,1,2,3,4,5,6,7,8,9]

(Harder): Do all functions Nat -> Maybe a denote lists in this way? Put another way, is there a total function recover_all : (Nat -> Maybe a) -> List a such that (tabulate . recover) does the same thing as the identity function? If so, implement recover_all. If not, can you characterize the functions (Nat -> Maybe a) that denote lists in this way?
Suppose (Nat -> Maybe a) denotes a list in the manner considered above. Write a function
```
tabTail : (Nat -> Maybe a) -> (Nat -> Maybe a)
```
that returns the tail of a tabulated list, without using the recover function. (That is, without transforming the input into a List a at any point). Next, write a function
```
tabMap : (a -> b) -> (Nat -> Maybe a) -> (Nat -> Maybe b)
```
which does simulates map : (a -> b) -> List a -> List b on our encoded lists. Again, try not to use the recover function.
Define the data type of binary trees:
```
data Tree : Type -> Type where
  Leaf : Tree a
  Node : Tree a -> a -> Tree a -> Tree a
```
In which, for example,
```
example_tree : Tree Nat
example_tree = Node (Node (Node Leaf 1 Leaf) 2 (Node Leaf 3 Leaf)) 4 (Node Leaf 5 (Node Leaf 6 Leaf))
```
denotes the tree
```
 4
/ \
  2   5
 / \   \
1   3   6
```
Recall that the “in-order” traversal of a tree begins at the root, visits the left subtree, the current node, and then the right subtree. Write a function
```
in_order : Tree a -> List a
```
which performs an in-order traversal of the input tree, returning the list values stored in the tree in the order they visited. For example,
```
 > in_order example_tree
 > [1,2,3,4,5,6]
```
Next, recall that the post-order traversal visits the left subtree, then the right subtree then the current node, and that the pre-order traversal visits the current node, the left subtree, and then the right subtree. Write similar functions
```
pre_order : Tree a -> List a
post_order : Tree a -> List a
```
that perform these traversals. For example:
```
 > pre_order example_tree
 > [4,2,1,3,5,6]
 > post_order example_tree
 > [1,3,2,6,5,4]
```
should be the result of each function on the example.
Write a function
```
insert : Nat -> Tree Nat -> Tree Nat
```
where insert n t is the result of inserting n into tree t such that if t was sorted, so is insert n t. More preciesly, say that a tree t is sorted in case the list in_order t is sorted. Next, write a sorting function
```
sort : List Nat -> List Nat
```
that sorts a list by building a tree out of it, then traversing the tree.
Define the type of paths in a binary tree to be
```
Path : Type
Path = List Bool
```
and define a function
```
follow : Path -> Tree a -> Maybe a
```
that follows the input path through the input tree, returning the value stored at the end of the path, if any. The idea is that, if we imagine outselves standing at the root of the tree, then the first element of the path tells us whether to walk to the left subtree (for, say False), the right subtree (for True), or that we have reached the end of the path (in case it is empty). For example:
```
 > follow [True, True] example_tree
 > Just 6
 > follow [False, True] example_tree
 > Just 3
 > follow [False, False, True] example_tree
 > Nothing
```
Define a function
```
path_to : Nat -> Tree Nat -> Maybe Path
```
such that path_to x t returns a path to x in tree t if any exist. For example,
```
 > path_to 6 example_tree
 > Just [True,True]
```
and so on.
In the questions involving the Tree type, sometimes you were asked to write functions that would work for Tree a for any type a, and other times were only asked to write functions that would work for Tree Nat. Why?