<p>Let me reformulate the question like this:</p>
<p>&quot;Which functors have least fixpoints that represent data structures that can be traversed in a finite number of operations?&quot;</p>
<p>We are looking for data structures like a finite list or a finite tree, such that each particular value of a list or a tree will store only a finite number of data items. However, that total size is not limited in advance, so we can have lists and trees that are arbitrarily large (but always finite).</p>
<p>The &quot;traversability&quot; is defined formally via the property of being a &quot;traversable functor&quot;. There is a classification theorem for traversable functors, saying that they are all &quot;finitary containers&quot;. This was proved independently by Bird et al., in the paper &quot;Understanding idiomatic traversals backwards and forwards&quot; <a href="https://www.cs.ox.ac.uk/jeremy.gibbons/publications/uitbaf.pdf" rel="nofollow noreferrer">https://www.cs.ox.ac.uk/jeremy.gibbons/publications/uitbaf.pdf</a> and by Jaskelioff and O'Connor, in the paper &quot;A representation theorem for second-order functionals&quot;  <a href="https://arxiv.org/pdf/1402.1699.pdf" rel="nofollow noreferrer">https://arxiv.org/pdf/1402.1699.pdf</a></p>
<p>A &quot;finitary container&quot; is a polynomial functor that is generated by a fixed family of &quot;shapes&quot; and whose possible values can be enumerated in a certain way.</p>
<p>So, most likely you are asking the question, what functors have finitary containers as their least fixpoints. I believe the answer is again &quot;finitary containers&quot; but with two type parameters.</p>
<p>If you take a bifunctor <span class="math-container">$F$</span> that is a finitary container and impose a fixpoint on the second type parameter, you will again get a finitary container (<span class="math-container">$G ~a =  \mu x.~F~a~x$</span>).</p>

CC BY-SA 4.0
2024-10-23T11:10:59.097Z
Thank you very much for the answer!
shintuku
CC BY-SA 4.0
2024-10-10T08:24:24.293Z
2024-10-10T08:24:24.293Z
winitzki
<p>Am currently reading Types and Programming Languages' chapter on the Metatheory of recursive types, and we see a couple of examples of least fixed points of type-functors that provide a definition for types that can be traversed in a finite number of operations. However type-functors in Haskell, for example, may have least fixed points that produce types that cannot be enumerated in a finite number of operations. So when do least fixed points of type-functors provide us with well-founded data types?</p>

CC BY-SA 4.0
2024-10-06T21:45:33.607Z
The initial algerba for the functor $F(X) = 1 + X^\mathbb{N}$ is the type of countably-branching well-founded trees, some of which are infinite, and there are uncountably many of them. So, what do oyu think "well-founded" means?
Andrej Bauer
CC BY-SA 4.0
2024-10-07T03:22:50.300Z
@AndrejBauer I forgot about those. can any definition of interest capture the idea of traversable in a finite number of operations?
shintuku
CC BY-SA 4.0
2024-10-07T05:54:00.737Z
I am trying to capture some notion of computable types, types who can be exhausted/listed through machine iteration
shintuku
CC BY-SA 4.0
2024-10-07T08:35:39.050Z
I believe that if a functor $F$ is polynomial then its initial algebra will be "traversable in a finite number of operations". The example Andrej gave was non-polynomial.
winitzki
CC BY-SA 4.0
2024-10-07T15:49:13.053Z
@winitzki That's not correct. That *is* a polynomial functor. The exponents of these sort of abstract polynomials are not necessarily finite.
Dan Doel
CC BY-SA 4.0
2024-10-07T16:23:08.717Z
By "exhaustible/listed" you could mean (a) listed in finite time (b) a possibly infinite enumeration of all the elements or (c) exhaustible in the sense of Martín Escardó, i.e., there is a search operator that finds an element satisfying a given predicate. Which one would it be, please edit your question to make it clear. (And stop using the phrase "well-founded".)
Andrej Bauer
CC BY-SA 4.0
2024-10-07T17:29:55.393Z
@DanDoel I believe that functor would be written as the type $F ~ A = 1 + \mathbb N \to A$, and that involves an infinite product, as it is not just a finite combination of products and co-products. An infinite product is what causes trouble. Is there another word (like "finite in an ordinary sense") that describes polynomial functors without infinite products or sums? I believe you cannot express an infinite product like that $F$ as a least fixpoint of some polynomial functor that is "finite in an ordinary sense".
winitzki
CC BY-SA 4.0
2024-10-08T21:19:44.107Z
@winitzki: Your definition of $F$ is the same as mine, just using different notation for exponentials. You also are mistaken about what "polynomial functor" means, because it's not "just a finite combination of products and co-products". Please consult https://ncatlab.org/nlab/show/polynomial+functor.
Andrej Bauer
<ds.data-structures><ct.category-theory><recursion><domain-theory><inductive-type>
When do least fixed points of type-functors provide well-founded data types?
shintuku
# When do least fixed points of type-functors provide well-founded data types?

(Asked by: username_0 on 2024-10-06)

Am currently reading Types and Programming Languages' chapter on the Metatheory of recursive types, and we see a couple of examples of least fixed points of type-functors that provide a definition for types that can be traversed in a finite number of operations. However type-functors in Haskell, for example, may have least fixed points that produce types that cannot be enumerated in a finite number of operations. So when do least fixed points of type-functors provide us with well-founded data types?

**Tags:** ds.data-structures, ct.category-theory, recursion, domain-theory, inductive-type
> **Comments:**
> **username_1**: The initial algerba for the functor $F(X) = 1 + X^\mathbb{N}$ is the type of countably-branching well-founded trees, some of which are infinite, and there are uncountably many of them. So, what do oyu think "well-founded" means?  
> **username_0**: @AndrejBauer I forgot about those. can any definition of interest capture the idea of traversable in a finite number of operations?  
> **username_0**: I am trying to capture some notion of computable types, types who can be exhausted/listed through machine iteration  
> **username_2**: I believe that if a functor $F$ is polynomial then its initial algebra will be "traversable in a finite number of operations". The example Andrej gave was non-polynomial.  
> **username_3**: @winitzki That's not correct. That *is* a polynomial functor. The exponents of these sort of abstract polynomials are not necessarily finite.  
> **username_1**: By "exhaustible/listed" you could mean (a) listed in finite time (b) a possibly infinite enumeration of all the elements or (c) exhaustible in the sense of Martín Escardó, i.e., there is a search operator that finds an element satisfying a given predicate. Which one would it be, please edit your question to make it clear. (And stop using the phrase "well-founded".)  
> **username_2**: @DanDoel I believe that functor would be written as the type $F ~ A = 1 + \mathbb N \to A$, and that involves an infinite product, as it is not just a finite combination of products and co-products. An infinite product is what causes trouble. Is there another word (like "finite in an ordinary sense") that describes polynomial functors without infinite products or sums? I believe you cannot express an infinite product like that $F$ as a least fixpoint of some polynomial functor that is "finite in an ordinary sense".  
> **username_1**: @winitzki: Your definition of $F$ is the same as mine, just using different notation for exponentials. You also are mistaken about what "polynomial functor" means, because it's not "just a finite combination of products and co-products". Please consult https://ncatlab.org/nlab/show/polynomial+functor.  

---

## 1 answers

### Answer by username_2 on 2024-10-10. Score: 1 | Accepted answer

Let me reformulate the question like this:

"Which functors have least fixpoints that represent data structures that can be traversed in a finite number of operations?"

We are looking for data structures like a finite list or a finite tree, such that each particular value of a list or a tree will store only a finite number of data items. However, that total size is not limited in advance, so we can have lists and trees that are arbitrarily large (but always finite).

The "traversability" is defined formally via the property of being a "traversable functor". There is a classification theorem for traversable functors, saying that they are all "finitary containers". This was proved independently by Bird et al., in the paper "Understanding idiomatic traversals backwards and forwards" <https://www.cs.ox.ac.uk/jeremy.gibbons/publications/uitbaf.pdf> and by Jaskelioff and O'Connor, in the paper "A representation theorem for second-order functionals" <https://arxiv.org/pdf/1402.1699.pdf>

A "finitary container" is a polynomial functor that is generated by a fixed family of "shapes" and whose possible values can be enumerated in a certain way.

So, most likely you are asking the question, what functors have finitary containers as their least fixpoints. I believe the answer is again "finitary containers" but with two type parameters.

If you take a bifunctor $F$ that is a finitary container and impose a fixpoint on the second type parameter, you will again get a finitary container ($G ~a = \mu x.~F~a~x$).

> **Comments:**
> **username_0**: Thank you very much for the answer!  

---

