Parameters and indices [Re: [Agda] general question]

[Ondrej Rypacek]

On 5 May 2011 08:24, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>
> To get to a less "magic" treatment of parameters in constructor types, we
> need to semantically solve the nature of parameter quantification first,
> imho.  Meaning, what makes the quantification over A in the constructor type
>
>  nil : forall {A} -> Vec 0 A
>
> parametric?
>

Interesting.
Perhaps it has to do with the fact that Vec is a monoid homomorphism
from (Nat, suc , zero) to (Set -> Set , cons, nil) ?

Cheers,
Ondrej



> Cheers,
> Andreas
>
>
> On 03.05.11 1:23 PM, Peter Dybjer wrote:
>>
>> 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).
>>
>> 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
>
>>
>>
>> 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.
>>
>> On 3 May 2011 11:58, Dominique Devriese
>>>
>>> 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.
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>