[Agda] Why does this pass the positivity checker?

[Neel Krishnaswami]

Hello,

Is there any way to annotate the type signature with positivity 
information? It would be helpful for localizing errors, and for doing 
ML-style modular programming.

Thanks for your help!


On 20/07/18 13:06, Jesper Cockx wrote:
> 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
>>

-- 
Neel Krishnaswami
nk480 at cl.cam.ac.uk