Stream: Coq users

Topic: Whatis induction-recursion?

walker (Jan 07 2023 at 13:48):

I am reading the paper: Decidability of Conversion for Type Theory in Type Theory
and they mention they require somegthing called "induction-recursion"

and then there is this gist https://gist.github.com/jcmckeown/07d844a9724745cedd61 which implies that this feature is not in coq, and based on the explanation, it sounds like mutual inductive types, can someone help me get un-lost in this area ?

Karl Palmskog (Jan 07 2023 at 13:50):

"Feature request: induction-recursion" https://github.com/coq/coq/issues/4259

walker (Jan 07 2023 at 13:51):

so it is not there, but what are alternative options/workarounds ? (given that I don't even know what induction-recursion is to start with)

Paolo Giarrusso (Jan 07 2023 at 14:30):

Not sure on the alternative (other than "use dependent types less"), but it is a form of mutual recursion: it just involves datatypes (inductive) and functions (recursive).

Kenji Maillard (Jan 07 2023 at 14:34):

Induction-recursion is a scheme to define inductively a type mutually with a function on this type given recursively. The typical example of an Inductive-recursive type is that of a universe of code U : Type together with a decoding function El : U -> Type. In pseudo Coq code for instance you might hope to be able to write (if Coq supported induction-recursion which it does not)

Inductive U : Type :=
| codeBool : U
| codePi : forall (domain : U) (codomain : El domain -> U), U
with El (A : U) : Type :=
match A with
| codeBool => Bool
| codePi A B => forall (a : El A), El (B a).

Note that El is required in the constructor codePiand conversely the two constructors of U are required to be able to define El

Paolo Giarrusso (Jan 07 2023 at 14:35):

Thanks Kanji, that's a nicer explanation...

Kenji Maillard (Jan 07 2023 at 14:36):

For references, I guess one of the original point to go is Induction recursion and initial algebras, and the phd thesis of Fredrik Nordvall Forsberg

Paolo Giarrusso (Jan 07 2023 at 14:36):

IIRC a common use case is that the indexes of your inductive mention the recursive function, and sometimes that can disappear with less precise types; for instance, switching from intrinsically typed terms (Exp T) back to intrinsically typed (Exp). OTOH, for the paper you mention it would probably be a major change. I'm not sure how well what they do would even work.

Kenji Maillard (Jan 07 2023 at 14:38):

And then there are encodings of some form of induction recursion in Coq, usually by first passing through an inductive-inductive definition where you replace the function El by its graph ElGraph : U -> Type -> Type and then using an encoding of induction-induction such as that one (For finitary induction-induction, induction is enough ) (Edit: That encoding probably does not work for the case of a universe of codes, but there is another one presented in partial univalence in n-truncated type theory that I use quite often)

Kenji Maillard (Jan 07 2023 at 14:41):

For the paper you mention, Loic Pujet managed to do an encoding using only indexed inductive types in Agda last year, and a few people are trying to port this encoding to Coq but it is largely a work in progress

Paolo Giarrusso (Jan 07 2023 at 14:43):

I'm sorry, but the link on "that one" isn't working for me... Could somebody please post the URL?

walker (Jan 07 2023 at 17:16):

thanks for the clarifications from everyone

Ali Caglayan (Jan 07 2023 at 20:43):

Before we can support induction-induction or induction-recursion, we need to generalize fix points so that the types of later clauses can depend on the bodies of previous clauses. This has been called "recursion-recursion" by some. @Matthieu Sozeau had a ind-rec patch which we diluted to a rec-rec patch at some point, but there is a lot going on so we never made progress on it.

The general idea of the patch is to replace List.map in the fixpoint datastructure with List.foldl or something. Once we have rec-rec then implementing ind-ind or ind-rec will become clearer, and will essentially require internalising the codes for such definitions. ind-rec at least has a clear compilation but ind-ind always has some extra incompatability which needs thinking about. (Basically ind-ind also changes the proof strength of Coq only in the absense of axiom K.

Ali Caglayan (Jan 07 2023 at 20:43):

Agda has had both for a while, so maybe the main issue is lack of developer time and attention.

walker (Jan 07 2023 at 21:05):

@Ali Caglayan May I ask how hard is that (given my non-existant knowledge of ocaml), maybe you have estimation of how long it will take working full time on it (1 month, one year)?
If I am ever going to work on this feature, my goal will not just have a POC but instead have it upstream so the time to upstream is what I am mostly interested in ?

Ali Caglayan (Jan 07 2023 at 21:09):

I mean the feature was already basically implemented by @Matthieu Sozeau. Most of the work is rebasing on top of a newer Coq, trying to understand how the PR was meant to work and trying to understand how Coq works. Once you get something that runs, then you spend time fixing the test-suite and any developments in the CI.

Technically, it shouldn't take a long time to do. But it ultimately requires a few weeks total of dev time from a few devs which isn't something I think is available at the moment.

Ali Caglayan (Jan 07 2023 at 21:10):

Depending on your situation that you need it for, there are ways to encode the types you need directly in Coq today.

Ali Caglayan (Jan 07 2023 at 21:11):

Most ind-ind types for instance can be done as a mutual inductive type together with extra checks. Think syntax of type theory with an IsWellTyped predicate. For induction recurison the situation is similar also, as long as you aren't doing something crazy like adding a universe of types.

walker (Jan 07 2023 at 21:11):

Noted, I will have to first understand the paper I am trying to implement thoroughly and then see what is the best approach.

walker (Jan 07 2023 at 21:11):

To be honest,I am still fairly noob

walker (Jan 07 2023 at 21:12):

hopefully I will get back with a plan on Monday

walker (Jan 07 2023 at 21:12):

thanks a lot for the insights

Ali Caglayan (Jan 07 2023 at 21:13):

There is a dev working group coming up soon, I'll make a note to ask if we might spend some time getting RR, II and IR in Coq.

Meven Lennon-Bertrand (Jan 09 2023 at 10:56):

Also note that there are two levels of "having a feature in Coq": one is having it added to the kernel, another is to have all the upper layers know about it and be able to use it properly. Having a feature in the kernel is already nice because you can experiment with it, but if it is not well integrated in the upper layers, you quickly get into trouble if you want to use it in a "real" development… AFAICT this is for instance the current status of SProp: it is in the kernel, but close to nobody uses it yet, because it has poor interaction with eg tactics

Karl Palmskog (Jan 09 2023 at 10:59):

isn't there going to be a rule or recommendation to formalize stuff like induction-induction and induction-recursion and recursion-recursion in MetaCoq first, and then get it into the ML kernel?

Pierre-Marie Pédrot (Jan 09 2023 at 10:59):

(Depending on the kernel feature, it might take a while before the upper layers handle it properly. See e.g. universe polymorphism / primitive projections, introduced in 2014 and which is still quirky)

Karl Palmskog (Jan 09 2023 at 11:00):

I think there is already some rule/recommendation about peer-reviewed paper, but peer reviewing is a bit more hit and miss

Pierre-Marie Pédrot (Jan 09 2023 at 11:00):

@Karl Palmskog While it'd be very nice to have it in MetaCoq before having it in the kernel (which may actually happen) I think that the current difficulties are more about design trade-offs than foundational issues.

walker (Jan 09 2023 at 23:50):

well I am not sure if I will be able to work on that direction for the time being

Last updated: Oct 13 2024 at 01:02 UTC