<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span><div><span>Doesn't this make it every so slightly possible to violate parametricity?</span></div><div></div><div>&nbsp;</div><div>- darryl</div></span></div><div></div><div>&nbsp;</div><div>- darryl<br></div>  <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <font size="2" face="Arial"> <hr size="1">  <b><span style="font-weight:bold;">From:</span></b> Andreas Abel &lt;andreas.abel@ifi.lmu.de&gt;<br> <b><span style="font-weight: bold;">To:</span></b> Arseniy Alekseyev &lt;arseniy.alekseyev@gmail.com&gt;; Agda mailing list &lt;agda@lists.chalmers.se&gt; <br> <b><span style="font-weight: bold;">Sent:</span></b> Monday, February 18, 2013 6:13 PM<br> <b><span style="font-weight:
 bold;">Subject:</span></b> Re: [Agda] Can rigid variables be treated as constructors/postulates?<br> </font> </div> <br>
That could be debated.&nbsp; Opinions?<br><br>A consequence of this relaxation would be that injectivity is not <br>stable under module instantiation, so it has to be recomputed when <br>'test' is applied to concrete sets A and B.&nbsp; However, other properties <br>are also recomputed at that point, for instance, polarity <br>(=monotonicity) and the compiled clauses.<br><br>Cheers,<br>Andreas<br><br>Am 18.02.2013 15:57, schrieb Arseniy Alekseyev:<br>&gt; I have the following example, which does not work:<br>&gt;<br>&gt;&nbsp; &nbsp;  module test (A B : Set) where<br>&gt;<br>&gt;&nbsp; &nbsp;  data U : Set where<br>&gt;&nbsp; &nbsp; &nbsp;  a b : U<br>&gt;<br>&gt;&nbsp; &nbsp;  [_] : U → Set<br>&gt;&nbsp; &nbsp;  [_] a = A<br>&gt;&nbsp; &nbsp;  [_] b = B<br>&gt;<br>&gt;&nbsp; &nbsp;  f : ∀ u → [ u ] → U<br>&gt;&nbsp; &nbsp;  f u _ = u<br>&gt;<br>&gt;&nbsp; &nbsp;  postulate x : A<br>&gt;<br>&gt;&nbsp; &nbsp;  zzz = f _ x<br>&gt;<br>&gt; Here we
 have unresolved meta on the last line.<br>&gt; When we change A and B to be constructors with a data keyword (or<br>&gt; postulates), the meta gets resolved. It gets resolved because the<br>&gt; function [_] becomes constructor-headed (A and B become different<br>&gt; constructors).<br>&gt;<br>&gt; Does it make sense to treat rigid variables, such as A and B in the<br>&gt; example the same way constructors are treated? Why not?<br>&gt;<br>&gt; A related, but separate issue:<br>&gt; http://code.google.com/p/agda/issues/detail?id=796<br>&gt;<br>&gt; Cheers!<br>&gt; Arseniy<br>&gt; _______________________________________________<br>&gt; Agda mailing list<br>&gt; <a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br>-- <br>Andreas Abel&nbsp; &lt;&gt;&lt;&nbsp; &nbsp;
  Du bist der geliebte Mensch.<br><br>Theoretical Computer Science, University of Munich<br>http://www.tcs.informatik.uni-muenchen.de/~abel/<br>_______________________________________________<br>Agda mailing list<br><a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br><br> </div> </div>  </div></body></html>