Limitation of inductive families · Miscellaneous

Inductive Foo (T1: Type) (T2: T1 -> Type) : A -> B -> Type := ....

At least this is how it works in coq
Is there a limitation that prevents us from having something like:

Inductive Foo (T1: Type) (T2: T1 -> Type) : (a: A) -> B a -> Type := ....

Kenji Maillard (Aug 28 2023 at 12:37):

Inductive Foo (A : Type) (B : A -> Type) : forall (a : A), B a -> Type :=
  | K a b : Foo A B a b.

walker (Aug 28 2023 at 13:40):

Follow up question, I have seen loads of papers for recopies for implementing and formalizing Dependent type theories whether it is MLTT or CoC like Work of Meven, and Steven Schäfer. But I have not seen any work describing the formal implementation details of inductive families and their proofs. I know it exists in metacoq, but it is over generalized and for me, sometimes it is hard to follow. Even in Meven thesis he mentioned, it is lots of details and unless I missed it somehow, it wasn't described how the inner mechanics would work on formal level.

So it is really the case that the implementation details are not formally described in the literature or did I just miss it somewhere?

walker (Aug 28 2023 at 13:42):

This kind of knowledge feels like it is not that obvious, but it is floating in the air in metacoq community, but with no clear recipe.

Paolo Giarrusso (Aug 28 2023 at 13:44):

Paolo Giarrusso (Aug 28 2023 at 13:45):

walker (Aug 28 2023 at 13:55):

I did checked Dybjer papers, they are high level, very very far from implementation.

Perhaps for some people Dybjer papers are detailed enough, but It's been over a month trying to implement the most basic inductive famility, and there are subtle details that are not obvious, at least not to me.

I am not sure if the gap is real, or is it my lack of experience, (in other words, is there no written proofs published somewhere because most people think it is to basic and most people in that domain can connect the dots with ease)

Stefan Monnier (Aug 28 2023 at 15:39):

Could you clarify what it is you're looking for? Several papers from the "early Coq" work give detailed and usable rules for inductive families. E.g. Gimenez's 1994 "Codifying guarded definitions with recursive schemes" or Werner's 1994 PhD "Une Théorie des Constructions Inductives". I have found them sufficient to understand how to implement them. Admittedly, they don't cover the full language used by Coq (e.g. the tower of universes or the more refined positivity checks), but these seem orthogonal to the "families" part of inductive types.

walker (Aug 28 2023 at 17:17):

Well, What was trying to do is the have basic inductive families, with recursors (no pattern matching or fixed points), type checking algorithms, and then proofs of progress and preservation, and that type checking is sound w.r.t the semantics of the language.

The tricky part is getting the proofs of progress and preservation, there two many things that one needed to implement for instance a theory of maps on lists with custom index functions, and bunch of various other small but tricky details. People from MetaCoq project were familiar with those details (which at least gave me the impression that I am not doing things incorrectly) but then they were the only source of information, aside from checking the code base of metacoq.

Meven Lennon-Bertrand (Aug 29 2023 at 10:18):

Are you aware of the latest MetaCoq paper? At least it documents what happens in MetaCoq for inductive families. But I agree that this is very general and complex. As far as I know, there are not many resources (at least, not published papers) that are not either 1) 20-30 years old (like the papers by Gimenez, Paulin-Mohring, Werner…) 2) quite abstract and remote from implementation (like Dybjer's) 3) dealing with something more complex than inductive families with recursors (pattern-matching + fixpoint as in MetaCoq, higher inductive types, induction-recursion/induction-induction, etc.)… So I think you'll have to somehow piece together things from various sources, probably a combination of early Coq papers + MetaCoq?

Meven Lennon-Bertrand (Aug 29 2023 at 10:23):

Note that if you want to provide some semantics, things will get even trickier than just proving PL properties like progress & preservation. As far as I know, a formalized semantics for a dependently-typed language with universes and inductive types would be a proper research project, I don't think there is any out there (it is for instance turrently completely out of MetaCoq's scope). Beware that depending on the exact language you have, this might hit Gödel's incompleteness: as providing a model for a language usually proves its soundness, in a type theory T you can only construct models for type theories less logically powerful than T, because T cannot prove its own soundness.

Karl Palmskog (Aug 29 2023 at 10:28):

they have inductive types formalized in Candle last I checked. Not the full "dependent" part and universes, but still.

walker (Aug 29 2023 at 12:06):

@Meven Lennon-Bertrand what do you mean by "if you want to provide some semantics"?

Do you mean normal small step semantics with single step and multi step, or you mean categorical semantics ?

The whole purpose of what I am doing is experimenting with some form of compiling inductive families and code that touches them, at least formally, but then I need the typing rules and at least type safety. I am not sure where I would require soundness of language model for that ?

Meven Lennon-Bertrand (Aug 29 2023 at 14:27):

Ah, sorry, I went ahead of myself: in this setting, I think "semantics" is usually used to mean some sort of denotational/categorical semantics. Indeed, if you give an operational semantics as a reduction relation, you should be fine. (Note though, that the caveat still applies to proving normalization of the small-step operational semantics, or that every well-typed term is in the domain of the big-step operational semantics, because you can usually use these to show soundness of the inference system.) But I think that given your aims you should not need soundness, and should thus be fine.

Meven Lennon-Bertrand (Aug 29 2023 at 14:30):

In my experience, indices are one of the biggest pain of full-blown inductive types, and these ML-style inductive types usually also do not come with positivity/guard restriction, which are the other big pain of CIC's inductives. Although it still cannot hurt to give a look at what happens there, for sure :)

Stream: Miscellaneous

Topic: Limitation of inductive families

walker (Aug 28 2023 at 12:21):