[Agda] Argument order, universes and erasability

[Pierre-Evariste Dagand]

> Pierre-Évariste Dagand had a formalization in Agda of a system
> allowing this increased liberality in datatype definitions but I
> don't quite remember whether it is available somewhere online or
> not.

Do I? :-)

I certainly have a few universes of datatypes in Agda that support
this style (e.g. IDesc in
[https://personal.cis.strath.ac.uk/pierreevariste.dagand/stuffs/thesis-2011-phd/model/html/Main.html]).

But there is nothing deep (or new) there: as Guillaume said, as long
as you forbid parameters to depend on indices, you can reorder them in
any way you like. For instance, you could define vectors the way Agda
allows them (Vec' below) and then define Vec the way you want (Vec
below):

data Vec' (A : Set) : Nat -> Set where (...)

Vec : (n : Nat)(A : Set) -> Set
Vec n A = Vec' A n


In the (infamous) Chapter 7 of my thesis
([https://personal.cis.strath.ac.uk/pierreevariste.dagand/#phd-thesis]),
I describe an "elaboration" of inductive definitions down to a
universe of datatypes (Section 7.2, not mechanised). In theory, my
syntax of inductive definitions allows the user to mix parameters and
indices (see Section 3.2.2 for an intro to the syntax). However, in
practice, it is significantly easier to treat parameters first and
indices second (Def. 7.37). I guess that the same pragmatism lead to
Agda's current design(?)



Cheers,

--
Pierre