positivity parametrization? · Coq devs & plugin devs

Are there any plans to implicit positivity constraints, so that, e.g., I can write

Inductive Fix (F : Type{+} -> Type) : Type := step { unstep : F (Fix F) }.

Inductive nat_step (N : Set) : Set :=
| O : nat_step N
| S : N -> nat_step N.
Inductive NAT := wrap { unwrap : nat_step NAT }.

but I want to be able to reason about this sort of inductive construction in general and build some theory up around it.

(Alternatively, does anyone know of another proof assistant that allows this sort of parameterization?)

Jason Gross (Mar 06 2021 at 16:48):

Jasper Hugunin (Mar 06 2021 at 19:42):

I've spent a lot of time figuring out how to do this in Coq today, without any extensions to the kernel.

My preferred approach starts with defining a universe of codes for strictly positive functors as a Coq inductive type, and then you can define all the generic programs you want from there. I have a paper Why not W (To appear in TYPES 2020 post-proceedings) that works out the definition of the induction principle and existence of least fixed points for strictly positive functors defined internally, among answering other less-related questions.
There are some details and usability aspects that haven't been worked out yet, but I'd love to discuss more if you are interested.

I prefer this to the positivity constraints approach because it stays within the theory: for example, how would you imagine the induction principle for Fix should look like with Inductive Fix (F : Type{+} -> Type) ...? You need some way to lift a predicate over F, and adding that to the kernel seems like an invitation to complexity.

Jason Gross (Mar 08 2021 at 23:19):

@Jasper Hugunin Thanks! That looks interesting, and I'll look into the codes more deeply soon. The trick with canonical looks neat!
Btw, it's pretty easy to construct a "computer scientist's version" of W that allows the desired rules for nat just by splitting up the data a bit more and being explicit about recursive and non-recursive constructors; I did this today at https://gist.github.com/JasonGross/dea27f68289d96e5bb0811e86eb66a63, idk if someone has done this before.

Jasper Hugunin (Mar 08 2021 at 23:32):

Looks cool. I've known about variants on this approach for a while, though I haven't seen them formalized anywhere. My preferred W-like is morally

Inductive W' (A : Type) (B : A -> list (option Type)) : Type :=
  sup (a : A) (_ : fold (map (function None => W' A B | Some X => X -> W' A B) (B a)) (_*_) unit).

where the fold-map bit for the recursive cases would need to be implemented by similar things to your match_option type.

Jasper Hugunin (Mar 08 2021 at 23:35):

Your W' will struggle to encode two infinitary arguments, like Inductive foo := C (_ : nat -> foo) (_ : bool -> foo) : foo. Pushing them together as nat + bool won't quite work, that's why I use list (option Type) instead of your nat * option Type.

Jasper Hugunin (Mar 08 2021 at 23:37):

Your encoding of nat also gets the universes wrong, if I'm not mistaken: I think you get nat : Type@{Set+1} rather than nat : Set. This happens because you have the large arguments A_nr, A_r, and B to your constructors. There are ways to avoid that, and you probably want to.

Jasper Hugunin (Mar 08 2021 at 23:40):

@Jason Gross But you've already come up with a reasonable spartan notion of codes: In your formalization you have roughly

Record Code := {
  A_nr : option Type;
  A_r : option Type;
  B : match A_r return Type with
      | None => unit
      | Some A_r => A_r -> nat (* finite recursion count *) * option Type (* non-finite recursion labels *)
      end;
}.

Jasper Hugunin (Mar 08 2021 at 23:43):

My particular construction from W types was not a large part of the point here. W types are particularly simple to define, and they have strong historical significance, but it may turn out that approaches like your W' give better usability and performance.

Paolo Giarrusso (Mar 11 2021 at 09:55):

Paolo Giarrusso (Mar 11 2021 at 09:57):

IIRC, one objection is that if you replace Type -> Type by k function spaces for k polarities, you need variants of your higher-order functions for the new polarities, _or_ some new construct to avoid that.

Stream: Coq devs & plugin devs

Topic: positivity parametrization?

Jason Gross (Mar 06 2021 at 16:45):