7
$\begingroup$

If we consider a definition of recursive type as:

F : Type -> Type;
T = fix F;

It is customary to talk about the functor F needing to be positive or strictly positive in order to avoid non-termination in the recursor.

I'm familiar with the usual syntactic definition of strict positivity, but I'm looking for corresponding semantic definitions, especially ones that can be expressed in the system (rather than being defined at the meta level).

The closest I have found is the work on containers (Abbott et.al., 2005), but it appears to require some "creativity" to come up with a container corresponding to a given functor and then prove equivalence between the two. I'm looking for something that talks more directly about the properties of F.

Improve this question
$\endgroup$
3
  • $\begingroup$ I'm confused: a functor is "positive" if it is co-variant, that is it has a map_f : (A -> B) -> F A -> F B. What more do you need? $\endgroup$
    – cody
    Feb 3, 2020 at 19:42
  • $\begingroup$ @cody: Duh, yes, I see I messed my copy&paste and left plain positivity in there. I'm looking for the "strict positivity". I updated my question accordingly. $\endgroup$
    – Stefan
    Feb 3, 2020 at 21:32
  • 1
    $\begingroup$ Some sort of accessibility? $\endgroup$
    – Andrej Bauer
    Feb 4, 2020 at 7:41

1 Answer 1

Reset to default
9
$\begingroup$

One semantic criterion is preservation of $\omega$-colimits, or $\omega$-cocontinuity. AFAIK, initial algebras of such functors correspond to finitary inductive types in type theory. The construction of initial algebras, given by Adámek's theorem, can be formalized inside type theory as well. It's described in this paper and there's a Coq formalization for it. Probably there is a generalization of this to transfinite colimits, which would give us infinitary inductive types, but for this I don't know any formalization.

Improve this answer
$\endgroup$
1
  • $\begingroup$ That's $\aleph_0$-accessibility, is it not? I was thinking that accessibility should have a type-theoretic formulation in which the cardinals are replaced by universes (so a $U$-accessible functor), but then we still need another condition that captures preservation of "filtered $U$-colimits", whatever that is. $\endgroup$
    – Andrej Bauer
    Feb 7, 2020 at 9:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.