[Agda] Inductive indexing

[Dan Doel]

On Thursday 03 April 2008, Wouter Swierstra wrote:
> Hi Dan,
>
> >  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:
>
> I think you are allowed to write:
>
>    data Env : (n : Nat) -> Vec n -> Set where
>      ...

Oh! Even better than that, you can do this:

  data Env : {n : Nat} -> Cxt n -> Set where
    empty : Env []
    push  : {t : Type}{n : Nat}{ts : Cxt n}
               -> ↑ t -> Env ts -> Env (t :: ts)

which is ideal! I thought that the dependent parts of the signature were 
always supposed to go to the left of the colon, but evidently there's some 
subtlety that I was missing. It seems that in

   data Foo (a : A) (b : B) : (c : C) -> (d : D) -> SetN where ...

a and b are fixed and arbitrary, like the parameters to an ordinary algebraic 
data type, whereas c and d are more like the paramaters to a GADT (if I may 
relate it to Haskell/GHC; that's what makes it an inductive family, I guess). 
Going back and looking at the wiki, this is all spelled out, but apparently I 
skimmed to fast, and only looked at the code samples my first time through, 
so I only have myself to blame.

Many thanks for the enlightenment.

-- Dan