[Agda] Argument order, universes and erasability

Pierre-Evariste Dagand dagand at cis.strath.ac.uk
Mon Oct 14 13:35:39 CEST 2013

> 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

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

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



More information about the Agda mailing list