9
$\begingroup$

I was wondering if the order of declarations of an inductive type can matter.

For example in Coq you can define Nat either by:

Inductive Nat :=
  | O : Nat
  | S : Nat -> Nat.

or

Inductive Nat :=
  | S : Nat -> Nat
  | O : Nat.

This will perhaps change the order of the parameters in the automatically generated eliminator, but that’s not a big deal.

What I’m wondering is if it is possible to write a declaration like

Inductive typewhereordermatters :=
  | cons1 : type1
  | cons2 : type2.

where type2 is a dependent type, depending on cons1? (and in this case, write the declarations in the other order would not have any meaning, because type2 would be referring to cons1 which does not exists yet).

$\endgroup$
9
$\begingroup$
  1. The order does not matter. I cannot think of a case where it would. As Andrej Bauer points out in a comment, if you change the order the result is canonically isomorphic to the original.

  2. One case cannot depend on another case. The elements of the sum represent a choice, so it doesn't make sense that the choice taken depends upon a choice that is not taken.

$\endgroup$
  • 2
    $\begingroup$ You can be more specific about your first point. The order does not matter. If you change the order the result is canonically isomorphic to the original. $\endgroup$ – Andrej Bauer May 14 '11 at 8:45
  • 2
    $\begingroup$ @Dave: Thanks! I was asking this question because of (the highly experimental theory of) higher inductive types, where this phenomena seems to happen, and I wanted to know whether this can also be the case with regular inductive types. $\endgroup$ – Guillaume Brunerie May 14 '11 at 9:27
  • 1
    $\begingroup$ @Guillaume: I'm not sure what phenomenon you are pointing to with the link. The different constructor clauses of a datatype definition cannot depend on each other, whether or not it is a higher-order datatype. Perhaps you are thinking of dependent records (which are used at the link, and are available in Agda and in Coq)? $\endgroup$ – Noam Zeilberger May 14 '11 at 11:55
  • 1
    $\begingroup$ @Noam: In the example of the higher inductive type circle, the type of the loop constructor depends on the base constructor. $\endgroup$ – Guillaume Brunerie May 14 '11 at 12:04
  • 2
    $\begingroup$ @Guillaume: I see now (they are introducing an experimental syntax), don't know how I missed that. $\endgroup$ – Noam Zeilberger May 14 '11 at 13:10
6
$\begingroup$

Does the order matter in the way you ask? No.

But is the order completely irrelevant to the functioning of the proof assistant? Again, no. In Matita, a proof assistant very similar to Coq, the order in which constructors are written in an inductive definition does matter for type checking, specifically when type checking a match expression.

Matita first has to check that all constructors are being matched against in the body of the match. It does this by cycling through the constructors in the order in which they are declared. Then, it comes to type check the match expression proper, which happens in reverse order, checking the case for the last declared constructor first. This type is then carried forth and used to check the other cases.

This very often shows up when writing a large match expression. You'd like to fill in the easy cases first, leaving harder cases under a wildcard, periodically type checking what you have written to make sure it makes sense. Sometimes Matita is unable to infer the type of the incomplete match expression but will quite happily do so if you fill in the case for the last constructor defined in the inductive type.

I presume, though I'm not certain, that Coq does something similar.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.