<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> </div><div>- darryl</div></span></div><div></div><div> </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 <andreas.abel@ifi.lmu.de><br> <b><span style="font-weight: bold;">To:</span></b> Arseniy Alekseyev <arseniy.alekseyev@gmail.com>; Agda mailing list <agda@lists.chalmers.se> <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. 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. 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>> I have the following example, which does not work:<br>><br>> module test (A B : Set) where<br>><br>> data U : Set where<br>> a b : U<br>><br>> [_] : U → Set<br>> [_] a = A<br>> [_] b = B<br>><br>> f : ∀ u → [ u ] → U<br>> f u _ = u<br>><br>> postulate x : A<br>><br>> zzz = f _ x<br>><br>> Here we
have unresolved meta on the last line.<br>> When we change A and B to be constructors with a data keyword (or<br>> postulates), the meta gets resolved. It gets resolved because the<br>> function [_] becomes constructor-headed (A and B become different<br>> constructors).<br>><br>> Does it make sense to treat rigid variables, such as A and B in the<br>> example the same way constructors are treated? Why not?<br>><br>> A related, but separate issue:<br>> http://code.google.com/p/agda/issues/detail?id=796<br>><br>> Cheers!<br>> Arseniy<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>Andreas Abel <><
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>