[Agda] Argument order, universes and erasability

[gallais]

Hi,

There is no theoretical reason why you shouldn't be able to interleave
parameters and indices as long as the parameters are not allowed to
depend upon indices (which basically means that you could reorder them
to fit the current pattern). 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.

Cheers,

On 13/10/13 15:59, Mathijs Kwik wrote:
> Hi all,
>
> I have a bunch of questions, but I think they are somehow related.
>
> A little while ago, the idris standard library chose to swap the
> arguments for Vec from `Vec A n` to `Vec n A`. I did not really pay
> attention at the time, but a while later I found the paper "Hasochism:
> The Pleasure and Pain of Dependently Typed Haskell", which explores
> how far haskell can go already towards dependent types. This paper
> used `Vec n A` as well, which proved convenient when defining
> Traversable/Foldable/Functor instances for it. Are there any other
> advantages or disadvantages either way?
>
> 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?
>
> One reason I could think of myself is that it has to do with
> static/dynamic stuff. If for some reason all indexes are kept around
> dynamically, and initiated on construction (when creating a Vec at
> runtime), I can see how "something that keeps track of a Set" cannot
> be a Set by itself, but that sounds more like a technical issue, and
> I'm not at all sure if this is true.
>
> 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? :)
>
> Thanks,
> Mathijs
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>