DCS Part II: Mendler Inductive-Functor Algebras

Mendler-inductive functor algebras. What are they? How do you use them for recursion? Seriously, what are they?

First off, functor algebras, section 4.1 in the paper. they’re a category theory thing that generalizes algebraic structure. The way we’re thinking about them is that we have a functor F called the “signature functor”, and a type X called the carrier type; an F-algebra with carrier X is a function F X -> X. One big thing we can do with this function is take an F (F X) to an F X to an X, folding an arbitrary number of Fs down to the X at the bottom. We’ll be taking a fixed point of F, i.e. a type T where T = F T, called 𝜇F; folding an F-algebra with carrier X will give us a function 𝜇F -> X, which in category-theory terms is a “catamorphism”.

We can use this to define a datatype that’s practically recursive without having a recursive definition. The example given is lists. ListF A is a functor for lists with elements of type A. The carrier X represents the type of the tail, which we’re leaving as a parameter (so we can take a fixed-point over it).

Inductive ListF (A X: Set) : Set :=
| Nil : ListF A X
| Cons : A -> X -> ListF A X.

The special part here is the Cons constructor. We’re consing an object of type A to an object of the carrier type X, which is a parameter to ListF A X and could hypothetically be anything. ListF A, then, has one parameter open, and it’s easy to see that it’s a functor - if you have a ListF A X and a function X -> Y, you just apply the function to the tail. So to make the actual List type, we take a fixed point of ListF A, which we’ll call List A. List A = ListF A (List A), i.e. a list whose tail is another list. This requires impredicative sets, which is at odds with normal Coq practice, but is possible to support. I believe this is what the “Mendler-style” recursion/induction means, though the actual Mendler paper goes way over my head (Predicative Type Universes and Primitive Recursion, 1991, DOI 10.1109/LICS.1991.151642).

To typecheck a List A, we do have to check that the tail type is List A, which is a bit scary at first - what if typechecking doesn’t terminate? But we’re guaranteed to eventually hit a Nil, which doesn’t care about its carrier, and we can just say “yeah this is valid, stop checking”. So the fixed point can’t make the typechecker run forever.

Where it gets weird is when we start thinking about algebras that aren’t fixed points. It turns out these look a lot like recursive functions:

Definition lengthAlg (A : Set)
(d : ListF A nat) : nat :=
match d with
  Nil => 0
| Cons x xs => 1 + xs
end.

lengthAlg A has type (ListF A) nat -> nat, which makes it a ListF A-algebra with carrier nat. The Cons x xs => 1 + xs typechecks because xs is a nat.

This is where the fold/catamorphism is relevant. Let’s start with a List Char with one element, and unfold the fixed point in the type signature until we get to Nil.

Cons 'a' Nil: ListF Char (ListF Char (List Char))

Since Nil can have any carrier, we can also type that same expression as:

Cons 'a' Nil: ListF Char (ListF Char nat)

Then we can map lengthAlg down the list and convert our Nil to 0, giving us:

Cons 'a' 0: ListF Char nat

Another application of lengthAlg converts it to 1, the length of the list. Thus folding lengthAlg over a list gives us our catamorphism of type List A -> nat which lets us take the length of an arbitrary list.

Expanding beyond lists, the DCS language has a very different syntax, but for simple cases it does essentially this. Natural numbers are handled by a functor Nat with constructors 0 and Succ X where X is the carrier, though this is abstracted away in the code by what appears to be a recursive datatype declaration. The add function in the Stdlib is a Nat-algebra with carrier Nat -> Nat, i.e. a function Nat -> Nat -> Nat. (This does make it a bit more complex than usual, as it has to construct a function to return. The code could be simplified by moving the lambda binding up: putting it outside the pattern-match would remove the repeated bindings in the branches, and putting it outside the algebra entirely would let the algebra be (Add n) with carrier Nat. But both of these options would require more work to be done inside the curried function, hurting performance.)

As for how this works in a termination checker, that bit is beyond me yet. Future post to come if i ever figure it out. I might have to go against my will and install…. emacs.