[Agda] Inductive indexing

[Dan Doel]

Hello,

Not too long ago, I was looking at the Idris[1] home page, and decided that 
translating the type preserving interpreter program there to Agda might be a 
good exercise. Everything worked out all right, but along the way, I had to 
work through a bit of a snag, and thought I'd ask here to make sure that I 
didn't miss some better solution.

The crux of the matter is this type in the Idris version:

  data Env : (xs : Vect Ty n) -> # where
      Empty  : Env VNil
    | Extend : {xs : Vect Ty n} -> (interpTy t) -> (Env xs) ->
               (Env (VCons t xs));

My first attempt at translating this to Agda went something like:

  data Env {n : Nat} : Vect Type n -> Set where
    Empty  : Env []
    Extend : forall {t ts} -> ↑ t -> Env ts -> Env (t :: ts)

Where ↑ : Type -> Set. However, this fails, because n is some arbitrary, fixed 
natural, so '[] : Vect Type n' doesn't necessarily hold, for example. To 
allow for a parameter to vary, we can't give it a name; for instance, 
the 'Vect Type n' isn't given a name. So, one might proceed to try:

  data Env : Nat -> ...

But, we're stuck there, because the vector depends on the value of the 
natural. I eventually worked out the following encoding:

  data Env : (Σ Nat (Vect Type)) -> Set where
    empty : Env (0 , [])
    push  : {t : Type}{n : Nat}{ts : Vect Type n}
               -> ↑ t -> Env (n , ts) -> Env (suc n , t :: ts)

Which works fine, of course, but it's rather more verbose than what one might 
hope for. Vectors know their own size, so having to specify again that the 
length of the null vector is 0 seems redundant.

I suppose in general, the situation is that we have an inductive family F1 
indexed by F2, which is itself an inductive family indexed by I, and in 
practice, instead of just indexing F1 by F2, we need to index by Σ I F2.

Anyhow, as I said, this isn't really a problem, as the solution I arrived at 
is bearable. But I was wondering if anyone else had come across this (it 
doesn't seem like too exceptional a situation), and if so, did they come up 
with something nicer than I did.

My thanks for your time and help.
-- Dan Doel

[1]: http://www.cs.st-and.ac.uk/~eb/Idris/