In inductive families we can have things like:

```
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 := ....
```

There is no limitation, you can perfectly define

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

with dependencies between indices.

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?

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.

Dybjer has written multiple papers for MLTT, example https://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf. I remember similar papers exist for CIC...

But I'm no expert and I'm not sure how much those would count for your question

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

From my experience they are close to this paper about Parallel reduction by Takahashi: https://www.sciencedirect.com/science/article/pii/S0890540185710577

While What I was looking for is real step by step proof paper like Chapter 4 here:

https://www.ps.uni-saarland.de/Publications/documents/Schaefer_2019_Engineering.pdf

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)

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.

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.

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?

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.

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

@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 ?

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.

Karl Palmskog said:

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

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 :)

Last updated: May 18 2024 at 10:02 UTC