[Agda] eta expansion

[Martin Escardo]

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