[Agda] Absurd question

[Martin Escardo]

Thanks for the explanation.

I think I need to ditch pattern matching and work with the Fin 
eliminator instead, as Guillaume suggested.

But I still don't understand why if I write

   blah (\())

I get a type-checking error, whereas if I write

   blah y

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.

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.

Anyway, I at least understand one of the two problems after Guillaume 
and your explanation.

Thanks,
Martin

On 24/05/13 15:02, Andrea Vezzosi wrote:
> Not an implementor, but I'll add my explanation.
>
> On Fri, May 24, 2013 at 12:37 AM, Martin Escardo
> <m.escardo at cs.bham.ac.uk <mailto:m.escardo at cs.bham.ac.uk>> wrote:
>
>     [...]
>     However, my first, original, definition of y:Y was
>
>     y : Y
>     y ()
>
>
> That's the same as desugaring the \() manually, hence it'll get the same
> results.
>
> 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.
>
>     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.
>
> 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".
>
>     [...]
>     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.
>
>
> 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.
>
> [1] http://www.cs.nott.ac.uk/~txa/publ/pisigma-new.pdf
> [2] https://lists.chalmers.se/pipermail/agda/2010/002573.html
>
> Cheers,
>    Andrea.
>
>
>     Best,
>     Martin
>
>
>         Guillaume
>
>         2013/5/23 Martin Escardo <m.escardo at cs.bham.ac.uk
>         <mailto:m.escardo at cs.bham.ac.uk>>:
>
>             I have a problem with absurdity in Agda, which I can solve
>             in an undesirable
>             way, which forces me to change several definitions.
>
>             I would like to both understand what the problem is, and why
>             the desirable
>             way doesn't work.
>
>             I have three types X,Y,Z, whose definition I omit here. I
>             can define, using
>             absurd patterns,
>
>             x : X
>             x = \a ()
>
>             y : Y
>             y : \()
>
>             z : Z
>             z : \()
>
>             These are types which have a parameter n:N that happens to
>             be zero and so
>             they trivialize in this special case, as they have
>             occurrences of Fin n in
>             their definitions.
>
>             Now I have three holes in a definition (of a fourth type),
>             reported to have
>             types X,Y,Z. I can fill the holes with x,y,z, and the definition
>             type-checks.
>
>             But if I instead fill the holes with \a (), \(), and \(),
>             expanding the
>             definitions of x,y,z, then type-checking fails.
>
>             Moreover, if just one of the three holes is filled with the
>             corresponding
>             term, type checking still fails.
>
>             Additionally, if I ask the emacs interface to fill the
>             wholes with ctrl-c-a,
>             this succeeds, with expressions containing the string
>             "absurd". But then the
>             resulting expression doesn't type check.
>
>             And there is a more annoying fact. I have previous
>             definition of something
>             else that uses \() and does type check. However, when I use
>             it, things fail.
>             I instead need to use the same definition with replaced \()
>             by y.
>
>             This is very mysterious to me.
>
>             I didn't manage to distil a simple instance of this to
>             reproduce here. But
>             if you are brave enough, you can search for "AGDA PROBLEM"
>             in any of the two
>             following links:
>
>             http://www.cs.bham.ac.uk/~mhe/__dialogue/dialogue-lambda.html <http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.html>
>             http://www.cs.bham.ac.uk/~mhe/__dialogue/dialogue-lambda.lagda
>             <http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.lagda>
>
>             Help is appreciated.
>
>             Martin
>             _________________________________________________
>             Agda mailing list
>             Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>             https://lists.chalmers.se/__mailman/listinfo/agda
>             <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>     --
>     Martin Escardo
>     http://www.cs.bham.ac.uk/~mhe
>
>     _________________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/__mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe