<div dir="ltr"><div>Not an implementor, but I'll add my explanation.</div><div><br></div>On Fri, May 24, 2013 at 12:37 AM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br>
<div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div>
[...]</div>
However, my first, original, definition of y:Y was<br>
<br>
y : Y<br>
y ()<br></blockquote><div><br></div><div>That's the same as desugaring the \() manually, hence it'll get the same results.</div><div><br></div><div>In general functions defined by pattern matching, including absurd ones, are compared by name like lambda-bound variables would. Being defined with the same structure doesn't matter.</div>
<div> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
If you replace that in the link I give below, the Agda file still type-checks. But we still have the problem I mentioned, that a definition of something using \() type checks, but its uses don't, unless \() is replaced by y.</blockquote>
<div> </div><div>Its use won't typecheck because you are trying to use a theorem that talks about y to prove something about a definition using \() and they are not equal because they are not compared structurally. It's more surprising for the case where you use \() in both places, but each use of \() gets desugared into its own definition so each one gets a distinct "name".</div>
<div> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div>[...]</div>
BTW, Agda has a lot of "eta expansion" I mentioned in a previous message. You seem to be saying that my problem is a lack of absurd eta. But I am saying I don't necessarily see this as the problem. Further clarification by the Agda implementors would be really appreciated here.<br>
<br></blockquote><div><br></div><div>Indeed, a more structural equality for pattern-matching definitions, like in PiSigma [1], should also solve this, as proposed in another thread [2] about the same problem, but in the context of coinduction.</div>
<div>
<br></div><div>[1] <a href="http://www.cs.nott.ac.uk/~txa/publ/pisigma-new.pdf" target="_blank">http://www.cs.nott.ac.uk/~txa/publ/pisigma-new.pdf</a><br></div><div>[2] <a href="https://lists.chalmers.se/pipermail/agda/2010/002573.html">https://lists.chalmers.se/pipermail/agda/2010/002573.html</a></div>
<div><br></div><div style>Cheers, </div><div style> Andrea.</div><div style><br></div><div style><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Best,<br>
Martin<div><div><br>
<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Guillaume<br>
<br>
2013/5/23 Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>>:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
I have a problem with absurdity in Agda, which I can solve in an undesirable<br>
way, which forces me to change several definitions.<br><br>
I would like to both understand what the problem is, and why the desirable<br>
way doesn't work.<br>
<br>
I have three types X,Y,Z, whose definition I omit here. I can define, using<br>
absurd patterns,<br>
<br>
x : X<br>
x = \a ()<br>
<br>
y : Y<br>
y : \()<br>
<br>
z : Z<br>
z : \()<br>
<br>
These are types which have a parameter n:N that happens to be zero and so<br>
they trivialize in this special case, as they have occurrences of Fin n in<br>
their definitions.<br>
<br>
Now I have three holes in a definition (of a fourth type), reported to have<br>
types X,Y,Z. I can fill the holes with x,y,z, and the definition<br>
type-checks.<br>
<br>
But if I instead fill the holes with \a (), \(), and \(), expanding the<br>
definitions of x,y,z, then type-checking fails.<br>
<br>
Moreover, if just one of the three holes is filled with the corresponding<br>
term, type checking still fails.<br>
<br>
Additionally, if I ask the emacs interface to fill the wholes with ctrl-c-a,<br>
this succeeds, with expressions containing the string "absurd". But then the<br>
resulting expression doesn't type check.<br>
<br>
And there is a more annoying fact. I have previous definition of something<br>
else that uses \() and does type check. However, when I use it, things fail.<br>
I instead need to use the same definition with replaced \() by y.<br>
<br>
This is very mysterious to me.<br>
<br>
I didn't manage to distil a simple instance of this to reproduce here. But<br>
if you are brave enough, you can search for "AGDA PROBLEM" in any of the two<br>
following links:<br>
<br>
<a href="http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.html" target="_blank">http://www.cs.bham.ac.uk/~mhe/<u></u>dialogue/dialogue-lambda.html</a><br>
<a href="http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.lagda" target="_blank">http://www.cs.bham.ac.uk/~mhe/<u></u>dialogue/dialogue-lambda.lagda</a><br>
<br>
Help is appreciated.<br>
<br>
Martin<br>
______________________________<u></u>_________________<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" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></blockquote>
<br></div></div><span><font color="#888888">
-- <br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" target="_blank">http://www.cs.bham.ac.uk/~mhe</a></font></span><div><div><br>
______________________________<u></u>_________________<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" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div>