Coinduction and corecursion for dummies

Factual Questions
1

I’m trying to make some sense out of this stuff, but it’s a little tricky (to say the least), and all the categorical details are not helping.

Let’s consider a simple data type, which is just a list of integers. In Haskell, the declaration should look something like this:


data IntList = Empty | Concatenation Int IntList

It’s easy to see what the general structure of a recursive function or an inductive proof involving this type is: handle the case where the object Empty, and then recursively/inductively handle the case where the object is a Concatenation. But of course, intuitive reasoning isn’t enough to get all the details, and that seems to be what’s important.

So, here are the questions that I think are relevant:
[ol]
[li]What’s the initial algebra corresponding to the type IntList?[/li][li]How does that translate into induction and recursion principles?[/li][li]What’s the corresponding final coalgebra?[/li][li]What are the coinduction and corecursion principles, and how do they come from the coalgebra?[/li][/ol]
If that’s not interesting enough, let’s consider a similar tree type:


data IntTree = Empty | NonEmpty Int IntTree IntTree
2

(Alas, I only have time to scribble out a rather hasty response right now, which I fear may not be too tutorially helpful. Feel free to ask more questions, though, and I’ll hopefully be able to respond better in a more relaxed future. [If indeed relaxation is possible to attain…])

The initial algebra and final coalgebra depend on the category you are working in, but let’s start by just thinking of the case where the category is normal sets and normal functions up to normal function equality, whatever all that amounts to.

  1. The initial algebra is finite lists of integers (let’s call this type FinList), with Empty being the empty list of integers, and Concatenation being the map which, given an integer and a finite list of integers, returns the result of prepending its first argument to its second argument. (Actually, it will be helpful, particularly once we start reversing arrows, to think of this not as two separate constructors, but a single invertible constructor from 1 + Int * FinList -> FinList.).

  2. The recursion principle is captured in the initiality: Initiality says that, for any type X, given an element Empty’ of X and a function Concatenation’ : Int * X -> X, there is a unique function f : FinList -> X such that f(Empty) = Empty’ and f(Concatenation(n, l)) = Concatenation’(n, f(l)) for every integer n and finite list of integers l. In other words, you can uniquely define functions on finite lists of integers by recursion (specifying the function’s value on the empty list as the base case, and specifying the function’s value on non-empty lists in terms of the list’s first element and (recursively) the function’s value on the list’s tail).

Induction is a special case of recursion, as follows: Let X be a subset of the finite lists of integers (i.e., the subset satisfying some property of interest), and let Empty’ actually be Empty (so this subset contains the empty list) and let Concatenation’(n, x) actually be Concatenation(n, x) for every integer n and element x of X (so this subset is also closed under prepending of an integer). By recursive definition as above, we obtain a function f : FinList -> X. COmposing first f and then the inclusion from X back into FinList gives us a function from finite lists of integers to finite lists of integers which takes Empty to Empty and takes Concatenation to Concatenation, so to speak. Thus, it must be equal to the identity function (because they both satisfy the same recursive definition, and solutions to recursive definitions are unique). This means the composition’s range includes all of FinList, and thus the inclusion of X into FinList must be surjective, and thus X must contain all of FinList.

  1. The final coalgebra is finite or countably infinite lists of integers (let’s call this Stream), with Empty and Concatenation again being the obvious functions, combining into an invertible function of type 1 + Int * Stream -> Stream. Since we’re talking about coalgebras, though, its the inverse of this map that’s really of importance. Let us call that Unwrap : Stream -> 1 + Int * Stream. Given a stream, this “destructor” determines whether it’s empty or not; if it’s empty, a tag is returned saying “Yeah, it’s empty”. Otherwise, a tag is returned saying “No, it’s non-empty; here’s the head and tail”.

  2. The corecursion principle says that, for any type X, given a function Unwrap’ : X -> 1 + Int * X, there is a unique function g : X -> Stream such that… Well, such that certain equations hold, but perhaps you’ve already seen those and would rather have it explained in words. Imagine applying Unwrap’ to an element of X. You can either end up in the “1” branch, which is like “Stop, there’s nothing left”. Or you can end up in the “Int * X” branch, which is like “Ok, here’s my first integer, and here’s the guy to keep Unwrap’ing if you want more”. So if you keep Unwrap’ing over and over, you’ll generate a stream of integers, which maybe stops at some point or maybe keeps going forever. SO what g does is send an element of X to the corresponding Stream it generates.

Now, for coinduction. It will not have anything to do with subsets of Stream. Rather, we’ll be dealing with the dual notion to subsets: quotients. Consider the case where X is Stream modulo some equivalence relation on Streams (so instead of there being an injective inclusion from X into Stream, there’s a surjective function “modding out” function from Stream onto X). And suppose this equivalence relation respects Unwrapping, in that if Streams x and y are equivalent, then they’re either both empty, or they have the same first element and furthermore have equivalent tails. Then, by the dual of the induction-establishing argument above, we can use the uniqueness of corecursion to establish that this quotienting must be trivial; i.e., the equivalence relation must be the actual equality on Stream.

So induction gives us a way of showing that some property holds at every element of a type, while coinduction gives us a way of showing that some equivalence relation holds at precisely the equal elements of a type.

3

I think I mostly follow that, but what does the notation 1 + Int * FinList -> FinList mean?

4

In Haskell notation, it would be Either () (Int, FinList) -> FinList. [Equivalently, Maybe (Int, FinList) -> FinList]

By “1”, I mean the 0-ary tuple type, the type with just one element. In Haskell notation (ignoring issues of “boxing”), the type denoted ().

By a + b, I mean the disjoint union of a and b. In Haskell notation (again ignoring some details), Either a b.

Does that clear things up?

5

Whoops, and I also forgot to say, by a * b I mean the Cartesian product of a and b (i.e., the type of ordered pairs of the two). In Haskell notation, (a, b).

6

Basically, the single invertible constructor I was referring to is this:



makeList :: Either () (Int, IntList) -> IntList
makeList (Left _) = Empty
makeList (Right (a, b)) = Concatenation a b
7

I think I mostly get the answers to questions 1 and 2, but there are a couple details:

I’m not clear on what it means to compose a function and a set inclusion. Is there some way that you can view the latter as a function, or is it just a matter of saying something like “Every element of X is an element of FinList”?

And just to be clear, are there closure requirements for an initial algebra? I’m used to the word “algebra” as in universal algebra, and I think that’s different enough that it’s confusing. It seems like there should be some notion of the things that can be constructed by finitely many applications of the constructor associated with FinList, but I don’t think that’s the initial algebra.

(I know that’s a pretty basic question, but I barely know any category theory, and Wikipedia’s articles on these things are not accessible with that background.)

8

You can view an inclusion as a function like so: if A is a subset of B, then there is an injective function from A to B given by ((x :: A) -> x :: B). That’s what I mean by an “inclusion”, this injective function from the subset into the superset that just sends things to themselves. [Indeed, not that it matters, but in category theory, one generally treats all injective function as “inclusions”; that is, for many purposes, the appropriate category-theoretic definition of “a subset of B” is simply “a set A along with an injective function from A into B”]

I don’t know what you mean by “are there closure requirements”, so I’ll just say some random things in the hopes that some of it is helpful:

Well, in this case, that is the initial algebra: a finite list is one you can build up with finitely many invocations of Empty and Concatenation. Indeed, so long as all the constructors are of finitary arity, that’ll be true. Even if you have some constructors of infinitary arity, the elements of the initial algebra will correspond to well-founded rooted trees, each node of which is labelled with a constructor (with the number of children of a node corresponding to the arity of that constructor).

In the most category-theoretic generality, you might no longer be speaking of anything like constructors of particular arities (e.g., data X = CrazyConstructor ((X -> Bool) -> Bool); CrazyConstructor doesn’t really have an arity in the relevant sense (it doesn’t take in some particular number of Xes as arguments to construct a new X)), but you can still make sense of the notion of initial algebra. But perhaps you don’t care about such broad generality. If you only care about recursive specifications given using disjoint union and tupling, without any other constructs, then initial algebras will always correspond to well-founded rooted trees of the sort described above, and terminal coalgebras will always correspond more broadly to such trees without the well-foundedness condition (but still with the condition that every particular node is a finite descendant of the root).

[In case it isn’t clear, in the category-theoretic generality of relevance, an “algebra” is a function from T(X) to X, for some covariant type-constructor T and datatype X. T(X) is thought of as describing all the possible ways to apply a single constructor to X.]

Understandable. Everyone starts somewhere.

9

Er, that should have been placed somewhere else in that post where it would better belong. But anyway:

Given two algebras (let’s say A1 : T(X) → X and A2 : T(Y) → Y), a homomorphism between them, just like in universal algebra, is an operation that commutes with all the operators/constructors. Thus, it will be a function f : X → Y such that A2 . T(f) = f . A1, where T(f) : T(X) → T(Y) is the appropriately “lifted” version of f. [This may well be impenetrable; ask me to explain it more clearly in a second…]

An initial algebra is one with a unique homomorphism to any other algebra. In universal algebraic terms, it’s freely generated (on 0 generators). “Initial” and “free” are essentially synonyms.

Indeed, if you have familiarity with universal algebra, then all of this stuff about algebras is potentially very familiar, so long as you don’t worry about the added category-theoretic generality. (But the whole connection to coalgebras is in that generality, via turning all the arrows in a category around)

[Shit, I think this last post may not be very helpful to anyone who doesn’t already know the material. Well, the easiest way to make it better is for you to point out what needs better explaining, and then I’ll tend to that part.]

10

It should be pointed out that the induction principle for the list datatype in the OP is technically incorrect, as least for Haskell datatypes, which are all pointed. There’s another case that needs to be considered: the case for bottom. See the paper “Fast and Loose Reasoning is Morally Correct” which however shows that such simplified induction principles are in many cases correct.

11

On preview: What I’m really trying to understand with this thread is whether it’s reasonable to hope that I can use corecursion and coinduction without understanding “all the details”. For instance, I can define datatypes in Haskell and see how to write recursive functions and inductive proofs without having to know exactly what the precise mathematical structures involved are. I’m hoping that I can get to a similar point with infinite structures, but right now all of the expositions seem to be aimed at people who know a lot of programming language theory, which makes it a little impenetrable to me.

OK, that makes sense. The way I’m thinking about it, which may not be the best way, is that the initial algebra FinList is the smallest set which satisfies two conditions:
[ol]
[li]Empty \in FinList[/li][li]x \in Int & list \in FinList -> Concatenation x list \in FinList[/li][/ol]
That doesn’t seem to be significantly different from viewing FinList as the set of objects that you can get by finitely many applications of the constructor, which I think is how you’re thinking about it. Is that right?

Yes, I think these are the only objects I’m interested in. Basically finite or countably infinite combinatorial objects, which I think is captured here.

I don’t know a lot of universal algebra, but I think I mostly follow this. What does it mean for a type constructor to be covariant?

This isn’t obvious to me. Is it important, or is it a detail I can safely ignore.

I think I know what “pointed” means here, but let me make sure: If you view FinList as a lattice where x \leq y if and only if y can be constructed from x, pointedness corresponds to the existence of a least element. If that’s the case, can we take Empty to be the bottom element here? I can see why that’s a problem if you have distinct nullary constructors Empty1 and Empty2, but since we don’t, do we need to worry about that?

12

“pointed” does mean there’s a least element, but not in the sense you’re thinking of; more like “least information”. Specifically, in Haskell, there’s the element (often called “bottom”) which you might think of as corresponding to running forever without anything to show for it: the one defined by “let x = x”. In a strict programming language, you might use an analysis in which this doesn’t actually define an element of the list datatype (just sending the program into a non-returning blackhole instead), but in Haskell, with all its laziness, this really does assign a value to x, just not a very informative one.

The Haskell list type fails to satisfy naive induction in a number of other ways, as well; after all, it contains infinite lists!

It’s easiest to think of the Haskell “data” construct as producing terminal coalgebras, not initial algebras, because Haskell allows for all these infinite values. (There’s still a sense in which they are initial algebras in the context of Haskell (without strictness annotations) as well, because there aren’t any other types around that actually have such finiteness restrictions, but… that’s a detail perhaps worth returning to only later)

For now, I’m going to keep speaking not of Haskell, but of “naive”, straight-up normal sets and functions. (Even though I’ll keep using Haskell notation whenever it pleases me). I think it’s easiest to first understand things in that context.

13

Ah, ok. Yes, I think that’s reasonable; I’ll try and keep that in mind in my responses from hereon.

Sure, that’s an excellent way of thinking about it. But let me tease out something that’s implicit there: “smallest” means nothing is in the set except insofar as those rules force it to be. But you also implicitly require that no things in the set are equal except insofar as those conditions force it to be (e.g., “Empty” and “Concatenate(0, Empty)” aren’t equal in FinList).

So instead of saying “smallest”, let’s say “Nothing exists except insofar as those conditions force it to exist, and nothing is equal except insofar as they are forced to be equal”. Or, more explicitly, “Nothing is a FinList except insofar as the conditions ‘Empty is a FinList, and the Concatenation of an integer with a FinList is a FinList’ force it to be a FinList, and no two FinLists are equal except insofar as the conditions ‘Empty is equal to Empty, and Concatenating the same integer to equal FinLists results in equal FinLists’ forces them to be equal”. That’s the initial algebra.

The terminal coalgebra is where everything exists except insofar as the conditions won’t let it exist, and everything is equal except insofar as the conditions won’t let them be equal. Specifically, “Everything is a Stream except insofar as the condition ‘Every Stream is either Empty or the Concatenation of an integer with a Stream’ prevents it from being a Stream. Every two Streams are equal except insofar as the condition ‘Equal Streams are either both Empty or are Concatenations of the same integer to equal Streams’ prevents them from being equal”.

That it comes with some sort of way to take arbitrary functions of type X -> Y to functions of type T(X) -> T(Y), in a composition-preserving way. [E.g., for the list type constructor, this is called “map”]. But this is among the details you can likely safely ignore given your particular goals; if you’re only thinking about type constructors built out of tupling and tagged unions, everything is automatically covariant in a straightforward way.

You can safely ignore it.

14

The equality condition might seem odd. Let me motivate it: it basically says “Nothing has any properties beyond what it can be seen to have with finite inspection”.

Consider the type of, say, sequences of integers which are either finite (e.g., [0, 1, 2, 3]), countably infinite in the ordinary way (e.g., [0, 1, 2, 3, …]), or countably infinite in the ordinary way along with a “last” element (e.g., [0, 1, 2, 3, …, 7]).

To be one of these sequences is the same as to be either Empty or the Concatenation of an integer to one of these sequences. In that sense, the set of these sequences satisfies the same recursive property as the Stream datatype. But are the sequences [0, 1, 2, 3, …] and [0, 1, 2, 3, …, 7] equal? Well, the only difference between them is that the latter has this 7 at the end… but no amount of finite unwrapping would ever find that 7. Insofar as any finite inspection could determine, these lists have no difference. The final 7 is utterly irrelevant. You could only consider [0, 1, 2, 3, …, 7] a Stream if you were willing to consider it the same Stream as [0, 1, 2, 3, …].

So the equality condition in terminal coalgebraicity says “Yes, you can be infinite, but you can’t contain any distinguishing information other than what’s finitely reachable”. In other words, as put above, the elements of the terminal coalgebra are rooted constructor-trees which may be infinite, but still have the property that every node is at some finite depth from the root.

All of this is what you would probably take the simple informal definition “Terminal coalgebra = now allow for infinitely many applications of the constructors” to naively mean anyway, just spelt out more to make sure.

15

That all seems pretty clear.

And that’s where the notion of observational equivalence comes from, right?

Assuming that I don’t need to worry about pointed types in Haskell, I think I’m comfortable with everything we’ve discussed about induction and recursion. I’ll start trying to wrap my head around the coinduction and corecursion stuff from earlier, and see if I can’t get somewhere with it.

16

Well, it could come from a lot of places, but that’s one place it might come up.

If it helps, you can in fact think of coinduction as an instance of induction on natural numbers: the premises needed to coinductively establish that some equivalence relation entails actual equality are precisely the premises needed to inductively establish that the equivalence relation entails looking the same up to depth n, for all n.

For example, given an equivalence relation E, if you know that E-equivalent Streams are either both Empty or both Concatenations of the same integer to E-equivalent streams, coinduction says you can conclude that E-equivalent Streams are equal. But even if you’d never heard of “coinduction”, you could establish by induction on n that E-equivalent Streams agree on their first n elements, for all n, and then conclude (by an “Equality is looking the same up to arbitrary finite depth” principle) that E-equivalent Streams are equal. Whether you call this “induction” or “coinduction” depends on how you look at it, but it’s the same result from the same premises either way.

17

Thinking about this, it seems like a corecursive function would look largely the same as a recursive function: define the function for Empty, and then define the function for Concatenation. Is there really any content here when you’re limited to construction by tuples and disjoint unions, or do you need something like CrazyConstructor above in order to see a difference?

18

Well… I’m not sure what exactly you mean by that. In considering the possibilities, you may be saying that from a place of understanding things fine now and I should be saying “Yes, exactly”, or you may be saying that from a place of having some confusions still and I should be saying “No, not quite”. So here’s what I’ll say in response (and let me know if it’s helpful or not to the point):

A corecursive function doesn’t take a Stream as input and produce something else as output. It takes something else as input and produces Streams as output. You’re aware of that, right?

So here’s an example of a corecursively defined function: consider the process of taking in a real number r in [0, 1) and then outputting either “Yes, r is zero” or “No, r is not zero; here’s the integer floor(10 * r) and here’s the new real number r - floor(10 * r)/10”. [On some implementation of real numbers for which you can robustly test whether they’re 0 or not and take integer floors and so on]

The corresponding corecursive function sends a real number to a Stream of integers, whose elements are the digits of the input’s decimal expansion, terminating after the last non-zero digit if it is possible to use such a representation.

It doesn’t start by asking of its input “Is this Empty or is this a Concatenation”, because its input isn’t a Stream. But it does start by asking of its input “Will this lead to an Empty output or will this lead to a Concatenation output?”. If you’re happy still thinking of that sort of thing as recursion, then you don’t need to think of recursion and corecursion as separate things.

Indeed, recursion and corecursion can be made to look very, very similar in Haskell (but this is basically because (typical) Haskell is infused with a corecursive spirit; it doesn’t actually have familiar inductive types like “finite natural numbers” and “finite lists” and so on; if you try to define “FinList” in Haskell, it’ll act exactly like “Stream”, with infinite lists and everything)

Consider this function definition:



curse :: Functor f => (a -> f a) -> (f b -> b) -> a -> b
curse unwrap wrap = let f x = wrap $ fmap f $ unwrap x in f

If you say how to “unwrap” inputs and how to correspondingly “wrap” outputs, this peels inputs apart and then mimicks their structure in the output, in a sense.

Recursion is what you get when you fix the type a to be an initial algebra, and unwrap to be the corresponding unwrapper. [For example, taking unwrap to be the function



unwrap :: [Int] -> Either () (Int, [Int])
unwrap [] = Left ()
unwrap (head:tail) = Right (head, tail)

, thinking of [Int] as FinList (and fmap as



fmap :: (a -> b) -> Either () a -> Either () b
fmap f (Left ()) = Left ()
fmap f (Right x) = Right (f x)

)]. Then the further “wrap” argument would be a specification of how to inductively build up an output value (with a base case, a recursive case, etc.); you would call this defining the function by recursion on the input FinList.

Corecursion is what you get when you fix “b” to be a terminal coalgebra, and “wrap” to be the corresopnding wrapper. [For example, taking wrap to be the function



wrap :: Either () (Int, [Int]) -> [Int]
wrap (Left ()) = Empty
wrap (Right (head, tail)) = Concatenation head tail

, thinking of [Int] as Stream]. Then the further “unwrap” argument would be a specification of how to peel apart the input (possibly producing a base case, possibly producing a non-base case…); you would call this defining the function by corecursion on the output Stream.

In some sense, it’s all the same if you can’t enforce finiteness requirements. If you can enforce finiteness requirements, then curse can’t always be well-defined; it must “break” in some way when asked to output the FinList containing the digits of 1/3, or the natural number containing the length of the Stream [0, 0, 0, 0, …]. And then you might want to learn what an initial algebra is and a terminal coalgebra and so on, to understand what kinds of things curse is actually well-defined on. But you just want to understand what curse does as a down-in-the-trenches, spare-me-the-theory programmer, then you can just read its code above, and not worry about when it should be called recursion, corecursion, or even something else.

19

Bug corrected in bold. (I had it right and then, in worrying about bugs, I off-by-oned myself out of it…)

Missing word reinstated in bold.

20

I suddenly realize I should have made the following terminological clarification long ago:

The sense of “recursion” which is tied to initial algebras is where the word actually means “primitive recursion” (note: primitive recursion doesn’t only make sense for natural numbers, but for all kinds of inductive types; for example, “foldr” is the primitive recursor for finite lists in Haskell). And “corecursion” is a word for some mirror-image of that process.

If “recursion” means more broadly “The phenomenon of functions which might possibly call themselves”, then “corecursion” (which might better be called “primitive corecursion”) is just a special form of this, just like its mirror-image “primitive recursion” is just a special form of self-calling behavior.