[Agda] Why does this pass the positivity checker?

[Jesper Cockx]

I think Agda checks for each function definition whether it is (strictly)
positive in each of its arguments. The 'depth' of this check is not limited
AFAICT, but it is determined at the definition site of the function, not at
the use site. I've seen this used quite often for universe constructions
such as in your example.

-- Jesper

On Thu, Jul 19, 2018 at 1:15 PM, Neel Krishnaswami <nk480 at cl.cam.ac.uk>
wrote:

> Hello,
>
> I wrote the following bit of code, to experiment with generic programming.
>
>>
>> data _×_ (A B : Set) : Set where
>>    _,_ : A → B → A × B
>>
>>
>> data _+_ (A B : Set) : Set where
>>   inl : A → A + B
>>   inr : B → A + B
>>
>>
>> data Poly : Set₁ where
>>   K : Set → Poly
>>   _⊗_ : Poly → Poly → Poly
>>   _⊕_ : Poly → Poly → Poly
>>   Id : Poly
>>
>> [_] : Poly → Set → Set
>> [ K X ] A = X
>> [ p ⊗ q ] A = [ p ] A × [ q ] A
>> [ p ⊕ q ] A = [ p ] A + [ q ] A
>> [ Id ] A = A
>>
>> data μ (F : Poly) : Set where
>>   into : [ F ] (μ F) → μ F
>>
> and Agda accepted the declaration of μ. I was surprised by this -- did
> Agda look at the body of the definition of [_] to decide that every
> recursive occurrence was  positive? If so, how deeply does it look?
>
> --
> Neel Krishnaswami
> nk480 at cl.cam.ac.uk
>
> _______________________________________________
> 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/20180720/4fd93d64/attachment.html>