[Agda] general question

[Ondrej Rypacek]

Hi Martin,

I think the difference is semantical rather then just syntactical.
Although it is true that

Vec : (A : ℕ → Set) →  ℕ → Set

is the type of  matrices of Sets, indexed by (ℕ → Set) x ℕ, the definition

data Vec (A : ℕ → Set) : ℕ → Set where
 [] : Vec A O
 _::_ : {n : ℕ} → A n → Vec A n → Vec A (succ n)


defines one column in it for each A fixed throughout the definition.
data Vec (n : ℕ) :  (ℕ → Set) → Set where
...

would define one line, for each n: N and (ℕ → Set) variable. None of
these alone define the whole matrix, thus you cannot flip at will and
turn a parameter into a index. You'd need to define

data Vec : (A : ℕ → Set) →  ℕ → Set where
....


or an A -> Nat indexed collection of the former, or an Nat indexed
collection of the latter to make the situation symmetrical.


Hope this helps.
Best,
Ondrej


On 3 May 2011 11:58, Dominique Devriese
<dominique.devriese at cs.kuleuven.be> wrote:
> Martin,
>
> 2011/5/3 Martin Escardo <m.escardo at cs.bham.ac.uk>:
>> Dominuqe, thanks. Yes, I can do this.
>>
>> But what is, in the syntax of the data declaration, forcing me to have A
>> first? And why?
>
> I guess this is related to the distinction between data type indices
> and parameters in Agda data definitions. I don't immediately find a
> good reference, but other people on this list will be able to explain
> this, I think.
>
> Dominique
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>