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) }.
I can do this for concrete F
, currently, such as
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?)
Hm, I guess Agda allows polarity pragmas...
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.
@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.
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.
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
.
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.
@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;
}.
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.
@Jason Gross polarity pragmas (in https://agda.readthedocs.io/en/v2.6.1.3/language/positivity-checking.html) shouldn't qualify — there's no way to make them safe, nor a way to attach them to arguments.
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.
Last updated: Dec 01 2023 at 07:01 UTC