[Agda] Argument order, universes and erasability

[wren at freegeek.org]

On 10/14/13 6:48 PM, Andreas Abel wrote:
> On 13.10.2013 20:53, Dan Doel wrote:
>> On Sun, Oct 13, 2013 at 10:59 AM, Mathijs Kwik wrote:
>>> I tried to declare `Vec n A` with agda as well, but because agda 
>>> makes
>>> this clear distinction between parameters and indexes, this meant I
>>> had to make the Set parameter into an index, which forces `Vec n A` 
>>> to
>>> become Set1.
>
> Idris gives up on the "parameter first, then indices" order and does
> some analysis instead.  I think Agda should follow Idris' lead 
> here...

As others've suggested, there are two issues at hand here:

#1) In principle there need be no distinction between `Vec n A` and 
`Vec A n`. It's only because of a restriction on the syntax of defining 
data types that Agda (and Coq) treats them differently.

#2) As a side-effect of the syntactic restriction, if you try to define 
`Vec n A` as a data type then it ends up living in Set1. Of course, we 
want things _indexed_ by Set0 to live in Set1; but there's no 
non-syntactic reason to consider `Vec n A` to be indexed by Set0.

The current workarounds are either to suffer through the `Vec A n` 
definition, or to define an auxiliary function `Vec n A` which just 
reorders the arguments to the data type definition.

-- 
Live well,
~wren