# [Agda] Absurd question

Martin Escardo m.escardo at cs.bham.ac.uk
Fri May 24 00:37:13 CEST 2013

```This seems something sensible to conjecture (but there is a "but" below):

On 23/05/13 23:01, Guillaume Brunerie wrote:
> One possible reason is the following: when you write
>
> y : Y
> y = \()
>
> I think that Agda replaces it by something like:
>
> y : Y
> y = fresh where
>    fresh : Y
>    fresh ()
>
> In other words, the primitive notion is the notion of definition by
> absurd pattern and when you write an absurd lambda \(), Agda will
> replace it by a fresh name which is a function defined by an absurd
> pattern.
> A consequence of that is that \() is not definitionally equal to \(),
> or more generally you don’t have
>
> let x = \() in M   definitionally equal to    M[\() / x]
>
> because in the first case only one new function will be generated, and
> in the second case one new function will be generated for each
> occurrence of x in M.

However, my first, original, definition of y:Y was

y : Y
y ()

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.

> In your case, you can maybe work around this issue by defining a
> function Fin0-elim which proves anything given an element of Fin 0
> (this function is defined by an absurd pattern or absurd lambda), and
> then only use Fin0-elim instead of absurd lambdas.

Yes, possibly, I will try that when I have time.

But, still, this requires redefining the natural formulations into
unnatural ones. (You would have to see the file to appreciate the

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.

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
>>
>> http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.html
>> 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

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