[Agda] Absurd question

[Martin Escardo]

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 
unnaturality, reported in the comments.)

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
>> following links:
>>
>> 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