Given an algebraic data type such as: data List a = Nil | Cons a (List a) You can define its recursion principle by building a higher-order function that

Given an algebraic data type such as: data List a = Nil | Cons a (List a) You can define its recursion principle by building a higher-order function that receives an element of your type and, for each constructor, receives a function that takes all the parameters of that constructor (with any recursive parameters replaced by `r`) and returns `r`. For `List` this becomes: foldr :: (() -> r) -> (a -> r -> r) -> List a -> r The eliminator for `Nil` can be simplified to `r` as `() -> r` is isomorphic to `r`: foldr :: r -> (a -> r -> r) -> List a -> r foldr z f Nil = z foldr z f (List a xs) = f a (foldr f z xs) For `Bool`: data Bool = True | False We get: bool :: a -> a -> Bool -> a bool p q True = q bool p q False = p Which is precisely an If statement as a function! :D