[Agda] eta expansion

[Martin Escardo]

The point I am trying to make is that some people use Agda for practical 
purposes and other people use it for research purposes. It would be good 
if Agda catered for both.

Martin

On 08/03/13 19:23, Martin Escardo wrote:
> There are many uses of Agda, and for some of them I love eta, as a
> poor-man's version of function extensionality. In fact, I would love to
> have full function extensionality (that computes) for the purposes of
> doing (constructive) maths in Agda.
>
> But I am writing a paper in which I claim that certain things are
> provable in intensional Martin-Loef Type Theory, and I am using
> (minimal) Agda to help me. However, I (accidentally) noticed that Agda
> is silently doing eta in a particular situation, which doesn't belong to
> MLTT. I can do away with that by writing a different argument, that
> doesn't rely on eta. But my worry is that there maybe unnoticed uses of
> eta.
>
> So it would be good to have a pragma do enable/disable eta.
>
> Moreover, it would be good to have a pragma MLTT that doesn't allow any
> feature that take us beyond core MLTT (whatever we take that to be).
>
> Best,
> Martin
>
> On 08/03/13 16:59, Nils Anders Danielsson wrote:
>> On 2013-03-08 16:37, Andreas Abel wrote:
>>> Without eta, the equation Y x == f x gives two different solutions for
>>> Y: f and \lambda x -> f x.  It is not clear which one Agda should
>>> choose, one of the tests would fail, and it would be rather arbitrary.
>>
>> I think it's clear that Agda should refrain from choosing a solution.
>> This isn't arbitrary (but both tests would fail).
>>
>

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