Poniższe ćwiczenie odnosi się do rozdziału 9 "Dependent Data Structures"
-
Define a tree analogue of hlist. That is, define a parameterized type of binary trees with
data at their leaves, and define a type family htree indexed by trees. The structure of
an htree mirrors its index tree, with the type of each data element (which only occur
at leaves) determined by applying a type function to the corresponding element of the
index tree.
-
Define a type standing for all possible paths from the root of a tree to
leaves and use it to implement a function tget for extracting an element of an htree
by path.
-
Define a function htmap2 for “mapping over two trees in parallel.” That is,
htmap2 takes in two htrees with the same index tree, and it forms a new htree with
the same index by applying a binary function pointwise.
-
Repeat this process so that you implement each definition for each of the three
definition styles covered in this chapter: inductive, recursive, and index function.