<div dir="ltr"><div>Not an implementor, but I&#39;ll add my explanation.</div><div><br></div>On Fri, May 24, 2013 at 12:37 AM, Martin Escardo <span dir="ltr">&lt;<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>&gt;</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&#39;s the same as desugaring the \() manually, hence it&#39;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&#39;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&#39;t, unless \() is replaced by y.</blockquote>
<div> </div><div>Its use won&#39;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&#39;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 &quot;name&quot;.</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 &quot;eta expansion&quot; 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&#39;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 &lt;<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>&gt;:<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&#39;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 &quot;absurd&quot;. But then the<br>
resulting expression doesn&#39;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&#39;t manage to distil a simple instance of this to reproduce here. But<br>
if you are brave enough, you can search for &quot;AGDA PROBLEM&quot; 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>