10
$\begingroup$

When defining an inductive type, there is a famous "positivity" restriction on the constructor types. For example, an inductive type $\mathsf D$ has constructor $\mathsf c : F(\mathsf D) \to \mathsf D$, where $F(\mathsf D)$ is the type of the constructor argument, and it can contain $\mathsf D$ itself. Then the positivity restriction basically states that the proof assistant needs to see that $F$ is a functor $\mathsf{Type} \to \mathsf{Type}$(1). This is crucial because otherwise the induction principle wouldn't make sense: $$\forall (P : \mathsf D \to \mathsf{Prop}).\left(\forall (\vec x : F(\mathsf D)). \mathtt{fmap}_{F} P \, (\vec x) \to P(\mathsf c\, \vec x)\right) \to \forall x. P(x)$$ where $\mathtt{fmap}_F$ is the map on the morphisms associated with the functor $F$. The proof checker, based on the consideration above, implements some syntactic criteria to ensure functorality, which become known as positivity. On the other hand, the "strictly positive" criterion, as I view it, is added to avoid size issues similar to that of set theory.

This has led me to wonder if such a criterion can be relaxed on propositions. In languages having definitionally irrelevant (or related weaker notions of) propositions, the propositions can be roughly viewed as a subsingleton, i.e. a subset of the singleton. This avoids all the size issues. Also, the functorality condition degenerates because of the irrelevance. So perhaps for inductive propositions, we can allow $F : \mathsf{Prop} \to \mathsf{Prop}$ to simply be monotonic. So if the proof checker can deduce (from some syntactic criteria, or by a user supplied proof) that $F(p) \to F(q)$ whenever $p \to q$, then it should allow this inductive definition. In proof assistants embracing classical logic (at least in $\mathsf{Prop}$), this can be much more powerful. The proof checker might just run a small SAT solver to see if the definition is monotonic.

The question is: does this leads to anything interesting (including possible paradoxes when combined with other features in the type theory)? Pointers to existing literature are also welcome.

(1) : Let's ignore universe levels for now. $\mathsf{Type, Prop}$ are just suggestive notations.

$\endgroup$

2 Answers 2

10
$\begingroup$

Impredicative strict Prop supports initial F-algebras for all F : Prop → Prop functors. In Coq:

Require Import Coq.Unicode.Utf8.

Record Functor : Type := mkFunctor
  {ob : SProp → SProp; hom : ∀ (A B : SProp), (A → B) → ob A → ob B}.

Record Alg (F : Functor) : Type := mkAlg
  {carrier : SProp; phi : F.(ob) carrier → carrier}.

Arguments mkAlg {F}.
Arguments carrier {F}.
Arguments phi {F}.

Definition InitAlg (F : Functor) : Alg F :=
  mkAlg (∀ (P : SProp), (F.(ob) P → P) → P)
        (λ fx P c, c (F.(hom) _ _ (λ g, g P c) fx)).

Definition InitAlgInit (F : Functor)(A : Alg F) (x : (InitAlg F).(carrier)) : A.(carrier) :=
  x (A.(carrier)) (A.(phi)).

As you mentioned, all equations can be omitted here because of the irrelevance, and there's no need to consider "dependent" elimination. For ordinary Prop, we would need an axiom of irrelevance to do the same. Impredicativity is generally required, else ∀ (P : SProp), (F.(ob) P → P) → P) doesn't fit in SProp.

I couldn't come up with examples of interesting applications of non-strictly positive SProp-s, maybe someone else here can.

$\endgroup$
2
  • 3
    $\begingroup$ Just a small observation: a functor on propositions is precisely a monotone map, and the proof is just the same as for Tarski's fixed point theorem for monotone maps on complete lattices. $\endgroup$ Apr 6, 2022 at 10:39
  • $\begingroup$ Wouldn't this be useful for type systems? Inductive typ: term -> type -> SProp := | typ_lam: (typ x A -> typ e B) -> typ (lam x e) (fn A B) $\endgroup$ May 6, 2022 at 21:07
1
$\begingroup$

Can't you just use an impredicative encoding of inductive datatypes?

Definition W {A} (B: A → SProp): SProp := ∀ (Q: SProp), (∀ tag, (B tag → Q) → Q) → Q.
Definition sup {A} {B: A → SProp} (tag: A) (f: B tag → W B): W B :=
  λ _ p, p tag (λ b, f b _ p).
Definition W_sind (A: Type) (B: A → SProp) (P: W B → SProp)
           (f: ∀ tag field, (∀ b : B tag, P (field b)) → P (sup tag field)) (w: W B): P w :=
  w (P w) (λ tag field, f tag _ (λ b, field b)).

I ape strict positivity here but I'm not quite sure why just using any old functor shouldn't work.

$\endgroup$
1
  • 2
    $\begingroup$ I second that: the main points of inductive definitions are that 1) they give you better computations than impredicative encodings and 2) they have well-behaved induction principles rather than induction, so that you can show e.g. non-confusion of constructors. But both are unneeded in a propositionally irrelevant setting… People like Werner (see Sets in Types, Types in Sets) do not build propositional inductive types exactly because of this. $\endgroup$ Apr 4, 2022 at 18:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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