coqrecursion-schemes

# Infinite recursive types in Coq (for Bananas and Lenses)

I'd like to see a Coq version of the Bananas, Lenses, etc. They are built up in the excellent series of blog posts at sumtypeofway Introduction to Recursion schemes

However, the blog post is in Haskell, which permits infinite non-terminating recursion, and thus is perfectly content with the `Y` combinator. Which Coq isn't.

In particular, the definitions depend on the type

``````newtype Term f = In { out :: f (Term f) }
``````

which builds inifinite types `f (f (f (f ...)))`. `Term f` permits very pretty and succinct definitions for catamorphisms, paramorphisms, anamorphisms, etc., using the Term family of types.

Trying to port this to Coq as

``````Inductive Term f : Type := {out:f (Term f)}.
``````

gives me the expected

``````Error: Non strictly positive occurrence of "Term" in "f (Term f) -> Term f".
``````

Q: What would be a good way to formalize the above Haskell Term type in Coq?

Above `f` is of type `Type->Type`, but perhaps it is too general, and there could be some way to restrict us to inductive types such that each application of `f` is decreasing?

Perhaps someone has already implemented the recursion schemes from Banans, Lenses, Envelopes in Coq?

Solution

• I think the popular solution is to encode functors as "containers", the intro of this paper is a good starting point: https://arxiv.org/pdf/1805.08059.pdf The idea is much older (the paper means to give a self-contained explanation), and you can chase the references from that paper, but what I found in a cursory search can be hard to follow if you're not familiar with type theory or category theory.

In short, instead of `Type -> Type`, we use the following type:

``````Set Implicit Arguments.
Set Contextual Implicit.

Record container : Type := {
shape : Type;
pos : shape -> Type;
}.
``````

where roughly, if you imagine a "base functor" `F` of a recursive type `Fix F`, `shape` describes the constructors of `F`, and for each constructor, `pos` enumerates the "holes" in it. So the base functor of `List`

``````data ListF a x
= NilF       -- no holes
| ConsF a x  -- one hole x
``````

is given by this container:

``````Inductive list_shape a :=
| NilF : list_shape a
| ConsF : a -> list_shape a.

Definition list_pos a (s : list_shape a) : Type :=
match s with
| NilF    => False (* no holes *)
| ConsF _ => True  (* one hole x *)
end.

Definition list_container a : container := {|
shape := list_shape a;
pos := fun s => list_pos s;
|}.
``````

The point is that this container describes a strictly positive functor:

``````Inductive ext (c : container) (a : Type) : Type := {
this_shape : shape c;
this_rec : pos c this_shape -> a;
}.

Definition listF a : Type -> Type := ext (list_container a).
``````

so instead of `Fix f = f (Fix f)`, the fixpoint construction can take a container:

``````Inductive Fix (c : container) : Type := MkFix : ext c (Fix c) -> Fix c.
``````

Not all functors can be encoded as containers (the continuation functor being a prime example) but you don't often see them used with `Fix`.