[Agda] Argument order, universes and erasability

[Dan Doel]

On Sun, Oct 13, 2013 at 10:59 AM, Mathijs Kwik <mathijs at bluescreen303.nl> 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.
> Now, I have some understanding of Russell's paradox, and Set-in-Set
> problems, so I understand why a List of Sets becomes Set1 itself. But
> I don't see why this would apply to Vec if it's indexed with one
> instead of parameterized. It's still just _a Set_, not Set itself.
> What's the logic behind this?

The reason it becomes large is because the constructors change:

    data Vec : Set -> Nat -> Set1 where
      nil : {A : Set} -> Vec A 0
      _::_ : {A : Set} {n : Nat} -> A -> Vec A n -> Vec A (suc n)

There are now Set arguments to the constructors, and they can actually
be projected out. Having Vec be in Set would make it an impredicative,
strong sum, which allows you to write paradoxes. For instance, the
type:

    data Bad : Set where
      bad : Set -> Bad

is bad because Bad : Set, but Bad also contains all Sets.

Bad is a bit different than Vec, but the rules that stop you from
writing Bad also stop you from writing Vec, and I'm not sure that Vec
is safe anyway, unless you put additional restrictions on what you can
do with it, which Agda doesn't have.

> But speaking of dynamic stuff: how far is Agda able to erase type
> information when compiling? I understand this might be very tricky. If
> I only use indexes to guard myself from making mistakes (tracking
> meta-info), I would like all that to be erased from runtime. For
> example:
>
> test1 : forall {n} -> Vec Nat n -> Nat
> test1 v = head (v ++ (0 :: []))
>
> In this case I really don't care about n at runtime, but vectors still
> guard me from applying head to something empty at compile-time.
> While in this example:
>
> length1 : forall {n A} -> Vec A n -> Nat
> length1 [] = zero
> length1 (x :: xs) = succ (length1 xs)
>
> length2 : forall {n A} -> Vec A n -> Nat
> length2 {n} v = n
>
> I would expect length1 to have an erasable n (at the cost of
> traversing the vector to get its length), while length2 would have a
> runtime Nat associated with it.
> Am I correct in this assumption? Or is reality far more complicated? :)

There is work related to Agda's erasure annotations that would allow
you to write something like:

    length1 : forall {A .n} -> Vec A n -> Nat
    length1 [] = zero
    length1 (x :: xs) = succ (length1 xs)

which would specify that the n argument could be erased, since it is
only used inside type ascriptions (which are also erased). However,
there are some issues that still haven't been solved (I think) working
this into Agda. So for the time being, I don't think that the argument
would actually get erased.

-- Dan