[Agda] eta expansion

[Martin Escardo]

In fact, I would like to hear from the Agda developers and advisors how 
close or far Agda is from the MLTT family of type theories.

Let me make a sloppy summary of what I understand the situation is,
hoping that you will both enlarge the list and correct or improve my
items:

(0) Universes "Set_n" are `a la Russell in principle, but not quite if
one does naughty things (such as pattern-matching constructors, which
BTW falsify function extensionality).

(1) Pattern matching.

     Is fine provided refl is not a pattern (except for the definition
     of J).  Good to have without-K, but not so good that there isn't a
     theory of pattern matching without K, or any assurance that
     without-K actually works. This is particularly relevant for the
     HoTT enthusiasts using Agda.

(2) Inductive "data" types take us well beyond what we can do with
W-types in MLTT. This is good, but on the other hand not well
understood, and not guaranteed to be consistent. It would be good to
have a pragma W that only allows data definitions that can be
(automatically) translated to W-types (and/or well-understood
generalizations). Id types should be treated separately, as well as
Sigma types (?). I don't believe in the generality of the "data"
concept that allows Id, Sigma and W, and many more things, under the
same umbrella.

(3) Non-termination. Is there a theorem saying that if the Agda
termination algorithm succeeds then what we wrote using patterns and
recursion can be written down using MLTT combinators only? (We've
already been through this discussion in this list, but only
briefly. But what happens without-K? Etc.) This is particularly
pressing regarding type recursion.

(4) Eta. Already discussed.

(5) We badly need some form of well understood "core Agda" clearly
corresponding to well understood (families of) type systems, which
allows most of Agda to be reduced to that (mechanically).

(6) Of course, it is good to have experimental features outside the
core. They can either come from research directions or else inform
research, or both. Like it is happening in HoTT. But they should be
clearly distinguished from the "trusted" core.

(7) It is also good to have, as we do, (i) the possibility to disable
the termination checker locally in modules (for example to implement
Bar recursion), and (ii) Type:Type, for example to implement
h-propositional reflection in the sense of HoTT in a computationally
meaningful way. So please do keep allowing naught things in Agda. But
please also do allow a fine control of their allowability.

There are probably are more things that I didn't notice.

Needless to say, I do love Agda, and this is supposed to be
constructive criticism (no pun indended).

Best,
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