Examples

Natural Numbers

Initial algebra of the functor F(X) = 1 + X

data Nat = Zero | Succ Nat

Lists

Initial algebra of F(X) = 1 + A × X

data List a = Nil | Cons a (List a)

Binary Trees

Initial algebra of F(X) = A + X × X

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

Lambda Calculus

The classic fixed-point combinator

Y = λf.(λx.f(x x))(λx.f(x x))

Factorial via Y

Recursion without self-reference

fact = Y (λf.λn. if n=0 then 1 else n * f(n-1))