[Agda] general question

[Peter Dybjer]

Yes, let me just confirm Ondrej's answer Martin's question. The distinction between parameters and indices go back to my old papers on schemata for inductive families (and to an analogous distinction in CIC). See 

@article{dybjer:facs,
author  = "Peter Dybjer",
title   = "Inductive Families",
journal = "Formal Aspects of Computing",
volume  = 6,
pages   = "440-465",
year    = 1994}

@incollection{DybjerP:indsfm,
author  = "Peter Dybjer",
booktitle = "Logical Frameworks",
title   = "Inductive sets and families in {Martin-L{\"o}f's} Type Theory
       and their set-theoretic semantics",
year    = 1991,
publisher = "Cambridge University Press",
editor  = "Gerard Huet and Gordon Plotkin",
pages   = "280-306"}

The set-theoretic semantics in the latter paper makes use this distinction. Agda does not implement exactly these schemata, but something more general. 

Peter

________________________________________
From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of Ondrej Rypacek [ondrej.rypacek at gmail.com]
Sent: Tuesday, May 03, 2011 1:13 PM
To: Martin Escardo; Agda mailing list
Cc: Dominique Devriese
Subject: Re: [Agda] general question

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
>
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda