[Agda] eta expansion
m.escardo at cs.bham.ac.uk
Fri Mar 8 20:23:30 CET 2013
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
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).
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).
More information about the Agda