Stream: Coq users

Topic: Using indexed types

Ali Caglayan (Nov 28 2021 at 15:08):

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.

Ali Caglayan (Nov 28 2021 at 15:12):

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.

Pierre-Marie Pédrot (Nov 28 2021 at 15:13):

intrinsically typed syntax

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

Pierre-Marie Pédrot (Nov 28 2021 at 15:14):

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

Kenji Maillard (Nov 28 2021 at 15:17):

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

Pierre-Marie Pédrot (Nov 28 2021 at 15:49):

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

Pierre-Marie Pédrot (Nov 28 2021 at 15:49):

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

Kenji Maillard (Nov 28 2021 at 15:59):

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 ?

Paolo Giarrusso (Nov 28 2021 at 16:05):

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

Paolo Giarrusso (Nov 28 2021 at 16:07):

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.

Paolo Giarrusso (Nov 28 2021 at 16:09):

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

Paolo Giarrusso (Nov 28 2021 at 16:10):

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

Ali Caglayan (Nov 28 2021 at 16:51):

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.

Ali Caglayan (Nov 28 2021 at 16:53):

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

Hugo Herbelin (Nov 28 2021 at 16:56):

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

Hugo Herbelin (Nov 28 2021 at 16:58):

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.

Ali Caglayan (Nov 28 2021 at 17:04):

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?

Hugo Herbelin (Nov 28 2021 at 17:06):

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

Hugo Herbelin (Nov 28 2021 at 17:08):

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.

Hugo Herbelin (Nov 28 2021 at 17:35):

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: Oct 13 2024 at 01:02 UTC