Corecursion · Lablypedia

Both corecursion and recursion can be thought of as operating on trees, which include data structures like lists and streams as special cases. Since recursion must terminate, it only works on trees that are well-founded, i.e. not infinitely deep, which are called data or initial data types; on the other hand, corecursion produces codata or final data types, which includes infinitely deep trees. Codata cannot be represented in memory directly, so is often implemented using self-referential data structures or lazy evaluation.

Data and codata

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

<span id="mwJQ"></span><span class="kr" id="mwJg">data</span><span class="w" id="mwJw"> </span><span class="kt" id="mwKA">Nat</span><span class="w" id="mwKQ"> </span><span class="ow" id="mwKg">=</span><span class="w" id="mwKw"> </span><span class="kt" id="mwLA">Zero</span><span class="w" id="mwLQ"> </span><span class="o" id="mwLg">|</span><span class="w" id="mwLw"> </span><span class="kt" id="mwMA">Succ</span><span class="w" id="mwMQ"> </span><span class="kt" id="mwMg">Nat</span>

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 on this set: for example, we can use it to make a list that repeats a value n times:

<span id="mwQA"></span><span class="nf" id="mwQQ">repeat</span><span class="w" id="mwQg"> </span><span class="ow" id="mwQw">::</span><span class="w" id="mwRA"> </span><span class="n" id="mwRQ">a</span><span class="w" id="mwRg"> </span><span class="ow" id="mwRw">-></span><span class="w" id="mwSA"> </span><span class="kt" id="mwSQ">Nat</span><span class="w" id="mwSg"> </span><span class="ow" id="mwSw">-></span><span class="w" id="mwTA"> </span><span class="p" id="mwTQ">[</span><span class="n" id="mwTg">a</span><span class="p" id="mwTw">]</span> <span class="nf" id="mwUA">repeat</span><span class="w" id="mwUQ"> </span><span class="n" id="mwUg">x</span><span class="w" id="mwUw"> </span><span class="kt" id="mwVA">Zero</span><span class="w" id="mwVQ"> </span><span class="ow" id="mwVg">=</span><span class="w" id="mwVw"> </span><span class="kt" id="mwWA">[]</span><span class="w" id="mwWQ"> </span><span class="c1" id="mwWg">-- Base case</span> <span class="nf" id="mwWw">repeat</span><span class="w" id="mwXA"> </span><span class="n" id="mwXQ">x</span><span class="w" id="mwXg"> </span><span class="p" id="mwXw">(</span><span class="kt" id="mwYA">Succ</span><span class="w" id="mwYQ"> </span><span class="n" id="mwYg">n</span><span class="p" id="mwYw">)</span><span class="w" id="mwZA"> </span><span class="ow" id="mwZQ">=</span><span class="w" id="mwZg"> </span><span class="n" id="mwZw">x</span><span class="w" id="mwaA"> </span><span class="kt" id="mwaQ">:</span><span class="w" id="mwag"> </span><span class="n" id="mwaw">repeat</span><span class="w" id="mwbA"> </span><span class="n" id="mwbQ">x</span><span class="w" id="mwbg"> </span><span class="n" id="mwbw">n</span><span class="w" id="mwcA"> </span><span class="c1" id="mwcQ">-- Inductive step</span>

Note that the use of repeat x n is crucial—we could not have written repeat x (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:

<span id="mweQ"></span><span class="nf" id="mweg">codata</span><span class="w" id="mwew"> </span><span class="kt" id="mwfA">CoNat</span><span class="w" id="mwfQ"> </span><span class="ow" id="mwfg">=</span><span class="w" id="mwfw"> </span><span class="kt" id="mwgA">Zero</span><span class="w" id="mwgQ"> </span><span class="o" id="mwgg">|</span><span class="w" id="mwgw"> </span><span class="kt" id="mwhA">Succ</span><span class="w" id="mwhQ"> </span><span class="kt" id="mwhg">CoNat</span>

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 ∞. This is unique to the conatural numbers, so it can only be constructed using corecursion:

<span id="mwkQ"></span><span class="nf" id="mwkg">infinity</span><span class="w" id="mwkw"> </span><span class="ow" id="mwlA">::</span><span class="w" id="mwlQ"> </span><span class="kt" id="mwlg">CoNat</span> <span class="nf" id="mwlw">infinity</span><span class="w" id="mwmA"> </span><span class="ow" id="mwmQ">=</span><span class="w" id="mwmg"> </span><span class="kt" id="mwmw">Succ</span><span class="w" id="mwnA"> </span><span class="n" id="mwnQ">infinity</span>

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.

<span id="mwrA"></span><span class="nf" id="mwrQ">rec</span><span class="w" id="mwrg"> </span><span class="ow" id="mwrw">::</span><span class="w" id="mwsA"> </span><span class="kt" id="mwsQ">Nat</span><span class="w" id="mwsg"> </span><span class="ow" id="mwsw">-></span><span class="w" id="mwtA"> </span><span class="p" id="mwtQ">(</span><span class="kt" id="mwtg">Maybe</span><span class="w" id="mwtw"> </span><span class="n" id="mwuA">c</span><span class="w" id="mwuQ"> </span><span class="ow" id="mwug">-></span><span class="w" id="mwuw"> </span><span class="n" id="mwvA">c</span><span class="p" id="mwvQ">)</span><span class="w" id="mwvg"> </span><span class="ow" id="mwvw">-></span><span class="w" id="mwwA"> </span><span class="n" id="mwwQ">c</span> <span class="nf" id="mwwg">rec</span><span class="w" id="mwww"> </span><span class="kt" id="mwxA">Zero</span><span class="w" id="mwxQ"> </span><span class="n" id="mwxg">f</span><span class="w" id="mwxw"> </span><span class="ow" id="mwyA">=</span><span class="w" id="mwyQ"> </span><span class="n" id="mwyg">f</span><span class="w" id="mwyw"> </span><span class="kt" id="mwzA">Nothing</span> <span class="nf" id="mwzQ">rec</span><span class="w" id="mwzg"> </span><span class="p" id="mwzw">(</span><span class="kt" id="mw0A">Succ</span><span class="w" id="mw0Q"> </span><span class="n" id="mw0g">n</span><span class="p" id="mw0w">)</span><span class="w" id="mw1A"> </span><span class="n" id="mw1Q">f</span><span class="w" id="mw1g"> </span><span class="ow" id="mw1w">=</span><span class="w" id="mw2A"> </span><span class="n" id="mw2Q">f</span><span class="w" id="mw2g"> </span><span class="p" id="mw2w">(</span><span class="kt" id="mw3A">Just</span><span class="w" id="mw3Q"> </span><span class="p" id="mw3g">(</span><span class="n" id="mw3w">rec</span><span class="w" id="mw4A"> </span><span class="n" id="mw4Q">n</span><span class="w" id="mw4g"> </span><span class="n" id="mw4w">f</span><span class="p" id="mw5A">))</span> <span class="nf" id="mw5Q">corec</span><span class="w" id="mw5g"> </span><span class="ow" id="mw5w">::</span><span class="w" id="mw6A"> </span><span class="p" id="mw6Q">(</span><span class="n" id="mw6g">c</span><span class="w" id="mw6w"> </span><span class="ow" id="mw7A">-></span><span class="w" id="mw7Q"> </span><span class="kt" id="mw7g">Maybe</span><span class="w" id="mw7w"> </span><span class="n" id="mw8A">c</span><span class="p" id="mw8Q">)</span><span class="w" id="mw8g"> </span><span class="ow" id="mw8w">-></span><span class="w" id="mw9A"> </span><span class="n" id="mw9Q">c</span><span class="w" id="mw9g"> </span><span class="ow" id="mw9w">-></span><span class="w" id="mw-A"> </span><span class="kt" id="mw-Q">CoNat</span> <span class="nf" id="mw-g">corec</span><span class="w" id="mw-w"> </span><span class="n" id="mw_A">f</span><span class="w" id="mw_Q"> </span><span class="n" id="mw_g">base</span><span class="w" id="mw_w"> </span><span class="ow" id="mwAQA">=</span> <span class="w" id="mwAQE"> </span><span class="kr" id="mwAQI">case</span><span class="w" id="mwAQM"> </span><span class="n" id="mwAQQ">f</span><span class="w" id="mwAQU"> </span><span class="n" id="mwAQY">base</span><span class="w" id="mwAQc"> </span><span class="kr" id="mwAQg">of</span> <span class="w" id="mwAQk"> </span><span class="kt" id="mwAQo">Nothing</span><span class="w" id="mwAQs"> </span><span class="ow" id="mwAQw">-></span><span class="w" id="mwAQ0"> </span><span class="kt" id="mwAQ4">Zero</span> <span class="w" id="mwAQ8"> </span><span class="kt" id="mwARA">Just</span><span class="w" id="mwARE"> </span><span class="n" id="mwARI">x</span><span class="w" id="mwARM"> </span><span class="ow" id="mwARQ">-></span><span class="w" id="mwARU"> </span><span class="kt" id="mwARY">Succ</span><span class="w" id="mwARc"> </span><span class="p" id="mwARg">(</span><span class="n" id="mwARk">corec</span><span class="w" id="mwARo"> </span><span class="n" id="mwARs">f</span><span class="w" id="mwARw"> </span><span class="n" id="mwAR0">x</span><span class="p" id="mwAR4">)</span>

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:

<span id="mwASg"></span><span class="nf" id="mwASk">repeat</span><span class="w" id="mwASo"> </span><span class="n" id="mwASs">x</span><span class="w" id="mwASw"> </span><span class="n" id="mwAS0">n</span><span class="w" id="mwAS4"> </span><span class="ow" id="mwAS8">=</span><span class="w" id="mwATA"> </span><span class="n" id="mwATE">rec</span><span class="w" id="mwATI"> </span><span class="n" id="mwATM">n</span><span class="w" id="mwATQ"> </span><span class="p" id="mwATU">(</span><span class="nf" id="mwATY">\</span><span class="w" id="mwATc"> </span><span class="n" id="mwATg">s</span><span class="w" id="mwATk"> </span><span class="ow" id="mwATo">-></span> <span class="w" id="mwATs"> </span><span class="kr" id="mwATw">case</span><span class="w" id="mwAT0"> </span><span class="n" id="mwAT4">s</span><span class="w" id="mwAT8"> </span><span class="kr" id="mwAUA">of</span> <span class="w" id="mwAUE"> </span><span class="kt" id="mwAUI">Nothing</span><span class="w" id="mwAUM"> </span><span class="ow" id="mwAUQ">-></span><span class="w" id="mwAUU"> </span><span class="kt" id="mwAUY">[]</span> <span class="w" id="mwAUc"> </span><span class="kt" id="mwAUg">Just</span><span class="w" id="mwAUk"> </span><span class="n" id="mwAUo">a</span><span class="w" id="mwAUs"> </span><span class="ow" id="mwAUw">-></span><span class="w" id="mwAU0"> </span><span class="n" id="mwAU4">x</span><span class="w" id="mwAU8"> </span><span class="kt" id="mwAVA">:</span><span class="w" id="mwAVE"> </span><span class="n" id="mwAVI">a</span><span class="p" id="mwAVM">)</span> <span class="w" id="mwAVQ"> </span> <span class="nf" id="mwAVU">infinity</span><span class="w" id="mwAVY"> </span><span class="ow" id="mwAVc">=</span><span class="w" id="mwAVg"> </span><span class="n" id="mwAVk">corec</span><span class="w" id="mwAVo"> </span><span class="p" id="mwAVs">(</span><span class="nf" id="mwAVw">\</span><span class="w" id="mwAV0"> </span><span class="nb" id="mwAV4">()</span><span class="w" id="mwAV8"> </span><span class="ow" id="mwAWA">-></span><span class="w" id="mwAWE"> </span><span class="kt" id="mwAWI">Just</span><span class="w" id="mwAWM"> </span><span class="nb" id="mwAWQ">()</span><span class="p" id="mwAWU">)</span><span class="w" id="mwAWY"> </span><span class="nb" id="mwAWc">()</span>

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:

<span id="mwAWw"></span><span class="nf" id="mwAW0">codata</span><span class="w" id="mwAW4"> </span><span class="kt" id="mwAW8">BinaryTree</span><span class="w" id="mwAXA"> </span><span class="n" id="mwAXE">a</span><span class="w" id="mwAXI"> </span><span class="ow" id="mwAXM">=</span><span class="w" id="mwAXQ"> </span><span class="kt" id="mwAXU">Leaf</span><span class="w" id="mwAXY"> </span><span class="n" id="mwAXc">a</span><span class="w" id="mwAXg"> </span><span class="o" id="mwAXk">|</span><span class="w" id="mwAXo"> </span><span class="kt" id="mwAXs">Branch</span><span class="w" id="mwAXw"> </span><span class="p" id="mwAX0">(</span><span class="kt" id="mwAX4">BinaryTree</span><span class="w" id="mwAX8"> </span><span class="n" id="mwAYA">a</span><span class="p" id="mwAYE">)</span><span class="w" id="mwAYI"> </span><span class="p" id="mwAYM">(</span><span class="kt" id="mwAYQ">BinaryTree</span><span class="w" id="mwAYU"> </span><span class="n" id="mwAYY">a</span><span class="p" id="mwAYc">)</span>

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:

<span id="mwAYs"></span><span class="nf" id="mwAYw">infiniteLeft</span><span class="w" id="mwAY0"> </span><span class="ow" id="mwAY4">::</span><span class="w" id="mwAY8"> </span><span class="n" id="mwAZA">a</span><span class="w" id="mwAZE"> </span><span class="ow" id="mwAZI">-></span><span class="w" id="mwAZM"> </span><span class="kt" id="mwAZQ">BinaryTree</span><span class="w" id="mwAZU"> </span><span class="n" id="mwAZY">a</span> <span class="nf" id="mwAZc">infiniteLeft</span><span class="w" id="mwAZg"> </span><span class="n" id="mwAZk">x</span><span class="w" id="mwAZo"> </span><span class="ow" id="mwAZs">=</span><span class="w" id="mwAZw"> </span><span class="kt" id="mwAZ0">Branch</span><span class="w" id="mwAZ4"> </span><span class="p" id="mwAZ8">(</span><span class="n" id="mwAaA">infiniteLeft</span><span class="w" id="mwAaE"> </span><span class="n" id="mwAaI">x</span><span class="p" id="mwAaM">)</span><span class="w" id="mwAaQ"> </span><span class="p" id="mwAaU">(</span><span class="kt" id="mwAaY">Leaf</span><span class="w" id="mwAac"> </span><span class="n" id="mwAag">x</span><span class="p" id="mwAak">)</span> <span class="nf" id="mwAao">infiniteBoth</span><span class="w" id="mwAas"> </span><span class="ow" id="mwAaw">::</span><span class="w" id="mwAa0"> </span><span class="kt" id="mwAa4">BinaryTree</span><span class="w" id="mwAa8"> </span><span class="n" id="mwAbA">a</span> <span class="nf" id="mwAbE">infiniteBoth</span><span class="w" id="mwAbI"> </span><span class="ow" id="mwAbM">=</span><span class="w" id="mwAbQ"> </span><span class="kt" id="mwAbU">Branch</span><span class="w" id="mwAbY"> </span><span class="n" id="mwAbc">infiniteBoth</span><span class="w" id="mwAbg"> </span><span class="n" id="mwAbk">infiniteBoth</span> <span class="nf" id="mwAbo">infiniteAlternating</span><span class="w" id="mwAbs"> </span><span class="ow" id="mwAbw">::</span><span class="w" id="mwAb0"> </span><span class="n" id="mwAb4">a</span><span class="w" id="mwAb8"> </span><span class="ow" id="mwAcA">-></span><span class="w" id="mwAcE"> </span><span class="kt" id="mwAcI">Bool</span><span class="w" id="mwAcM"> </span><span class="ow" id="mwAcQ">-></span><span class="w" id="mwAcU"> </span><span class="kt" id="mwAcY">BinaryTree</span><span class="w" id="mwAcc"> </span><span class="n" id="mwAcg">a</span> <span class="nf" id="mwAck">infiniteAlternating</span><span class="w" id="mwAco"> </span><span class="n" id="mwAcs">x</span><span class="w" id="mwAcw"> </span><span class="kt" id="mwAc0">False</span><span class="w" id="mwAc4"> </span><span class="ow" id="mwAc8">=</span><span class="w" id="mwAdA"> </span><span class="kt" id="mwAdE">Branch</span><span class="w" id="mwAdI"> </span><span class="p" id="mwAdM">(</span><span class="n" id="mwAdQ">infiniteAlternating</span><span class="w" id="mwAdU"> </span><span class="n" id="mwAdY">x</span><span class="w" id="mwAdc"> </span><span class="kt" id="mwAdg">True</span><span class="p" id="mwAdk">)</span><span class="w" id="mwAdo"> </span><span class="p" id="mwAds">(</span><span class="kt" id="mwAdw">Leaf</span><span class="w" id="mwAd0"> </span><span class="n" id="mwAd4">x</span><span class="p" id="mwAd8">)</span> <span class="nf" id="mwAeA">infiniteAlternating</span><span class="w" id="mwAeE"> </span><span class="n" id="mwAeI">x</span><span class="w" id="mwAeM"> </span><span class="kt" id="mwAeQ">True</span><span class="w" id="mwAeU"> </span><span class="ow" id="mwAeY">=</span><span class="w" id="mwAec"> </span><span class="kt" id="mwAeg">Branch</span><span class="w" id="mwAek"> </span><span class="p" id="mwAeo">(</span><span class="kt" id="mwAes">Leaf</span><span class="w" id="mwAew"> </span><span class="n" id="mwAe0">x</span><span class="p" id="mwAe4">)</span><span class="w" id="mwAe8"> </span><span class="p" id="mwAfA">(</span><span class="n" id="mwAfE">infiniteAlternating</span><span class="w" id="mwAfI"> </span><span class="n" id="mwAfM">x</span><span class="w" id="mwAfQ"> </span><span class="kt" id="mwAfU">False</span><span class="p" id="mwAfY">)</span>

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

<span id="mwAfo"></span><span class="nf" id="mwAfs">corec</span><span class="w" id="mwAfw"> </span><span class="ow" id="mwAf0">::</span><span class="w" id="mwAf4"> </span><span class="p" id="mwAf8">(</span><span class="n" id="mwAgA">c</span><span class="w" id="mwAgE"> </span><span class="ow" id="mwAgI">-></span><span class="w" id="mwAgM"> </span><span class="kt" id="mwAgQ">Either</span><span class="w" id="mwAgU"> </span><span class="n" id="mwAgY">a</span><span class="w" id="mwAgc"> </span><span class="p" id="mwAgg">(</span><span class="n" id="mwAgk">c</span><span class="p" id="mwAgo">,</span><span class="w" id="mwAgs"> </span><span class="n" id="mwAgw">c</span><span class="p" id="mwAg0">))</span><span class="w" id="mwAg4"> </span><span class="ow" id="mwAg8">-></span><span class="w" id="mwAhA"> </span><span class="n" id="mwAhE">c</span><span class="w" id="mwAhI"> </span><span class="ow" id="mwAhM">-></span><span class="w" id="mwAhQ"> </span><span class="kt" id="mwAhU">BinaryTree</span><span class="w" id="mwAhY"> </span><span class="n" id="mwAhc">a</span> <span class="nf" id="mwAhg">corec</span><span class="w" id="mwAhk"> </span><span class="n" id="mwAho">f</span><span class="w" id="mwAhs"> </span><span class="n" id="mwAhw">base</span><span class="w" id="mwAh0"> </span><span class="ow" id="mwAh4">=</span> <span class="w" id="mwAh8"> </span><span class="kr" id="mwAiA">case</span><span class="w" id="mwAiE"> </span><span class="n" id="mwAiI">f</span><span class="w" id="mwAiM"> </span><span class="n" id="mwAiQ">base</span><span class="w" id="mwAiU"> </span><span class="kr" id="mwAiY">of</span> <span class="w" id="mwAic"> </span><span class="kt" id="mwAig">Left</span><span class="w" id="mwAik"> </span><span class="n" id="mwAio">x</span><span class="w" id="mwAis"> </span><span class="ow" id="mwAiw">-></span><span class="w" id="mwAi0"> </span><span class="kt" id="mwAi4">Leaf</span><span class="w" id="mwAi8"> </span><span class="n" id="mwAjA">x</span> <span class="w" id="mwAjE"> </span><span class="kt" id="mwAjI">Right</span><span class="w" id="mwAjM"> </span><span class="p" id="mwAjQ">(</span><span class="n" id="mwAjU">x</span><span class="p" id="mwAjY">,</span><span class="w" id="mwAjc"> </span><span class="n" id="mwAjg">y</span><span class="p" id="mwAjk">)</span><span class="w" id="mwAjo"> </span><span class="ow" id="mwAjs">-></span><span class="w" id="mwAjw"> </span><span class="kt" id="mwAj0">Branch</span><span class="w" id="mwAj4"> </span><span class="p" id="mwAj8">(</span><span class="n" id="mwAkA">corec</span><span class="w" id="mwAkE"> </span><span class="n" id="mwAkI">f</span><span class="w" id="mwAkM"> </span><span class="n" id="mwAkQ">x</span><span class="p" id="mwAkU">)</span><span class="w" id="mwAkY"> </span><span class="p" id="mwAkc">(</span><span class="n" id="mwAkg">corec</span><span class="w" id="mwAkk"> </span><span class="n" id="mwAko">f</span><span class="w" id="mwAks"> </span><span class="n" id="mwAkw">y</span><span class="p" id="mwAk0">)</span>

M-types

In a dependently-typed setting, codata can be encoded using M-types, which are dual to W-types. Given a type A and an A-indexed family of types B, one can form the M-type $M_{a : A} B (a)$ , representing the type of trees whose nodes are labelled with elements of A and who child nodes are indexed by the set B(a). In pseudocode, M-types (and their corecursion principle) may be defined as:

<span id="mwAl0"></span><span class="nf" id="mwAl4">codata</span><span class="w" id="mwAl8"> </span><span class="kt" id="mwAmA">M</span><span class="w" id="mwAmE"> </span><span class="n" id="mwAmI">a</span><span class="w" id="mwAmM"> </span><span class="p" id="mwAmQ">(</span><span class="n" id="mwAmU">b</span><span class="w" id="mwAmY"> </span><span class="ow" id="mwAmc">::</span><span class="w" id="mwAmg"> </span><span class="n" id="mwAmk">a</span><span class="w" id="mwAmo"> </span><span class="ow" id="mwAms">-></span><span class="w" id="mwAmw"> </span><span class="o" id="mwAm0">*</span><span class="p" id="mwAm4">)</span><span class="w" id="mwAm8"> </span><span class="ow" id="mwAnA">=</span><span class="w" id="mwAnE"> </span><span class="kt" id="mwAnI">M</span> <span class="w" id="mwAnM"> </span><span class="p" id="mwAnQ">{</span><span class="w" id="mwAnU"> </span><span class="n" id="mwAnY">root</span><span class="w" id="mwAnc"> </span><span class="ow" id="mwAng">::</span><span class="w" id="mwAnk"> </span><span class="n" id="mwAno">a</span> <span class="w" id="mwAns"> </span><span class="p" id="mwAnw">,</span><span class="w" id="mwAn0"> </span><span class="n" id="mwAn4">branch</span><span class="w" id="mwAn8"> </span><span class="ow" id="mwAoA">::</span><span class="w" id="mwAoE"> </span><span class="n" id="mwAoI">b</span><span class="w" id="mwAoM"> </span><span class="n" id="mwAoQ">root</span><span class="w" id="mwAoU"> </span><span class="ow" id="mwAoY">-></span><span class="w" id="mwAoc"> </span><span class="kt" id="mwAog">M</span><span class="w" id="mwAok"> </span><span class="n" id="mwAoo">a</span><span class="w" id="mwAos"> </span><span class="n" id="mwAow">b</span><span class="w" id="mwAo0"> </span><span class="p" id="mwAo4">}</span><span class="w" id="mwAo8"> </span> <span class="w" id="mwApA"> </span> <span class="nf" id="mwApE">corec</span><span class="w" id="mwApI"> </span><span class="ow" id="mwApM">::</span><span class="w" id="mwApQ"> </span><span class="p" id="mwApU">(</span><span class="n" id="mwApY">c</span><span class="w" id="mwApc"> </span><span class="ow" id="mwApg">-></span><span class="w" id="mwApk"> </span><span class="p" id="mwApo">(</span><span class="n" id="mwAps">root</span><span class="w" id="mwApw"> </span><span class="ow" id="mwAp0">::</span><span class="w" id="mwAp4"> </span><span class="n" id="mwAp8">a</span><span class="p" id="mwAqA">,</span><span class="w" id="mwAqE"> </span><span class="n" id="mwAqI">b</span><span class="w" id="mwAqM"> </span><span class="n" id="mwAqQ">root</span><span class="w" id="mwAqU"> </span><span class="ow" id="mwAqY">-></span><span class="w" id="mwAqc"> </span><span class="n" id="mwAqg">c</span><span class="p" id="mwAqk">))</span><span class="w" id="mwAqo"> </span><span class="ow" id="mwAqs">-></span><span class="w" id="mwAqw"> </span><span class="n" id="mwAq0">c</span><span class="w" id="mwAq4"> </span><span class="ow" id="mwAq8">-></span><span class="w" id="mwArA"> </span><span class="kt" id="mwArE">M</span><span class="w" id="mwArI"> </span><span class="n" id="mwArM">a</span><span class="w" id="mwArQ"> </span><span class="n" id="mwArU">b</span> <span class="nf" id="mwArY">corec</span><span class="w" id="mwArc"> </span><span class="n" id="mwArg">f</span><span class="w" id="mwArk"> </span><span class="n" id="mwAro">base</span><span class="w" id="mwArs"> </span><span class="ow" id="mwArw">=</span> <span class="w" id="mwAr0"> </span><span class="kr" id="mwAr4">let</span><span class="w" id="mwAr8"> </span><span class="p" id="mwAsA">(</span><span class="n" id="mwAsE">root</span><span class="p" id="mwAsI">,</span><span class="w" id="mwAsM"> </span><span class="n" id="mwAsQ">branch</span><span class="p" id="mwAsU">)</span><span class="w" id="mwAsY"> </span><span class="ow" id="mwAsc">=</span><span class="w" id="mwAsg"> </span><span class="n" id="mwAsk">f</span><span class="w" id="mwAso"> </span><span class="n" id="mwAss">base</span> <span class="w" id="mwAsw"> </span><span class="kr" id="mwAs0">in</span><span class="w" id="mwAs4"> </span><span class="kt" id="mwAs8">M</span><span class="w" id="mwAtA"> </span><span class="p" id="mwAtE">{</span><span class="w" id="mwAtI"> </span><span class="n" id="mwAtM">root</span><span class="w" id="mwAtQ"> </span><span class="ow" id="mwAtU">=</span><span class="w" id="mwAtY"> </span><span class="n" id="mwAtc">root</span><span class="p" id="mwAtg">,</span><span class="w" id="mwAtk"> </span><span class="n" id="mwAto">branch</span><span class="w" id="mwAts"> </span><span class="ow" id="mwAtw">=</span><span class="w" id="mwAt0"> </span><span class="nf" id="mwAt4">\</span><span class="w" id="mwAt8"> </span><span class="n" id="mwAuA">i</span><span class="w" id="mwAuE"> </span><span class="ow" id="mwAuI">-></span><span class="w" id="mwAuM"> </span><span class="n" id="mwAuQ">corec</span><span class="w" id="mwAuU"> </span><span class="n" id="mwAuY">f</span><span class="w" id="mwAuc"> </span><span class="p" id="mwAug">(</span><span class="n" id="mwAuk">branch</span><span class="w" id="mwAuo"> </span><span class="n" id="mwAus">i</span><span class="p" id="mwAuw">)</span><span class="w" id="mwAu0"> </span><span class="p" id="mwAu4">}</span>

As an example, the natural and conatural numbers may be constructed as W- and M-types of the same function:

<span id="mwAvI"></span><span class="nf" id="mwAvM">f</span><span class="w" id="mwAvQ"> </span><span class="ow" id="mwAvU">::</span><span class="w" id="mwAvY"> </span><span class="kt" id="mwAvc">Bool</span><span class="w" id="mwAvg"> </span><span class="ow" id="mwAvk">-></span><span class="w" id="mwAvo"> </span><span class="o" id="mwAvs">*</span> <span class="nf" id="mwAvw">f</span><span class="w" id="mwAv0"> </span><span class="kt" id="mwAv4">False</span><span class="w" id="mwAv8"> </span><span class="ow" id="mwAwA">=</span><span class="w" id="mwAwE"> </span><span class="kt" id="mwAwI">Void</span><span class="w" id="mwAwM"> </span><span class="c1" id="mwAwQ">-- Zero case (no branches)</span> <span class="nf" id="mwAwU">f</span><span class="w" id="mwAwY"> </span><span class="kt" id="mwAwc">True</span><span class="w" id="mwAwg"> </span><span class="ow" id="mwAwk">=</span><span class="w" id="mwAwo"> </span><span class="nb" id="mwAws">()</span><span class="w" id="mwAww"> </span><span class="c1" id="mwAw0">-- Succ case (one branch)</span> <span class="kt" id="mwAw4">Nat</span><span class="w" id="mwAw8"> </span><span class="ow" id="mwAxA">=</span><span class="w" id="mwAxE"> </span><span class="kt" id="mwAxI">W</span><span class="w" id="mwAxM"> </span><span class="kt" id="mwAxQ">Bool</span><span class="w" id="mwAxU"> </span><span class="n" id="mwAxY">f</span> <span class="kt" id="mwAxc">CoNat</span><span class="w" id="mwAxg"> </span><span class="ow" id="mwAxk">=</span><span class="w" id="mwAxo"> </span><span class="kt" id="mwAxs">M</span><span class="w" id="mwAxw"> </span><span class="kt" id="mwAx0">Bool</span><span class="w" id="mwAx4"> </span><span class="n" id="mwAx8">f</span>

M-types can be proven to exist in many elementary topoi, and their existence follows from the existence of W-types.

4 more chapters are free with a Lably account.

Mathematical description

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 bijection 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 $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 $X \mapsto X + 1$ . 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 further, 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, final coalgebras always exist; polynomial functors are functors that can be expressed in the form $X \mapsto \sum_{a : α} X^{β (a)}$ for a type α and α-indexed type family β(a). The M-type is exactly the construction of this final coalgebra.

Coinduction

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 final coalgebra A of a polynomial functor F—i.e. $F (X) = \sum_{a : α} X^{β (a)}$ — we say that a relation $R \subseteq A \times A$ is a bisimulation if, for all $(a, b) \in R$ , $root (a) = root (b)$ and $branch (a, i) R branch (b, i)$ for all $i : B (root (a))$ . Here, $root$ and $branch$ refer to the maps:

$\begin{matrix} root & : A \to α \\ branch & : \prod_{a : A} β (root (a)) \to A \end{matrix}$

The principle of coinduction states that for all bisimulations R on A and $(a, b) \in R$ , $a = b$ .

More generally, for a coalgebra map $get : A \to F (A)$ , a relation R on A is a bisimulation if there exists a function $f : R \to F (R)$ satisfying, for all $(a, b) \in R$ ,

$get (a) = F (π_{1}) (f (a, b))$ and
$get (b) = F (π_{2}) (f (a, b))$ ,

where π₁ and π₂ are the first and second projection maps $R \to A$ . It can be seen this equivalent to the polynomial case by setting $f (a, b) = (root (a), i \mapsto (branch (a, i), branch (b, i)))$ . The required equalities can also be expressed as a commutative diagram:

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 $a = π_{1} (a, b) = π_{2} (a, b) = b$ .

Example: Conatural number addition

To demonstrate the usage of coinduction, we will prove some basic properties about addition on conatural numbers. Addition can be defined identically to how it is defined for natural numbers:

<span id="mwA7g"></span><span class="nf" id="mwA7k">add</span><span class="w" id="mwA7o"> </span><span class="ow" id="mwA7s">::</span><span class="w" id="mwA7w"> </span><span class="kt" id="mwA70">CoNat</span><span class="w" id="mwA74"> </span><span class="ow" id="mwA78">-></span><span class="w" id="mwA8A"> </span><span class="kt" id="mwA8E">CoNat</span><span class="w" id="mwA8I"> </span><span class="ow" id="mwA8M">-></span><span class="w" id="mwA8Q"> </span><span class="kt" id="mwA8U">CoNat</span> <span class="nf" id="mwA8Y">add</span><span class="w" id="mwA8c"> </span><span class="n" id="mwA8g">a</span><span class="w" id="mwA8k"> </span><span class="kt" id="mwA8o">Zero</span><span class="w" id="mwA8s"> </span><span class="ow" id="mwA8w">=</span><span class="w" id="mwA80"> </span><span class="n" id="mwA84">a</span> <span class="nf" id="mwA88">add</span><span class="w" id="mwA9A"> </span><span class="n" id="mwA9E">a</span><span class="w" id="mwA9I"> </span><span class="p" id="mwA9M">(</span><span class="kt" id="mwA9Q">Succ</span><span class="w" id="mwA9U"> </span><span class="n" id="mwA9Y">b</span><span class="p" id="mwA9c">)</span><span class="w" id="mwA9g"> </span><span class="ow" id="mwA9k">=</span><span class="w" id="mwA9o"> </span><span class="kt" id="mwA9s">Succ</span><span class="w" id="mwA9w"> </span><span class="p" id="mwA90">(</span><span class="n" id="mwA94">add</span><span class="w" id="mwA98"> </span><span class="n" id="mwA-A">a</span><span class="w" id="mwA-E"> </span><span class="n" id="mwA-I">b</span><span class="p" id="mwA-M">)</span>

This definition, while valid, hides some amount of complexity. We may alternatively write:

<span id="mwA-c"></span><span class="nf" id="mwA-g">add</span><span class="w" id="mwA-k"> </span><span class="kt" id="mwA-o">Zero</span><span class="w" id="mwA-s"> </span><span class="kt" id="mwA-w">Zero</span><span class="w" id="mwA-0"> </span><span class="ow" id="mwA-4">=</span><span class="w" id="mwA-8"> </span><span class="kt" id="mwA_A">Zero</span> <span class="nf" id="mwA_E">add</span><span class="w" id="mwA_I"> </span><span class="p" id="mwA_M">(</span><span class="kt" id="mwA_Q">Succ</span><span class="w" id="mwA_U"> </span><span class="n" id="mwA_Y">a</span><span class="p" id="mwA_c">)</span><span class="w" id="mwA_g"> </span><span class="kt" id="mwA_k">Zero</span><span class="w" id="mwA_o"> </span><span class="ow" id="mwA_s">=</span><span class="w" id="mwA_w"> </span><span class="kt" id="mwA_0">Succ</span><span class="w" id="mwA_4"> </span><span class="p" id="mwA_8">(</span><span class="n" id="mwBAA">add</span><span class="w" id="mwBAE"> </span><span class="n" id="mwBAI">a</span><span class="w" id="mwBAM"> </span><span class="kt" id="mwBAQ">Zero</span><span class="p" id="mwBAU">)</span> <span class="nf" id="mwBAY">add</span><span class="w" id="mwBAc"> </span><span class="n" id="mwBAg">a</span><span class="w" id="mwBAk"> </span><span class="p" id="mwBAo">(</span><span class="kt" id="mwBAs">Succ</span><span class="w" id="mwBAw"> </span><span class="n" id="mwBA0">b</span><span class="p" id="mwBA4">)</span><span class="w" id="mwBA8"> </span><span class="ow" id="mwBBA">=</span><span class="w" id="mwBBE"> </span><span class="kt" id="mwBBI">Succ</span><span class="w" id="mwBBM"> </span><span class="p" id="mwBBQ">(</span><span class="n" id="mwBBU">add</span><span class="w" id="mwBBY"> </span><span class="n" id="mwBBc">a</span><span class="w" id="mwBBg"> </span><span class="n" id="mwBBk">b</span><span class="p" id="mwBBo">)</span>

This definition makes the translation to corec straightforward:

<span id="mwBB8"></span><span class="nf" id="mwBCA">iterate</span><span class="w" id="mwBCE"> </span><span class="ow" id="mwBCI">::</span><span class="w" id="mwBCM"> </span><span class="p" id="mwBCQ">(</span><span class="kt" id="mwBCU">CoNat</span><span class="p" id="mwBCY">,</span><span class="w" id="mwBCc"> </span><span class="kt" id="mwBCg">CoNat</span><span class="p" id="mwBCk">)</span><span class="w" id="mwBCo"> </span><span class="ow" id="mwBCs">-></span><span class="w" id="mwBCw"> </span><span class="kt" id="mwBC0">Maybe</span><span class="w" id="mwBC4"> </span><span class="p" id="mwBC8">(</span><span class="kt" id="mwBDA">CoNat</span><span class="p" id="mwBDE">,</span><span class="w" id="mwBDI"> </span><span class="kt" id="mwBDM">CoNat</span><span class="p" id="mwBDQ">)</span> <span class="nf" id="mwBDU">iterate</span><span class="w" id="mwBDY"> </span><span class="kt" id="mwBDc">Zero</span><span class="w" id="mwBDg"> </span><span class="kt" id="mwBDk">Zero</span><span class="w" id="mwBDo"> </span><span class="ow" id="mwBDs">=</span><span class="w" id="mwBDw"> </span><span class="kt" id="mwBD0">Nothing</span> <span class="nf" id="mwBD4">iterate</span><span class="w" id="mwBD8"> </span><span class="p" id="mwBEA">(</span><span class="kt" id="mwBEE">Succ</span><span class="w" id="mwBEI"> </span><span class="n" id="mwBEM">a</span><span class="p" id="mwBEQ">)</span><span class="w" id="mwBEU"> </span><span class="kt" id="mwBEY">Zero</span><span class="w" id="mwBEc"> </span><span class="ow" id="mwBEg">=</span><span class="w" id="mwBEk"> </span><span class="kt" id="mwBEo">Just</span><span class="w" id="mwBEs"> </span><span class="p" id="mwBEw">(</span><span class="n" id="mwBE0">a</span><span class="p" id="mwBE4">,</span><span class="w" id="mwBE8"> </span><span class="kt" id="mwBFA">Zero</span><span class="p" id="mwBFE">)</span> <span class="nf" id="mwBFI">iterate</span><span class="w" id="mwBFM"> </span><span class="n" id="mwBFQ">a</span><span class="w" id="mwBFU"> </span><span class="p" id="mwBFY">(</span><span class="kt" id="mwBFc">Succ</span><span class="w" id="mwBFg"> </span><span class="n" id="mwBFk">b</span><span class="p" id="mwBFo">)</span><span class="w" id="mwBFs"> </span><span class="ow" id="mwBFw">=</span><span class="w" id="mwBF0"> </span><span class="kt" id="mwBF4">Just</span><span class="w" id="mwBF8"> </span><span class="p" id="mwBGA">(</span><span class="n" id="mwBGE">a</span><span class="p" id="mwBGI">,</span><span class="w" id="mwBGM"> </span><span class="n" id="mwBGQ">b</span><span class="p" id="mwBGU">)</span> <span class="nf" id="mwBGY">add</span><span class="w" id="mwBGc"> </span><span class="n" id="mwBGg">a</span><span class="w" id="mwBGk"> </span><span class="n" id="mwBGo">b</span><span class="w" id="mwBGs"> </span><span class="ow" id="mwBGw">=</span><span class="w" id="mwBG0"> </span><span class="n" id="mwBG4">corec</span><span class="w" id="mwBG8"> </span><span class="n" id="mwBHA">iterate</span><span class="w" id="mwBHE"> </span><span class="p" id="mwBHI">(</span><span class="n" id="mwBHM">a</span><span class="p" id="mwBHQ">,</span><span class="w" id="mwBHU"> </span><span class="n" id="mwBHY">b</span><span class="p" id="mwBHc">)</span>

We can prove that $a + 0 = a$ by coinduction on the relation ${(a + 0, a) | a \in N^{\infty}}$ (where $N^{\infty}$ is the set of conatural numbers). First, it follows from the definition of addition that $a + 0 = 0 ⟺ a = 0$ ; second, if we assume that $(x + 1, y + 1)$ is of the form $(a + 0, a)$ for some a, we must show that $(x, y)$ is also of this form. We have: $x + 1 = a + 0 = (y + 1) + 0 = (y + 0) + 1$ Thus $x = y + 0$ , and therefore $(x, y) = (y + 0, y)$ as required.

The identity $(a + 1) + b = (a + b) + 1$ may be similarly proven by coinduction on ${(((a + 1) + b) - 1, a + b) | a, b \in N^{\infty}}$ (remember the relation must necessarily include $(0, 0)$ ); finally, commutativity— $a + b = b + a$ —results from similar straightforward coinduction on ${(a + b, b + a) | a, b \in N^{\infty}}$ .

In programming languages

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. 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.

History

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.