10
$\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).

Improve this question
$\endgroup$
0

3 Answers 3

Reset to default
11
$\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.

Improve this answer
$\endgroup$
9
  • 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, 2011 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, 2011 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, 2011 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, 2011 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, 2011 at 13:10
7
$\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.

Improve this answer
$\endgroup$
0
$\begingroup$

It matters once you have higher inductive types. Consider the following example (Agda):

data S¹ : Set where
  base : S¹
  loop : base ≡ base

Changing the order will make loop impossible to see base.

EDIT: there is an interesting conversation in the comments below, which defines how 'does not matter' the order is.

Improve this answer
$\endgroup$
9
  • $\begingroup$ It still does not matter. An inductive type or a HIT does not "come into existence in successive steps". You need to read the definition as a whole, describing the overall structure of the type. It is convenient but not necessary that the path constructors are listed after the point constructors. $\endgroup$
    – Andrej Bauer
    Sep 25, 2021 at 8:03
  • $\begingroup$ @AndrejBauer I would say that this is just a different perspective and it doesn't make much sense. For instance, I would say the order of fields in a dependent record matters as the type checking of the fields depends on the order they're declared, but I can also say we must look at the record as a whole, so order doesn't matter. If field1's type depends on field2, it's convenient but not necessary that field1 is listed after field2. But in this perspective, order never matters, and it makes no sense to talk about orders at all. $\endgroup$
    – ice1000
    Sep 25, 2021 at 8:18
  • 1
    $\begingroup$ I am not sure what you are saying. But to keep things concrete, let's consider simple inductive types. A data T : Set where 〈clauses〉 construct is a presentation of a polynomial functor $P$, and $T$ is the initial $P$-algebra. Switching around the order in 〈clauses〉 results in a canonically isomorphic $P'$ and hence in a canonically isomorphic initial $P$-algebra. In this sense the order of the clauses does not matter. 1/3 $\endgroup$
    – Andrej Bauer
    Sep 25, 2021 at 8:35
  • $\begingroup$ In a definition of a dependent record type the fields are clearly ordered, because they are given as a list again. Assuming they do not refer to each other in a cyclic way, we may reconstruct a well-founded order on the fields. Any linearlization of that well-founded order then determines one way of forming the record type as a series of nested dependent sums (a telescope). These will all be canonically isomoprhic again. (However, I agree that it is convenient both for humans and algorithms to reqiure that each field refer only to the previous ones.) 2/3 $\endgroup$
    – Andrej Bauer
    Sep 25, 2021 at 8:38
  • 1
    $\begingroup$ As I tried to emphasize, but apparently not enough, there is an order of fields in the syntactic presentation of the type, and that order both makes sense and does not matter – in the sense explained above. And please do not confuse the definition of HITs with one particular way of constructing them from simpler HITs (coproducts and pushouts). It's the same with record types: they may be constructed as nested dependent sums, but need not, we can also give a direct definition of what they are. $\endgroup$
    – Andrej Bauer
    Sep 25, 2021 at 8:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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