<div dir="ltr">The crucial point is that (\()) is not equal to (\()), so e.g. the ones appearing in the body of main-closed-ground' don't match the ones in its own type.<div><br></div><div style>To be concrete we can use a simplified version of what happens in main-closed-ground':</div>
<div style><br></div><div style>data Empty : Set where</div><div style>postulate<br></div><div style> X : Set</div><div style> P : (Empty -> X) -> Set</div><div style> lemma : (f : Empty -> X) -> P f</div>
<div style><br></div><div style>Given the context above we attempt to feed agda code using (\()):</div><div style><br></div><div style>main : P (\())<br></div><div style>main = lemma (\())</div><div style><br></div><div style>
Before we can check the type of main we have to translate (\()) away into toplevel definitions, because internally only those are allowed pattern-matching. But each use of (\()) is translated separately, so we get:</div><div style>
<br></div><div style>absurd1 : Empty -> X</div><div style>absurd1 ()</div><div style><br></div><div style>absurd2 : Empty -> X</div><div style>absurd2 ()</div><div style><br></div><div style>main : P absurd1</div><div style>
main = lemma absurd2</div><div style><br></div><div style>Now we can proceed typechecking and find that (lemma absurd2 : P absurd2), i.e. applications of lemma only care about the type of its argument, but for main to typecheck we need the type of the body (P absurd2) to equal the declared type (P absurd1), and so we'd need absurd2 = absurd1 which unfortunately we can't deduce because those are different definitions.</div>
<div style><br></div><div style><br></div><div style>Hope it helps,</div><div style> Andrea</div><div style><br></div><div style><br></div><div style><br></div><div style> </div></div><div class="gmail_extra"><br><br>
<div class="gmail_quote">On Fri, May 24, 2013 at 6:26 PM, 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><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Thanks for the explanation.<br>
<br>
I think I need to ditch pattern matching and work with the Fin eliminator instead, as Guillaume suggested.<br>
<br>
But I still don't understand why if I write<br>
<br>
blah (\())<br>
<br>
I get a type-checking error, whereas if I write<br>
<br>
blah y<br>
<br>
then things type check. Below you are saying they are different. Fair enough. But they should have the same type, and this should be enough to get blah going.<br>
<br>
What is more, "y" didn't exist, and I tried to fill "blah ?" with \() to no avail. Then I created y defined to be \(), and this was allowed to fill the gap.<br>
<br>
Anyway, I at least understand one of the two problems after Guillaume and your explanation.<br>
<br>
Thanks,<br>
Martin<div class="im"><br>
<br>
On 24/05/13 15:02, Andrea Vezzosi wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
Not an implementor, but I'll add my explanation.<br>
<br>
On Fri, May 24, 2013 at 12:37 AM, Martin Escardo<br></div><div><div class="h5">
<<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a> <mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>>> wrote:<br>
<br>
[...]<br>
However, my first, original, definition of y:Y was<br>
<br>
y : Y<br>
y ()<br>
<br>
<br>
That's the same as desugaring the \() manually, hence it'll get the same<br>
results.<br>
<br>
In general functions defined by pattern matching, including absurd ones,<br>
are compared by name like lambda-bound variables would. Being defined<br>
with the same structure doesn't matter.<br>
<br>
If you replace that in the link I give below, the Agda file still<br>
type-checks. But we still have the problem I mentioned, that a<br>
definition of something using \() type checks, but its uses don't,<br>
unless \() is replaced by y.<br>
<br>
Its use won't typecheck because you are trying to use a theorem that<br>
talks about y to prove something about a definition using \() and they<br>
are not equal because they are not compared structurally. It's more<br>
surprising for the case where you use \() in both places, but each use<br>
of \() gets desugared into its own definition so each one gets a<br>
distinct "name".<br>
<br>
[...]<br>
BTW, Agda has a lot of "eta expansion" I mentioned in a previous<br>
message. You seem to be saying that my problem is a lack of absurd<br>
eta. But I am saying I don't necessarily see this as the problem.<br>
Further clarification by the Agda implementors would be really<br>
appreciated here.<br>
<br>
<br>
Indeed, a more structural equality for pattern-matching definitions,<br>
like in PiSigma [1], should also solve this, as proposed in another<br>
thread [2] about the same problem, but in the context of coinduction.<br>
<br>
[1] <a href="http://www.cs.nott.ac.uk/~txa/publ/pisigma-new.pdf" target="_blank">http://www.cs.nott.ac.uk/~txa/<u></u>publ/pisigma-new.pdf</a><br>
[2] <a href="https://lists.chalmers.se/pipermail/agda/2010/002573.html" target="_blank">https://lists.chalmers.se/<u></u>pipermail/agda/2010/002573.<u></u>html</a><br>
<br>
Cheers,<br>
Andrea.<br>
<br>
<br>
Best,<br>
Martin<br>
<br>
<br>
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></div></div>
<mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>>>:<div><div class="h5"><br>
<br>
I have a problem with absurdity in Agda, which I can solve<br>
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<br>
the desirable<br>
way doesn't work.<br>
<br>
I have three types X,Y,Z, whose definition I omit here. I<br>
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<br>
be zero and so<br>
they trivialize in this special case, as they have<br>
occurrences of Fin n in<br>
their definitions.<br>
<br>
Now I have three holes in a definition (of a fourth type),<br>
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 \(),<br>
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<br>
corresponding<br>
term, type checking still fails.<br>
<br>
Additionally, if I ask the emacs interface to fill the<br>
wholes with ctrl-c-a,<br>
this succeeds, with expressions containing the string<br>
"absurd". But then the<br>
resulting expression doesn't type check.<br>
<br>
And there is a more annoying fact. I have previous<br>
definition of something<br>
else that uses \() and does type check. However, when I use<br>
it, things fail.<br>
I instead need to use the same definition with replaced \()<br>
by y.<br>
<br>
This is very mysterious to me.<br>
<br>
I didn't manage to distil a simple instance of this to<br>
reproduce here. But<br>
if you are brave enough, you can search for "AGDA PROBLEM"<br>
in any of the two<br>
following links:<br>
<br></div></div>
<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.<u></u>html</a> <<a href="http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.html" target="_blank">http://www.cs.bham.ac.uk/~<u></u>mhe/dialogue/dialogue-lambda.<u></u>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.<u></u>lagda</a><div class="im"><br>
<<a href="http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.lagda" target="_blank">http://www.cs.bham.ac.uk/~<u></u>mhe/dialogue/dialogue-lambda.<u></u>lagda</a>><br>
<br>
Help is appreciated.<br>
<br>
Martin<br></div>
______________________________<u></u>___________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><br>
<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><div class="im"><br>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>><br>
<br>
<br>
--<br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
<br></div>
______________________________<u></u>___________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><br>
<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>><br>
<br>
<br>
</blockquote><div class="HOEnZb"><div class="h5">
<br>
-- <br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
</div></div></blockquote></div><br></div>