[Agda] Absurd question

[Andrea Vezzosi]

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>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>:
>>
>>> 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
>>> 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
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130524/c6b27219/attachment.html