<p>I think the popular solution is to encode functors as <a href="https://en.wikipedia.org/wiki/Container_(type_theory)" rel="nofollow noreferrer">"containers"</a>, the intro of this paper is a good starting point: <a href="https://arxiv.org/pdf/1805.08059.pdf" rel="nofollow noreferrer">https://arxiv.org/pdf/1805.08059.pdf</a> 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.</p>

<p>In short, instead of <code>Type -&gt; Type</code>, we use the following type:</p>

<pre><code>Set Implicit Arguments.
Set Contextual Implicit.

Record container : Type := {
  shape : Type;
  pos : shape -&gt; Type;
}.
</code></pre>

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

<pre><code>data ListF a x
  = NilF       -- no holes
  | ConsF a x  -- one hole x
</code></pre>

<p>is given by this container:</p>

<pre><code>Inductive list_shape a :=
  | NilF : list_shape a
  | ConsF : a -&gt; list_shape a.

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

Definition list_container a : container := {|
  shape := list_shape a;
  pos := fun s =&gt; list_pos s;
|}.
</code></pre>

<p>The point is that this container describes a strictly positive functor:</p>

<pre><code>Inductive ext (c : container) (a : Type) : Type := {
  this_shape : shape c;
  this_rec : pos c this_shape -&gt; a;
}.

Definition listF a : Type -&gt; Type := ext (list_container a).
</code></pre>

<p>so instead of <code>Fix f = f (Fix f)</code>, the fixpoint construction can take a container:</p>

<pre><code>Inductive Fix (c : container) : Type := MkFix : ext c (Fix c) -&gt; Fix c.
</code></pre>

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

<p>Full gist: <a href="https://gist.github.com/Lysxia/21dd5fc7b79ced410b129f31ddf25c12" rel="nofollow noreferrer">https://gist.github.com/Lysxia/21dd5fc7b79ced410b129f31ddf25c12</a></p>
Infinite recursive types in Coq (for Bananas and Lenses)
<p>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 <a href="https://blog.sumtypeofway.com/an-introduction-to-recursion-schemes/" rel="nofollow noreferrer">sumtypeofway Introduction to Recursion schemes</a></p>

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

<p>In particular, the definitions depend on the type</p>

<pre><code>newtype Term f = In { out :: f (Term f) }
</code></pre>

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

<p>Trying to port this to Coq as </p>

<pre><code>Inductive Term f : Type := {out:f (Term f)}.
</code></pre>

<p>gives me the expected </p>

<pre><code>Error: Non strictly positive occurrence of "Term" in "f (Term f) -&gt; Term f".
</code></pre>

<p><em>Q: What would be a good way to formalize the above Haskell Term type in Coq?</em></p>

<p>Above <code>f</code> is of type <code>Type-&gt;Type</code>, but perhaps it is too general, and there could be some way to restrict us to inductive types such that each application of <code>f</code> is decreasing?</p>

<p>Perhaps someone has already implemented the recursion schemes from <a href="https://research.utwente.nl/en/publications/functional-programming-with-bananas-lenses-envelopes-and-barbed-w" rel="nofollow noreferrer">Banans, Lenses, Envelopes</a> in Coq?</p>