Recursion schemes.

Last modified on November 24, 2018 by Alex


Folding a list.

Say we have a data type,

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

and we would like to fold over this data structure:

foldr :: forall a z. z -> (a -> z -> z) -> List a -> z
foldr nil cons = go where
  go Nil        = nil
  go (Cons h t) = cons h (go t)

Let’s look at the type of foldr and make some isomorphic transformations (see Counting Type Inhabitants for some extra techniques that are useful when dealing with isomorphisms):

 a z. z -> (a -> z -> z) -> List a -> z
~  a z. (1 -> z) -> (a * z -> z) -> List a -> z
~  a z. ((1 + a * z) -> z) -> List a -> z
-- define ListF a z = 1 + a * z
~  a z. (ListF a z -> z) -> List a -> z

We can define ListF as:

data ListF a z = NilF | ConsF a z

Armed with this new data type, and the new type signature for foldr, we rewrite it as:

foldr :: forall a z. (ListF a z -> z) -> List a -> z
foldr alg = go where
  go Nil        = alg NilF
  go (Cons h t) = alg (ConsF h (go t))

Trying a different ADT

Let’s start with a different ADT to see if we can use the same technique as we did for lists:

data Expr = Lit Int | Add Expr Expr | Mul Expr Expr

foldExpr :: forall z. (Int -> z) -> (z -> z -> z) -> (z -> z -> z) -> Expr -> z
foldExpr lit add mul = go where
  go (Lit i)    = lit i
  go (Add l r)  = add (go l) (go r)
  go (Mul l r)  = mul (go l) (go r) 
 z. (Int -> z) -> (z -> z -> z) -> (z -> z -> z) -> Expr -> z
~  z. (Int -> z) -> (z * z -> z) -> (z * z -> z) -> Expr -> z
~  z. ((Int + z * z + z * z) -> z) -> Expr -> z
-- define ExprF z = Int + z * z + z * z
~  z. (ExprF z -> z) -> Expr -> z

We can define ExprF as:

data ListF z = LitF Int | AddF z z | MulF z z

Back to lists

Let’s continue our List transformations, perhaps we can notice something else:

 a z. (ListF a z -> z) -> List a -> z
~  a. List a -> ( z. (ListF a z -> z) -> z)
~  a. List a -> (μ z. ListF a z)
-- define List' a = μ z. ListF a z
~ List :~> List'

We see that foldr’s type tells us it is isomorphic to a natural transformation from List to a structure of nested ListFs. Note that our specific instance (foldr) of that type is actually a natural isomorphism, or at least one part of it. What is the other part?

It’s signature,

List' :~> List
~ forall a. (μ z. ListF a z) -> List a
~ forall a. (forall z. (ListF a z -> z) -> z) -> List a

is not particularly insightful. But its implementation,

transform :: forall a. (forall z. (ListF a z -> z) -> z) -> List a
transform go = go $ \case
    NilF      -> Nil
    ConsF a z -> Cons a z

is rather interesting.

What happens is that given a forall z. (ListF a z -> z) -> z, we first substitute z = List a, obtaining (ListF a (List a) -> List a) -> List a and then pass it a function that embeds a pattern functor ListF a (List a) into List a. Let’s call this function embed:

embed :: ListF a (List a) -> List a
embed NilF        = Nil
embed (ConsF a z) = Cons a z

And now we can write transform as:

transform go = go embed

Ahh, this is quite satisfying.

Let’s now go back to foldr:

foldr :: forall a z. (ListF a z -> z) -> List a -> z
foldr alg = go where
  go Nil        = alg NilF
  go (Cons h t) = alg (ConsF h (go t))

A reader with a minor OCD might notice that if embed was perfectly symmetric, the second case of go here is not symmetric. Ideally we would like to have ConsF h t :: ListF a (List a) and then somehow transform it into ConsF h (go t) :: ListF a z. What does it remind you of? An fmap!

instance Functor (ListF a) where
  fmap f NilF       = NilF
  fmap f (Cons a x) = Cons a (f x)

Now we can rewrite foldr as:

foldr :: forall a z. (ListF a z -> z) -> List a -> z
foldr alg = go where
  go Nil        = alg NilF
  go (Cons h t) = alg $ fmap go $ (ConsF h t)

And factoring out project :: List a -> ListF a (List a):

project :: List a -> ListF a (List a)
project Nil        = NilF
project (Cons a z) = ConsF a z

foldr :: forall a z. (ListF a z -> z) -> List a -> z
foldr alg = go where
  go = alg . fmap go . project

Note the symmetry of project and embed. In particular, it is easy to show that project . embed = id and embed . project = id, so they are two parts of an isomorphism between ListF a (List a) and List a.

What happens if we pass embed into foldr?

foldr embed = go where
  go = embed . fmap go . project

What does go do? I suggest taking a few moments or minutes to convince yourself that go above (specialized for embed) is just an identity function on lists.

Generalizing

By following the same exact methodology as above, we can similarly derive:

embedExpr :: ExprF Expr -> Expr
embedExpr (LitF i)   = Lit i
embedExpr (AddF l r) = Add l r
embedExpr (MulF l r) = Mul l r

projectExpr :: Expr -> ExprF Expr
projectExpr (Lit i)   = LitF i 
projectExpr (Add l r) = AddF l r 
projectExpr (Mul l r) = MulF l r

foldExpr :: forall z. (ExprF z -> z) -> Expr -> z
foldExpr alg = go where
  go = alg . fmap go . projectExpr

This suggests that we can generalize folding over different data types by using a typeclass:

type Algebra f a = f a -> a

newtype Mu f = Mu (forall a. Algebra f a -> a)

class Functor f => Recursive t f | t -> f where
  project :: t -> f t
  embed :: f t -> t

  cata :: Algebra f a -> t -> a
  cata alg = go where
    go = alg . fmap go . project

  embed' :: Mu f -> t
  embed' (Mu go) = go embed

Note that I added two new type definitions, Algebra f a.

Algebra f a
~ f a -> a

which is also known as F-Algebra, and Mu f:

Mu f
~ forall a. Algebra f a -> a
~ forall a. (f a -> a) -> a
~ μ a. f a

foldr became cata, which stands for catamorphism.

Further note that Recursive t f is usually defined entirely in terms of project (so there is no embed nor embed'), but this is not completely satisfactory as there is always an embed when there is project, since together they form an isomorphism between t and f t.

An aside: F-algebras

As we defined above,

Algebra f a
~ f a -> a

Assuming that f is a Functor, this is called F-algebra, a is called the carrier and f the signature of the algebra. Note that F in F-algebra stands for f, a particular functor. However people often call algebras F-algebras in colloquial speech even if there is no one particular f.

F-Algebras form a category,

  • Objects: F-algebras, arrows φ :: F a -> a. F is a fixed functor for all objects of this category. Note that a is not universally quantified here, but rather fixed to a particular object of the underlying category.
  • Arrows: triples of (f, φ, ψ) where φ and ψ are F-algebras and f :: cod φ -> cod ψ is a homomorphism from φ to ψ, which means that f ∘ φ = ψ ∘ F f. Assuming that φ :: F a -> a and ψ :: F b -> b, it means that mapping F a first with a -> b and then reducing F b with ψ is the same as first reducing it with F a -> a and then applying a -> b. Here is an example of three algebras and two homomorphisms (one of them is almost an isomorphism):

    -- functor
    data F a = Lit Int | Add a a | Mul a a
    -- first algebra
    φ :: F [[Int]] -> [[Int]]
    φ   (Lit x) = [[x]]
    φ (Add x y) = x ++ y
    φ (Mul x y) = (++) <$> x <*> y
    -- second algebra
    ψ :: F Int -> Int
    ψ   (Lit x) = x
    ψ (Add x y) = x + y
    ψ (Mul x y) = x * y
    -- third algebra
    τ :: F [()] -> [()]
    τ   (Lit x) = replicate x ()
    τ (Add x y) = x ++ y
    τ (Mul x y) = (\_ _ -> ()) <$> x <*> y
    -- (f, φ, ψ) form an algebra homomorphism
    f :: [[Int]] -> Int
    f = foldr (+) 0 . fmap (foldr (*) 1)
    -- (g, ψ, τ) form an algebra homomorphism
    g :: Int -> [()]
    g = flip replicate ()
  • Identity is (id, φ, φ).
  • Composition is (f, φ₂, φ₃) ∘ (g, φ₁, φ₂) = (f ∘ g, φ₁, φ₃)

Now that we have defined a category, we should ask ourselves if this category has initial / terminal objects, products and coproducts, etc.

Turns out that for a lot of functors F, there is an initial object in the category of F-algebras, which is called initial F-algebra. An initial object of a category is such an object that there is a unique arrow from it to any other object. So in our case, an initial F-algebra is some morphism embed :: F μF -> μF (μF is some object of the underlying category) such that there is a unique homomorphism ⦇φ⦈ :: μF -> a to every other F-algebra φ :: F x -> x, where ⦇φ⦈ ∘ embed = φ ∘ F ⦇φ⦈. Let’s write it out as code:

-- functor
data F a = Lit Int | Add a a | Mul a a
-- initial algebra carrier
data μF = ???
-- initial algebra, known as `in` above
embed :: F μF -> μF
-- a unique ⦇φ⦈
cata :: forall x. (F x -> x) -> μF -> x
-- ⦇φ⦈ ∘ embed = φ ∘ F ⦇φ⦈
cata φ . embed = φ . fmap (cata φ)

Does this look familiar? These are almost all of the ingredients needed for Recursive μF F!

Before we continue, let’s review the laws that the initial algebra satisfies:

  • Cancellation: for any F-algebra φ, there is a unique ⦇φ⦈ such that ⦇φ⦈ ∘ embed = φ ∘ F ⦇φ⦈.
  • Reflection: Since ⦇embed⦈ is a unique homomorphism, it is necessarily an identity homomorphism id, therefore ⦇embed⦈ = id.
  • Fusion: For any two F-algebras φ : F a -> a, ψ : F b -> b and an arrow f : a -> b, f ∘ φ = ψ ∘ F f (a homomorphism condition) implies f ∘ ⦇φ⦈ = ⦇ψ⦈. This is again due to uniqueness. f ∘ ⦇φ⦈ is an algebra homomorphism between the initial algebra and ψ. But ⦇ψ⦈ is also a homomorphism between the initial algebra and ψ, hence by uniqueness of algebra homomorphisms out of the initial algebra, they are the same.

From these laws we can prove a fundamental theorem, known as Lambek lemma:

Lambek lemma

The initial algebra embed :: F μF -> μF is an isomorphism with the inverse defined as

project :: μF -> F μF
project = ⦇F embed⦈

Note that F embed :: F (F μF) -> F μF and ⦇F embed⦈ :: μF -> F μF as an algebra homomorphism from the initial F-algebra and an F-algebra with F μF as the carrier.

⦇embed⦈   :: μF -> μFF embed⦈ :: μF -> F μF
embed ∘ ⦇F embed⦈ :: μF -> μFF embed⦈ ∘ embed :: F μF -> F μF

embed ∘ ⦇F embed⦈
-- fusion
= ⦇embed⦈
-- reflection
= id

⦇F embed⦈ ∘ embed
-- cancellation
= F embed ∘ FF embed⦈
-- F is a functor
= F (embed ∘ ⦇F embed⦈)
-- see above
= F id
-- F is a functor
= id

If we look at the signature of cata a bit more closely,

 x. (F x -> x) -> μF -> x
~ μF ->  x. (F x -> x) -> x
~ μF -> μ x. F x

At the same time we can see that given mu :: μ x. F x, we can run mu embed and get a μF out, so the natural follow-up question is whether μF is isomorphic to μ x. F x ~ ∀ x. (F x -> x) -> x.

We will prove it in polymorphic lambda calculus.

cata :: Λ x. (F x -> x) -> μF -> x

from :: μF -> Λ x. (F x -> x) -> x
from muF = Λ x. λ (f : F x -> x). cata x f muF

to :: (Λ x. (F x -> x) -> x) -> μF
to muF = λ (f : Λ x. (F x -> x) -> x). f μF embed

to (from muF) 
= (λ (f : Λ x. (F x -> x) -> x). f μF embed) (Λ x. λ (f : F x -> x). cata x f muF)
= (Λ x. λ (f : F x -> x). cata x f muF) μF embed
= (λ (f : F μF -> μF). cata μF f muF) embed
= (cata μF embed) muF
-- using the homomorphism law

An aside: containers

An aside: derivatives

Folding with location

In this section we’ll discuss how to fold over a data structure while having some notion of location: e.g. if we are folding over a tree, we would like to know which path we took to arrive to a node. To motivate this problem, consider how you would accurately report that one of the tree nodes is erroneous.

Taking List’s derivative

First, let’s see what happens if we take a derivative of List a with respect to a:

∂ₐ(List a) 
= ∂ₐ(1 + a * List a)
= ∂ₐ(a) * List a + a * ∂ₐ(List a)
= List a + a * ∂ₐ(List a)
= List a * List a

On the other hand, as we have shown before, there is an isomorphism between List a and μ x . ListF a x, so

∂ₐ(List a) 
= ∂ₐ(μ x . ListF a x)
= ∂ₐ(ListF a (μ x . ListF a x))
= ∂ₐ(ListF a x)[x=μ x . ListF a x] +
  ∂ₓ(ListF a x)[x=μ x . ListF a x] * ∂ₐ(μ x . ListF a x)
= μ w . ∂ₐ(ListF a x)[x=μ x . ListF a x] +
        ∂ₓ(ListF a x)[x=μ x . ListF a x] * w
= ∂ₐ(ListF a x)[x=μ x . ListF a x] *
  List ∂ₓ(ListF a x)[x=μ x . ListF a x]
= x[x=μ x . ListF a x] *
  List a[x=μ x . ListF a x]
= List a *
  List a

Let’s put List a and ∂ₐ(List a) side by side:

List a     = μ w . ListF a w
           = μ w . 1 + a * w

∂ₐ(List a) = μ w . ∂ₐ(ListF a x)[x=μ x . ListF a x] +
                   ∂ₓ(ListF a x)[x=μ x . ListF a x] * w
           = μ w . List a + a * w

What do both branches of the recursive structure mean in each case? In the case of List a, 1 means that we are at the end of the list and a * w means that we have another element of the list, a, and the rest of the list w. In the case of ∂ₐ(List a), List a means that we are focused on the first element of the list and a * w means that we are descending further into the structure, passing an a as we go in; w represents descending in.

Not quite there yet

Note that when folding a data structure, we don’t really observe one a at a time, but rather one layer ListF a z at a time, with z representing the already folded part of the structure. This means that ∂ₐ(List a) = ∂ₐ(μ x . ListF a x) is not a good notion of location in a data structure.

We can improve the situation by using ListF a (z, lz : List a), where z is the result of folding lz (this is known as paramorphism). This tells us how what subtree z was produced from, but this doesn’t give us information about the path we took in the data structure to arrive to a particular layer ListF a z.

We can represent that path as a list of ∂ₓ(ListF a x)[x=List a] ~ a (we’ll use [] instead of List to indicate that it does not depend on the particular data structure we are considering): each element of the path is a particular choice of the direction we take as we descend down into the structure.

Generalizing to an arbitrary recursive data type, we get:

histCata :: Recursive t f => ([∂ₓ(f x)[x=t]] -> f (z, t) -> z) -> [∂ₓ(f x)[x=t]] -> t -> z
-- We pass [∂ₓ(f x)[x=t]] as an argument to histCata 
-- to represent the path we have taken before we started 
-- folding.

We have a slight problem, ∂ₓ(f x) can not be represented as a type constructor / type lambda, and furthermore we don’t have any operations consuming and producing values of type ∂ₓ(f x)[x=t] yet.

Derivative of ExprF

∂ₓ(ExprF x)
~ ∂ₓ(LitF Int | AddF x x | MulF x x)
~ ∂ₓ(Int + x * x + x * x)
~ 0 + (∂ₓ(x) * x + x * ∂ₓ(x)) + (∂ₓ(x) * x + x * ∂ₓ(x)) 
~ (x + x) + (x + x)
~ (AddL x | AddR x) | (MulL x | MulR x)

Let’s define it as a data type:

data ExprFD x = AddL x | AddR x | MulL x | MulR x

Now let’s look at the definition of project for expressions:

project :: Expr -> ExprF Expr
project (Lit i)   = LitF i
project (Add l r) = AddF l r 
project (Mul l r) = MulF l r

Notice that when we project, every Expr inside of ExprF Expr has a particular location in ExprF that could be represented by ∂ₓ(ExprF x):

projectD :: Expr -> ExprF (ExprFD Expr, Expr)
projectD (Lit i)   = LitF i
projectD (Add l r) = AddF (AddL r, l) (AddR l, r) 
projectD (Mul l r) = MulF (MulL r, l) (MulR l, r)

Note that projectD is not an isomorphism. And in the opposite direction there is a function of type (ExprFD Expr, Expr) -> Expr (also not an isomorphism):

embedD :: ExprFD Expr -> Expr -> Expr
embedD (AddL r) l = Add l r
embedD (AddR l) r = Add l r
embedD (MulL r) l = Mul l r
embedD (MulR l) r = Mul l r

Now we can express histCata for expressions as:

histCata :: ([ExprFD Expr] -> ExprF (z, Expr) -> z) -> [ExprFD Expr] -> List a -> z
histCata alg = go where
  go hist = alg hist . fmap (\(d, e) -> (go (d : hist) e, e)) . projectD

Generalizing

To generalize histCata, we’ll need to modify our typeclass by adding another type parameter for the derivative:

class Functor f => Recursive t f d | t -> f, t -> d where
  project :: t -> f t
  embed :: f t -> t
  -- and other methods

  projectD :: t -> f (d t, t)
  embedD :: (d t, t) -> t

  histCata :: ([d t] -> f (z, t) -> z) -> [d t] -> t -> z
  histCata alg = go where
    go hist = alg hist . fmap (\(d, e) -> (go (d : hist) e, e)) . projectD

Folding from the left

Consider the difference between foldl and foldr as seen through the lens of recursion schemes. Folding from the right is folding bottom-up, we start with leaves (non-recursive data constructors), fold those into z, then all data constructors above the leaves, etc. Folding from the left is folding top-down, we peel one layer of a data structure at a time and then proceed to the next layer until we reach the leaves. But this makes sense only if there is just a single direction to move! What if we have binary recursive data constructors like Add in Expr?

We can generalize foldl to arbitrary data structures in a few ways:

-- descend down all possible paths summing all values at the leaves
topDown1 :: Recursive t f d, Monoid z => z -> (z -> f () -> f z) -> z

-- preorder traversal
topDown2 :: Recursive t f d, Traversable f => z -> (z -> f () -> f z) -> (d z -> z) -> z

-- ??

References (that I have not read yet)

https://bartoszmilewski.com/2013/06/10/understanding-f-algebras/ http://comonad.com/reader/2009/recursion-schemes/ https://github.com/gallais/metamorphismsinagda https://en.wikipedia.org/wiki/F-coalgebra https://web.archive.org/web/20160304030154/http://www.cs.swan.ac.uk/csetzer/slides/lisbon2012/setzerLisbon2012InductionInductionInduction.pdf https://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/ http://www.cs.swan.ac.uk/csetzer/slides/dybjer60thBirthdayGothenburgJune2013/dybjer60thBirthdayGothenburgJune2013.pdf https://pchiusano.github.io/2014-08-12/zippers-not-useful.html https://stackoverflow.com/questions/5919901/data-structure-differentiation-intuition-building# http://www.randomhacks.net/2011/05/20/derivatives-of-algebraic-data-structures-an-excellent-tutorial/ http://okmij.org/ftp/continuations/zipper.html https://blog.sumtypeofway.com/an-introduction-to-recursion-schemes/ https://medium.com/@jaredtobin/practical-recursion-schemes-c10648ec1c29 https://blog.sumtypeofway.com/recursion-schemes-part-iv-time-is-of-the-essence/ https://www.reddit.com/r/haskell/comments/16qr6q/fixing_gadts_generic_recursion_schemes_for_gadts/ https://www.reddit.com/r/haskell/comments/3q0w7a/a_couple_of_quick_questions_about_recursionschemes/ http://blog.ezyang.com/2010/06/well-founded-recursion-in-agda/ https://hackage.haskell.org/package/recursion-schemes https://www.beyondthelines.net/programming/introduction-to-tagless-final/