[Agda] Datatype parameters and indices

[Darryl]

There's also a perspective on this that one can take from the Elims. For P the elim should be something like

Elim-P : (A : Set) (M : P A -> Set)
          -> (base : (a : A) -> P (pack a))
          -> (p : P A) -> M p

whereas for N

Elim-N : (A : Set) (M : (B : Set) -> N B -> Set)
          -> (base : (B : Set) -> (b : B) -> M B (packn b))
          -> (n : N A) -> M A n

The second one is obviously different. The motive and base cases are parametric on the value stored in the packing type, which will highly restrict their values. This just falls out of the parameter/index distinction formally: motives and inductive subproofs musthave as arguments everything the functors/constructors have as arguments, plus some additional stuff (additional recursive proofs).

- darryl


________________________________
 From: Andreas Abel <andreas.abel at ifi.lmu.de>
To: Jan Malakhovski <oxij at oxij.org> 
Cc: agda at lists.chalmers.se 
Sent: Friday, January 25, 2013 12:03 PM
Subject: Re: [Agda] Datatype parameters and indices
 
[This is a candidate for a FAQ.]

That P passes but N not is an artefact of data type declarations.

Parameters are actually *absent* from constructors, so pack is really

   pack : ?A -> P ?A

for ?A to be instantiated according to the context where pack occurs. 
The syntax

   pack {A = Nat} zero

is valid, but the instantiation of parameter of A to Nat should only 
regarded as a hint to the type checker, and not an actual setting of an 
argument of pack.

In contrast, packn actually expects a first argument of type Set, which 
is too big for type N : ... -> Set, so Agda complains.

Hope that helps,

Andreas

On 25.01.13 12:05 AM, Jan Malakhovski wrote:
> Hello everyone,
>
> A question that doesn't leave me for a while (like a year or so).
>
> If I remember right, a dozen of versions ago the following code did type check.
>
> ~~~~
> data P (A : Set) : Set where
>    pack : A → P A
>
> data N : Set → Set where
>    packn : {A : Set} → A → N A
> ~~~~
>
> Now it complains:
>
> ~~~~
> The type of the constructor does not fit in the sort of the
> datatype, since Set₁ is not less or equal than Set
> when checking the constructor packn in the declaration of N
> ~~~~
>
> I can't help but wonder about a justification for this.
> It is said that parameters transform into constructors' implicit arguments, but the code above makes me think that, strictly speaking, it isn't the case.
>
> Best regards,
>    Jan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
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/
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130126/6bda1c1e/attachment.html