Infinite recursive types in Coq (for Bananas and Lenses)

Question

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?

Answer 1

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.

Full gist: https://gist.github.com/Lysxia/21dd5fc7b79ced410b129f31ddf25c12