Search code examples
monadsfree-monadchurch-encoding

Are Free monads are Church numerals?


A commentator recently stated:

Free monads are Church numerals -- just using (endo-) functors instead of functions!

He goes on to explain this saying:

they are both an endofunct(ion|or) composed 0 - n times

I get that Church Numerals are a set of anonymous function compositions, with a composition for each number. I just don't see how that applies to Free Monads.

My question is: Are Free monads are Church numerals?


Solution

  • Sort of.

    A generalization of Church numerals is where the numeral n is f^n where f is an endomorphism (an arrow whose domain and codomain is the same object) in some category and f^n means "compose f with itself n times". The ordinary Church numerals are in the category of sets where the arrows are functions, so e.g. the numeral 3 applied to f and x is f(f(f(x))). For example if f(x) = x + 10, then 3 f 0 is 30.

    In a category of categories, the arrows are functors. There, the numeral 3 applied to some functor f and object x (for example, a type), is again f(f(f(x))). If f is e.g. the type constructor f x = Int => x, then 3 f String is Int => Int => Int => String, the type of functions that take three Int arguments and return a String.

    Now, for a functor f, Free f is the free monad generated by f, where an instance of the type Free f x is either just an x or an f (Free f x). So it will have a type of the form f(f(f(...(x))), a composition of zero or more fs applied to x.

    So it's not that "free monads are Church numerals", but that a free monad is a type construction on some functor, and the Church numerals on that functor embed in that type.