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

[Andreas Abel]

Giving the parameters to a data type first, as in

   data D (ParamContext) : IndexContext -> Set

has several practical advantages:

   - the parameters can easily receive their special treatment in 
constructors types, as their is:

   * they are hidden
   * they are absent in pattern matching, because they are determined
     by the type of the match

   - the syntax yields the same result as

       module M (ParamContext) where

         data D : IndexContext -> Set ...

     thus, giving parameters is a special form of the LEGO/Coq Section / 
Agda module mechanism

   - the user distinguishes parameters by himself, so the system only 
needs to check that parameters are not used as indices

However, it is not unthinkable to allow more flexibility.  For instance, 
in Idris you can write

   Vec : Nat -> Set -> Set
     nil  : Vec 0 A
     cons : A -> Vec n A -> Vec (suc n) A

and the system finds out by itself that A used as a parameter only.

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?

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/