Corecursion

In total programming languages, the natural numbers may be defined as follows (using Haskell syntax^[a]):

data Nat = Zero | Succ Nat

This states that every natural number is either zero or the successor of an existing natural number. For example, the number one is represented as Succ Zero, two as Succ (Succ Zero), three as Succ (Succ (Succ Zero)) and so on.

If we interpret the above declaration in an inductive way, then all natural numbers are generated like this, and we get our familiar set of natural numbers. Importantly, we can do recursion^[b] on this set: for example, we can use it to make a list that repeats a value n times:

repeat :: a -> Nat -> [x]
repeat x Zero = []                  -- Base case
repeat x (Succ n) = x : recursive n -- Inductive step

Note that the use of recursive n is crucial—we could not have written recursive (Succ n), because that is the function we are trying to define, and therefore it would loop forever. More specifically, the input must get smaller—or rather deeper, if seen as a data structure—each time we recurse.

The declaration may also be interpreted in a coinductive way, which may be denoted as:

codata CoNat = Zero | Succ CoNat

CoNat has all the natural numbers that Nat has automatically. But because codata can be infinitely deep, it has an extra term Succ (Succ (Succ (Succ …))) that continues on indefinitely—often denoted ∞.^[3] This is unique to the conatural numbers, so it can only be constructed using corecursion:

infinity :: CoNat
infinity = Succ infinity

While recursion requires that the input of the recursive call must get smaller each time, corecursion requires that the output of the recursive call must get larger each time. This is why we must write Succ infinity; just infinity = infinity would be disallowed as it loops forever.

To illustrate the duality between recursion and corecursion, we can encapsulate them in two functions, rec and corec. These functions' existence, together with the regular two constructors of Nat and CoNat, uniquely identify their respective types, and therefore allow rewriting all forms of recursion and corecursion in terms of them.^[4]

rec :: Nat -> (Maybe c -> c) -> c
rec Zero f = f Nothing
rec (Succ n) f = f (Just (rec n f))

corec :: (c -> Maybe c) -> c -> CoNat
corec f base =
  case f base of
    Nothing -> Zero
    Just x -> Succ (corec f x)

Conceptually, CoNat can be thought of as a state machine, where c is a type encapsulating the "current state". The function c -> Maybe c is a state transition function that either results in termination with Zero or continuation with Succ. We can rewrite the examples above using the functions:

repeat x n = rec n (\ s ->
  case s of
    Nothing -> []
    Just a -> x : a)
    
infinity = corec (\ () -> Just ()) ()

A more complex example of codata is that of binary trees, where each node is either a leaf node, holding some data, or is a branch node that has exactly two children:

codata BinaryTree a = Leaf a | Branch (BinaryTree a) (BinaryTree a)

This example has many more infinitely deep terms that can only be constructed by corecursion. For example, it can be infinitely deep only on the left-hand side, or on both sides, or alternating left and right:

infiniteLeft :: a -> BinaryTree a
infiniteLeft x = Branch (infiniteLeft x) (Leaf x)

infiniteBoth :: BinaryTree a
infiniteBoth = Branch infiniteBoth infiniteBoth

infiniteAlternating :: a -> Bool -> BinaryTree a
infiniteAlternating x False = Branch (infiniteAlternating x True) (Leaf x)
infiniteAlternating x True = Branch (Leaf x) (infiniteAlternating x False)

Again, corecursion on binary trees has a more general form based on a "state machine"-like constructor:

corec :: (c -> Either a (c, c)) -> c -> BinaryTree a
corec f base =
  case f base of
    Left x -> Leaf x
    Right (x, y) -> Branch (corec f x) (corec f y)

codata M a (b :: a -> *) = M
  { root :: a
  , branch :: b root -> M a b } 
  
corec :: (c -> (root :: a, b root -> c)) -> c -> M a b
corec f base =
  let (root, branch) = f base
  in M { root = root, branch = \ i -> corec f (branch i) }

f :: Bool -> *
f False = Void -- Zero case (no branches)
f True = ()    -- Succ case (one branch)

Nat = W Bool f
CoNat = M Bool f

The above section showed that there is an intimate link between natural and conatural numbers and Maybe c, and similarly between binary trees and Either a (c, c). This link is made precise by showing that Nat is in bijection with Maybe Nat, and CoNat with Maybe CoNat; explicitly, this bjiection associates Zero with Nothing and Succ n with Just n. In other words, Nat and CoNat are fixed points (up to isomorphism) of the map ${\displaystyle X\mapsto X+1}$.

The difference between data and codata is that data is the least such fixed point, while codata is the greatest. In this way, recursion can be summarized as the statement that "every element of the type was generated only by the given constructors (Zero and Succ in the case of Nat/CoNat)", while corecursion states that "every value that can be analysed using the constructors as cases exists".

From a category-theoretic perspective, CoNat can be precisely defined as the final coalgebra of the endofunctor${\displaystyle X\mapsto X+1}$.^[4] Unfolding this definition, we have that:

• There is a function pred :: CoNat -> Maybe CoNat. "Pred" stands for "predecessor", and the intuition is that it subtracts one from the conatural number or gives Nothing otherwise. In other words, pred Zero = Nothing and pred (Succ n) = Just n. This shows that CoNat is a coalgebra of the functor, but not necessarily the final one.
• For every type c and function f :: c -> Maybe c, there is a function corec f :: c -> CoNat such that pred (corec f x) = fmap (corec f) (f x).
  
  Breaking this down futher, if f x = Just y then corec f x = Succ (corec f y), while if f x = Nothing then corec f x = Zero—this matches the definition of corec we are familiar with.
• corec is unique in the following sense: for any other function g :: c -> CoNat that also satisfies pred (g x) = fmap g (f x), g x = corec f x. This ensures that CoNat is a final coalgebra.

Maybe c can be replaced with any other functor in the above description to obtain the definition of any other coinductive type.

Not all functors have final coalgebras. For example, Cantor's theorem tells us that no set can be in bijection with its powerset, and therefore the powerset functor a -> Bool has no final coalgebra. However, in the case of polynomial functors or quotient polynomial functors^[6], final coalgebras always exist; polynomial functors are functors that can be expressed in the form ${\displaystyle \textstyle X\mapsto \sum _{a:\alpha }X^{\beta (a)}}$ for a type α and α-indexed type family β(a). The M-type is exactly the construction of this final coalgebra.^[5]

While one can reason about coinductive data types using the uniqueness of corec directly, it is often more convenient to use coinduction, which can prove equalities of codata. Given a functor F and its final coalgebra A with map ${\displaystyle {\text{get}}:A\rightarrow F(A)}$, a bisimulation on A is a relation ${\displaystyle R\subseteq A\times A}$ such that there exists a function ${\displaystyle f:R\rightarrow F(R)}$ satisfying, for all ${\displaystyle (a,b)\in R}$,

• ${\displaystyle {\text{get}}(a)=F(\pi _{1})(f(a,b))}$ and
• ${\displaystyle {\text{get}}(b)=F(\pi _{2})(f(a,b))}$,

where π₁ and π₂ are the first and second projection maps ${\displaystyle R\rightarrow A}$. This can also be expressed as a commutative diagram:

Then, the principle of coinduction states that for all bisimulations R on A and ${\displaystyle (a,b)\in R}$, ${\displaystyle a=b}$.

Coinduction is easy to prove from the uniqueness of corec: π₁ and π₂ both satisfy the required property to be equal to corec f, and are therefore equal to each other, thus showing that ${\displaystyle a=\pi _{1}(a,b)=\pi _{2}(a,b)=b}$.^[4]

In the case where F is a polynomial functor—i.e. ${\displaystyle \textstyle F(X)=\sum _{a:\alpha }X^{\beta (a)}}$— there is an easier condition: R is a bisimulation if, for all ${\displaystyle (a,b)\in R}$, ${\displaystyle {\text{root}}(a)={\text{root}}(b)}$ and ${\displaystyle {\text{branch}}(a,i)R{\text{branch}}(b,i)}$ for all ${\displaystyle i:B({\text{root}}(a))}$. Here, ${\displaystyle {\text{root}}}$ and ${\displaystyle {\text{branch}}}$ refer to the maps:

${\displaystyle {\begin{aligned}{\text{root}}&:A\rightarrow \alpha \\{\text{branch}}&:\prod _{a:A}\beta ({\text{root}}(a))\rightarrow A\end{aligned}}}$

It can be seen this implies the general condition by setting ${\displaystyle f(a,b)=({\text{root}}(a),i\mapsto ({\text{branch}}(a,i),{\text{branch}}(b,i)))}$.

If the domain of discourse is the category of sets and total functions (such as in theorem provers like Agda and Rocq), then final types (codata) may contain infinite, non-wellfounded values, whereas initial types (data) do not.^[7][8] On the other hand, if the domain of discourse is the category of complete partial orders and continuous functions, which corresponds roughly to the Haskell programming language, then final types coincide with initial types, and the corresponding final coalgebra and initial algebra form an isomorphism.^[9]

Corecursion, referred to as circular programming, dates at least to (Bird 1984), who credits John Hughes and Philip Wadler; more general forms were developed in (Allison 1989). The original motivations included producing more efficient algorithms (allowing a single pass over data in some cases, instead of requiring multiple passes) and implementing classical data structures, such as doubly linked lists and queues, in functional languages.

• Bisimulation
• Coinduction
• Recursion
• Anamorphism