[Agda] Why does this pass the positivity checker?

[Jesper Cockx]

Currently there is no way to do that, (partly) because positivity
information is not stored in the type of a function. There has been talk of
integrating this into the type system, but it's not clear at the moment how
to do this in a nice way.

One special case are the polarity pragma's that can be used to assign a
given polarity to a postulate, see
https://github.com/agda/agda/blob/master/test/Succeed/Polarity-pragma.agda.

-- Jesper

On Fri, Jul 20, 2018 at 2:24 PM, Neel Krishnaswami <nk480 at cl.cam.ac.uk>
wrote:

> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180720/32b3336e/attachment.html>