* Folds for algebraic data types

For all algebraic data types 'T', the following can be mechanically derived:

 An induction scheme to prove properties P :: T -> Bool for all v::T.

 A fold function that reduces a value a::T to some value of type B
   given functions that reduce the different constructors.

(We will focus on the second aspect today.)

> data Unit = U

> foldUnit  
>   :: b 
>     -> Unit 
>     -> b
> foldUnit    fU   U     = fU

To define a function of type Unit -> b, give return value for U.

> data Boolean = T | F

> foldBoolean 
>   :: b 
>     -> b 
>     -> Boolean 
>     -> b
> foldBoolean    fF   fT   T        = fT
> foldBoolean    fF   fT   F        = fF

To define a function of type Boolean -> b, give the return value for T and
the return value for F.

> data IList = INil | ICons Int IList

> foldIList 
>   :: b 
>     -> (Int -> b -> b) 
>     -> IList  
>     -> b
> foldIList fINil fICons INil = fINil
> foldIList fINil fICons (ICons i l) = fICons i (foldIList fINil fICons l)

To define a function of type IList -> b, give the return value for INil and
a function that combines an Int and a value of type b (the result of
reducing the second argument of ICons) to a value of type b.

* Folds for algebraic data types II

Derivation of the type of the fold function:

> data Tree a = Leaf | Node a (Tree a) (Tree a)

Leaf :: Tree a
Node :: a -> Tree a -> Tree a -> Tree a
==>
fLeaf :: b
fNode :: a -> b -> b -> b

foldTree :: b -> (a -> b -> b -> b) -> Tree a -> b
foldTree fLeaf fNode t = go t
  where go Leaf           = fLeaf
        go (Node x t1 t2) = fNode x (go t1) (go t2)


* Folds for algebraic data types II

Derivation of the type of the fold function:

> data T a = T1 | T2 (T a) String (T a) Int | T3 (T a) (T a) (T a)

T1 :: T a
T2 :: T a -> String -> T a -> Int -> T a
T3 :: T a -> T a -> T a -> T a
==>
for the corresponding argument functions to foldT, replace T a with b.

fT1 :: b
fT2 :: b -> String -> b -> Int -> b
fT3 :: b -> b -> b -> b

Then the actual fold functions just pattern matches on the constructors of
the data type, recursively calls itself, and applies the given functions.

> foldT 
>   :: b 
>     -> (b -> String -> b -> Int -> b) 
>     -> (b -> b -> b -> b) 
>     -> T a 
>     -> b
> foldT fT1 fT2 fT3 t = go t
>   where go T1             = fT1
>         go (T2 t1 s t2 i) = fT2 (go t1) s (go t2) i
>         go (T3 t1 t2 t3)  = fT3 (go t1) (go t2) (go t3)

Exercise: Give the fold function for the following data type.

> data G a b = A Int | B (G a b) Bool (G a b) | C a b

A :: Int -> G a b
B :: G a b -> Bool -> G a b -> G a b
C :: a -> b -> G a b

fA :: Int -> c
fB :: c -> Bool -> c -> c
fC :: a -> b -> c

> foldG 
>   :: (Int -> c) 
>     -> (c -> Bool -> c -> c) 
>     -> (a -> b -> c) 
>     -> G a b 
>     -> c
> foldG  fA  fB  fC  g = go g
>  where go (A i) = fA i
>        go (B l b r) = fB (go l) b (go r)
>        go (C x y)   = fC x y