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`

.

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

- Coq can't define an inductive proposition
- The `specialize` tatic in Coq does not work well with typeclasses?
- What's the exact rule of applying a theorem in Coq?
- Coq inductive not right form
- Why I can't use exact P if P is a Prop?
- Why we can't use "simpl" on `j = j -> x = y`?
- Why can't I perform rewrite tactic here?
- Prove theorem about the last element of a list
- How do I apply (S n' <=? m) = true to S n' <= m?
- Coq : Using a parametrized Type from within a Module
- How to prove this in Coq
- Software Foundations (lf): proving leb_plus_exists and plus_leb_exists
- Coq QArith division by zero is zero, why?
- Coq/Ltac: is it possible to design a tactic that says the goal is proved when a decision procedure proves it, without the proof term?
- Proving some theorems on the function index in Coq
- Why does coq not recognize that `None = Some v` is false?
- Does import not only import but also change existing definitions?
- In Coq, what would be the steps to prove the correctness of a function that solves puzzles like Sudoku or Takuzu?
- Dependent equality with 2 different type functions
- Equivalence of inductive and recursive
- Efficient Record Construction in Coq: Is Direct Proof Inclusion Possible?
- How would I prove that b = c if (andb b c = orb b c) in coq?
- How to prove (X × Y = ∅) <-> (X = ∅) ∨ (Y = ∅)
- Iris/Coq replacing literal
- How do I install a library in coq? (MacOS)
- Is there a three-valued case analysis on patterns (a < b) (a = b) (a > b)?
- How can I give an alias to a type in coq
- How to prove the goals in more elegant way using ssreflect?
- How to continue case analysis of a nested match in coq?
- Coq: Is there a way to define "map" for Ensemble