<div dir="ltr"><div>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.<br></div><div><br></div><div>One special case are the polarity pragma's that can be used to assign a given polarity to a postulate, see <a href="https://github.com/agda/agda/blob/master/test/Succeed/Polarity-pragma.agda">https://github.com/agda/agda/blob/master/test/Succeed/Polarity-pragma.agda</a>.</div><div><br></div><div>-- Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jul 20, 2018 at 2:24 PM, Neel Krishnaswami <span dir="ltr"><<a href="mailto:nk480@cl.cam.ac.uk" target="_blank">nk480@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello,<br>
<br>
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.<br>
<br>
Thanks for your help!<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
On 20/07/18 13:06, Jesper Cockx wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I think Agda checks for each function definition whether it is (strictly)<br>
positive in each of its arguments. The 'depth' of this check is not limited<br>
AFAICT, but it is determined at the definition site of the function, not at<br>
the use site. I've seen this used quite often for universe constructions<br>
such as in your example.<br>
<br>
-- Jesper<br>
<br>
On Thu, Jul 19, 2018 at 1:15 PM, Neel Krishnaswami <<a href="mailto:nk480@cl.cam.ac.uk" target="_blank">nk480@cl.cam.ac.uk</a>><br>
wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello,<br>
<br>
I wrote the following bit of code, to experiment with generic programming.<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
data _×_ (A B : Set) : Set where<br>
    _,_ : A → B → A × B<br>
<br>
<br>
data _+_ (A B : Set) : Set where<br>
   inl : A → A + B<br>
   inr : B → A + B<br>
<br>
<br>
data Poly : Set₁ where<br>
   K : Set → Poly<br>
   _⊗_ : Poly → Poly → Poly<br>
   _⊕_ : Poly → Poly → Poly<br>
   Id : Poly<br>
<br>
[_] : Poly → Set → Set<br>
[ K X ] A = X<br>
[ p ⊗ q ] A = [ p ] A × [ q ] A<br>
[ p ⊕ q ] A = [ p ] A + [ q ] A<br>
[ Id ] A = A<br>
<br>
data μ (F : Poly) : Set where<br>
   into : [ F ] (μ F) → μ F<br>
<br>
</blockquote>
and Agda accepted the declaration of μ. I was surprised by this -- did<br>
Agda look at the body of the definition of [_] to decide that every<br>
recursive occurrence was  positive? If so, how deeply does it look?<br>
<br>
--<br>
Neel Krishnaswami<br>
<a href="mailto:nk480@cl.cam.ac.uk" target="_blank">nk480@cl.cam.ac.uk</a><br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
</blockquote></blockquote>
<br></div></div><span class="HOEnZb"><font color="#888888">
-- <br>
Neel Krishnaswami<br>
<a href="mailto:nk480@cl.cam.ac.uk" target="_blank">nk480@cl.cam.ac.uk</a><br>
<br>
</font></span></blockquote></div><br></div>