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

[Ondrej Rypacek]

Apologies, I was talking nonsense, I don't know what came over me


But it IS a lax monoid homomorphism from (Nat, suc, zero) to
(Set->Set, (- x Id) , const \top)



Cheers,
Ondrej



On 5 May 2011 09:51, Ondrej Rypacek <ondrej.rypacek at gmail.com> wrote:
> 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/
>>
>