[Agda] Difference between parameterized and indexed datatypes

[Ulf Norell]

The sort is not allowed to depend on an index to prevent you from defining
things like

  data D : (a : Level) -> Set a where
    c0 : D lzero
    c1 : D (lsuc lzero)
    _+_ : (a b : Level) -> D a -> D b -> D (a ⊔ b)

I don't know that having such definitions would break anything, but I also
have no idea
what they mean.

In principle the restriction could be relaxed to allow your definition, but
that would make
it more complex to implement and explain, and offer no tangible benefits.
We would
allow exactly those cases where the level could be made a parameter.

/ Ulf


On Thu, May 4, 2017 at 8:41 PM, v0id_NULL <igorzsci at gmail.com> wrote:

> Dear list,
>
> Help me please. I can not understand what difference between these
> definitions.
>
> data T1 {ℓ} : Set ℓ where
>  c1 : T1
>
> data T2 : {ℓ : _} → Set ℓ where
>  c2 : T2
>
> Why first one is approved but second one is rejected with error
> "The sort of T2 cannot depend on its indices in the type {ℓ :
> Agda.Primitive.Level} → Set ℓ when checking the definition of T2"?
>
> _______________________________________________
> 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/20170504/8d4e567c/attachment.html>