<p>Does the order matter in the way you ask?  No.</p>

<p>But is the order <em>completely</em> 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 <em>does</em> matter for type checking, specifically when type checking a match expression.</p>

<p>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.</p>

<p>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.</p>

<p>I presume, though I'm not certain, that Coq does something similar.</p>

CC BY-SA 3.0
2011-10-05T09:46:43.507Z
2011-10-05T09:46:43.507Z
Dominic Mulligan
<p>It matters once you have higher inductive types. Consider the following example (Agda):</p>
<pre><code>data S¹ : Set where
  base : S¹
  loop : base ≡ base
</code></pre>
<p>Changing the order will make <code>loop</code> impossible to see <code>base</code>.</p>
<p>EDIT: there is an interesting conversation in the comments below, which defines how 'does not matter' the order is.</p>

CC BY-SA 4.0
2021-09-25T08:03:54.270Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-09-25T08:18:47.823Z
@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.
ice1000
CC BY-SA 4.0
2021-09-25T08:35:18.297Z
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
Andrej Bauer
CC BY-SA 4.0
2021-09-25T08:38:04.950Z
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
Andrej Bauer
CC BY-SA 4.0
2021-09-25T08:39:50.503Z
The definition of a HIT is more like the case of an inductive type, with some resemblance to the dependent record type. In any case, the situation is analogous: the actual definition *presents* a (suitably generalized) functor $P$ by *listing* clauses in some order. Changing the order results in a canonically isomorphic $P'$. And this is the sense in which the "order does not matter". I hope that clarifies what I've tried to say. 3/3
Andrej Bauer
CC BY-SA 4.0
2021-09-25T08:44:07.677Z
@AndrejBauer If we think of canonically isomorphic types as 'the same type' (which, thanks to your clarification), then it makes no sense to talk about orders at all. Because it never matters. I think it's quite opinion-based (are uniquely isomorphic objects the same objects? I think the answer is no). OTOH, I would interpret dependent records as "sugared" sigma types, which is binary. So order matters. I think of HITs the same way -- generated by taking coproducts and pushouts, both binary.
ice1000
CC BY-SA 4.0
2021-09-25T08:46:32.960Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-09-25T08:50:46.193Z
Still, everything depends on the definition of 'does not matter' -- does it matter because it makes sense? Does it matter if from some perspective it makes no sense, but not all? I edited the answer to show that.
ice1000
CC BY-SA 4.0
2021-09-25T08:51:53.687Z
I am done discussing this, but I believe every single time I said "does not matter" I explained the sense in which it does not matter. I never used the phrase in such a way that it would be open to interpretation, and therefore your raising the issue seems misdirected.
Andrej Bauer
CC BY-SA 4.0
2021-09-25T05:15:47.263Z
2021-09-25T08:48:34.320Z
2021-09-25T08:48:34.320Z
ice1000
<ol>
<li><p>The order does not matter. I cannot think of a case where it would. As <a href="https://cstheory.stackexchange.com/users/705/andrej-bauer">Andrej Bauer</a> points out in a comment, <em>if you change the order the result is canonically isomorphic to the original</em>. </p></li>
<li><p>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.</p></li>
</ol>

CC BY-SA 3.0
2011-05-14T08:45:44.030Z
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.
Andrej Bauer
CC BY-SA 3.0
2011-05-14T08:52:18.307Z
Indeed. Will add that point to the answer.
Dave Clarke
CC BY-SA 3.0
2011-05-14T09:27:45.187Z
@Dave: Thanks! I was asking this question because of (the highly experimental theory of) higher inductive types, where this phenomena [seems to happen](http://homotopytypetheory.org/2011/04/29/a-formal-proof-that-pi1s1-is-z/), and I wanted to know whether this can also be the case with regular inductive types.
Guillaume Brunerie
CC BY-SA 3.0
2011-05-14T09:40:00.060Z
@Guillaume: That's certainly a very interesting link.
Dave Clarke
CC BY-SA 3.0
2011-05-14T10:53:32.880Z
If we think of definitions as a context free grammar, the context doesn't matter.
Vijay D
CC BY-SA 3.0
2011-05-14T11:55:50.310Z
@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](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records) and [in Coq](http://coq.inria.fr/doc/Reference-Manual004.html#toc14))?
Noam Zeilberger
CC BY-SA 3.0
2011-05-14T12:04:49.543Z
@Noam: In the example of the higher inductive type `circle`, the type of the `loop` constructor depends on the `base` constructor.
Guillaume Brunerie
CC BY-SA 3.0
2011-05-14T13:10:02.147Z
@Guillaume: I see now (they are introducing an experimental syntax), don't know how I missed that.
Noam Zeilberger
CC BY-SA 3.0
2011-05-16T15:46:07.770Z
Single point where order is matter is usages of builtin "if" operator for types with exactly two constructors.
Vag
CC BY-SA 3.0
2011-05-14T08:38:45.337Z
2011-05-14T08:53:47.243Z
2017-04-13T12:32:28.077Z
Dave Clarke
<p>I was wondering if the order of declarations of an inductive type can matter.</p>

<p>For example in Coq you can define <code>Nat</code> either by:</p>

<pre><code>Inductive Nat :=
  | O : Nat
  | S : Nat -&gt; Nat.
</code></pre>

<p>or</p>

<pre><code>Inductive Nat :=
  | S : Nat -&gt; Nat
  | O : Nat.
</code></pre>

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

<p>What I’m wondering is if it is possible to write a declaration like</p>

<pre><code>Inductive typewhereordermatters :=
  | cons1 : type1
  | cons2 : type2.
</code></pre>

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

<lo.logic><type-theory><coq><dependent-type>
Does the order of declarations in an inductive type matter?
Guillaume Brunerie
# Does the order of declarations in an inductive type matter?

(Asked by: username_0 on 2011-05-14)

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

**Tags:** lo.logic, type-theory, coq, dependent-type

---

## 3 answers

### Answer by username_4 on 2011-05-14. Score: 11 | Accepted answer

1. The order does not matter. I cannot think of a case where it would. As [Andrej Bauer](https://cstheory.stackexchange.com/users/705/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.

> **Comments:**
> **username_3**: 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.  
> **username_4**: Indeed. Will add that point to the answer.  
> **username_0**: @Dave: Thanks! I was asking this question because of (the highly experimental theory of) higher inductive types, where this phenomena [seems to happen](http://homotopytypetheory.org/2011/04/29/a-formal-proof-that-pi1s1-is-z/), and I wanted to know whether this can also be the case with regular inductive types.  
> **username_4**: @Guillaume: That's certainly a very interesting link.  
> **username_5**: If we think of definitions as a context free grammar, the context doesn't matter.  
> **username_6**: @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](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records) and [in Coq](http://coq.inria.fr/doc/Reference-Manual004.html#toc14))?  
> **username_0**: @Noam: In the example of the higher inductive type `circle`, the type of the `loop` constructor depends on the `base` constructor.  
> **username_6**: @Guillaume: I see now (they are introducing an experimental syntax), don't know how I missed that.  
> **username_7**: Single point where order is matter is usages of builtin "if" operator for types with exactly two constructors.  

---

### Answer by username_1 on 2011-10-05. Score: 7

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.


---

### Answer by username_2 on 2021-09-25. Score: 0

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.

> **Comments:**
> **username_3**: 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.  
> **username_2**: @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.  
> **username_3**: 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  
> **username_3**: 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  
> **username_3**: The definition of a HIT is more like the case of an inductive type, with some resemblance to the dependent record type. In any case, the situation is analogous: the actual definition *presents* a (suitably generalized) functor $P$ by *listing* clauses in some order. Changing the order results in a canonically isomorphic $P'$. And this is the sense in which the "order does not matter". I hope that clarifies what I've tried to say. 3/3  
> **username_2**: @AndrejBauer If we think of canonically isomorphic types as 'the same type' (which, thanks to your clarification), then it makes no sense to talk about orders at all. Because it never matters. I think it's quite opinion-based (are uniquely isomorphic objects the same objects? I think the answer is no). OTOH, I would interpret dependent records as "sugared" sigma types, which is binary. So order matters. I think of HITs the same way -- generated by taking coproducts and pushouts, both binary.  
> **username_3**: 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.  
> **username_2**: Still, everything depends on the definition of 'does not matter' -- does it matter because it makes sense? Does it matter if from some perspective it makes no sense, but not all? I edited the answer to show that.  
> **username_3**: I am done discussing this, but I believe every single time I said "does not matter" I explained the sense in which it does not matter. I never used the phrase in such a way that it would be open to interpretation, and therefore your raising the issue seems misdirected.  

---

