Pierre-Marie Pédrot said:

well, obviously you critically need dependent types to prove anything, but the point is that you should flee away from indexed types

The typical examples given in an introduction to dependent types such as vectors do really suck in practice. However I disagree that indexed types should be avoided all together. Take intrinsically typed syntax for example. This is a very expressive way of formalizing programming languages. I agree it is hard to set up and many real word (functional) languages don't quite fall into this category. But for the simply typed lambda calculus it can be done, and I find it very useful. You just can't write bad terms.

And sure dependent type theory doesn't fall into this pattern, but things like inductive-inductive and inductive-recursive types should allow for similar things.

intrinsically typed syntax

there are two ways to do that though, the inductive and the recursive one

the mathcomp people argue (with quite a bit of valid arguments) that the better way is the recursive one

@Pierre-Marie Pédrot what do you call "recursive intrisically typed syntax" ? I thought intrinsically typed syntax was essentially a way to present (inductive) typing derivations.

i.e. replace a derivation with a proof that the type-checking algorithm says it's well-typed

it requires more work upfront but then you get properties like irrelevance of the derivation for free

Isn't that approach called extrinsically typed since you are refining a "raw" term (+ context and type) with a proof that it is well-typed ?

@Ali Caglayan I think vectors are as good as intrinsically-typed syntax, _with proper support_ (like in Agda). But even that has significant issues…

some Agda people acknowledge the problem in papers about algebraic ornaments, but I’ve never understood ornaments, while math-comp’s approach seems to work better in general, and already lets you reuse list lemmas when working on their tuples, instead of reproving them.

the only advantage of indexed types seems when your program and the well-typedness proof are basically isomorphic, but it doesn’t seem worth the cost when they aren’t (as in Vector.snoc).

(of course, if you prefer Coq there’s Equations, but it’s not as ergonomic as Agda for a bunch of reasons, some about the UX some fundamental)

The biggest barrier to using indexed inductives in coq is inversion support basically. For a while we have been talking about the new `invert`

tactic, but that hasn't appeared. I've started to use Equations and it is starting to bridge this gap nicely.

I think one of the coolest use of (indexed) dependent types is Conor McBride's KIPLING: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.379.3169&rep=rep1&type=pdf

Since I learnt about Grothendieck's construction in category theory (which we should more strikingly call Grothendieck's correspondance by the way), I realized that this construction is pervasive. Applied to types, it says that `{B : Type & B -> A}`

and `A -> Type`

are isomorphic (from left to right, take `fun a => {x : B & f x = a}`

and from right to left, take `{ a & P a}`

and the first projection).

So, per se, this explains why `{l : list A & length l = n}`

and `Vector.t A n`

, i.e. the pair `(list A, length)`

and the predicate `Vector.t A`

are interchangeable.

I like to this also as a Church vs Curry view, or intrinsically vs extrinsically like @Kenji Maillard says, or type theory (where every data is intrinsically typed) vs set theory (where there is only one type, the raw type of sets, but sets come with specifications which implicitly type them).

The extrinsic approach allows a separation of concerns between the computational data and their specifications (which are meant to be hProp). Maybe, this separation of concerns is actually not so bad in practice, compared to, once the limits of decidable inference is reached, having to interleave data and explicit hProp proofs.

As another example, do we manipulate type theory itself in the syntax of Categories of Families (which can be seen as an intrinsic form of type theory) or do we prefer to write proofs in the type theory which we know (where we manipulate only rawterms in practice)?

Or when we manipulate expressions on real numbers, do we care about `u`

being non zero in a complex expression mentioning `t/u`

or do we only care that `u`

is non zero when proving properties of the expression?

In any case, I'd like to be optimistic and that, eventually, proof assistants, or their UI, will be able to freely switch between Church-style proving and Curry-style proving, being able to offer a view similar to Agda even if the implementation is à la Curry, or a set-theoretic view even if the implementation is à la Church, since, after all, there are canonical transformations from one view to the other (as the work on intrinsic/extrinsic type theory, or the works on the initiality conjecture in type theory, or the works on interpreting inductive-inductive types by means of only inductive types show).

Ali Caglayan said:

The biggest barrier to using indexed inductives in coq is inversion support basically. For a while we have been talking about the new

`invert`

tactic, but that hasn't appeared. I've started to use Equations and it is starting to bridge this gap nicely.

The new `invert`

tactic is actually making progress thanks to Thierry Martinez who applied the techniques of compilation of dependent pattern-matching (i.e. Agda/Equations style of pattern-matching) to the compilation of (dependent) `match`

.

Hugo Herbelin said:

The new

`invert`

tactic is actually making progress thanks to Thierry Martinez who applied the techniques of compilation of dependent pattern-matching (i.e. Agda/Equations style of pattern-matching) to the compilation of (dependent)`match`

.

Any idea when we will be able to get our hands on it?

Basically, "dependent pattern-matching" (as formulated by Coquand in 1992) is now known to be compiled to CIC `match`

in three different ways:

- using JMeq-based Goguen-McBride-McKinna algorithm (possibly requiring K),
- using Cockx-Devriese-Piessens algorithm based on homogeneous telescopic equality (not requiring K), which is the algorithm used in Equations if I'm not mistaken (though beforehand, it might have been based on Goguen-McBride-McKinna's algorithm?),
- using Monin's small inversion, as explored by Boutillier, but also by Meven Bertrand (probably also related to Chlipala's convey patterns that I don't know well).

Per se, each of these methods could be applied to compile the general dependent form of Coq's `match`

with multiple nested patterns in indexed types. For instance, Equations algorithm could be used in principle to compile `match`

and thus to produce an `invert`

tactic.

Any idea when we will be able to get our hands on it?

I'd be afraid to promise something yet. An implementation started two years ago which is debugging stage. Note also that at the current time, there is no `invert`

tactic. There is only a `match`

compiler based on small inversion. Once this compiler is available, `invert`

can be simulated using a `refine`

. Here is a short example using Equations:

```
From Equations Require Import Equations.
(* Toy language of expressions *)
Inductive te : Type :=
| Te_const : nat -> te
| Te_plus : te -> te -> te
| Te_div0 : te -> te.
Inductive val : Type :=
| Nval : nat -> val
| Bval : bool -> val.
(* Evaluation *)
Inductive eval : te -> val -> Type :=
| E_Const : forall n,
eval (Te_const n) (Nval n)
| E_Plus : forall t1 t2 n1 n2,
eval t1 (Nval n1) ->
eval t2 (Nval n2) ->
eval (Te_plus t1 t2) (Nval (n1 + n2)).
Derive NoConfusion Subterm for te.
Derive NoConfusion Subterm for val.
Equations test_ev1 v (H: eval (Te_plus (Te_const 1) (Te_const 0)) v) : v = Nval 1 :=
test_ev1 v (E_Plus t1 t2 n1 n2 (E_Const n1) (E_Const n2)) := eq_refl.
```

By working at the level of an anonymous `match`

rather than at the level of a toplevel function, this could be replaced by a `refine`

(and thus used at arbitrary positions in a proof):

```
Lemma test_ev1 v (H: eval (Te_plus (Te_const 1) (Te_const 0)) v) : v = Nval 1.
Proof.
refine (match H with E_Plus t1 t2 n1 n2 (E_Const n1) (E_Const n2) => eq_refl end).
Qed.
```

To get an `invert`

, one would then need to find the larger patterns that expose the variables of the goal out of the indices of the hypothesis under consideration.

Note that this does not answer the limitations of dependent types mentioned in the thread as this will not provide more automatisation of inversion than in Agda.

Last updated: Feb 06 2023 at 13:03 UTC