[Agda] eta expansion

[Andreas Abel]

Hi Martin,

thanks for your message.  I remember you asked about the relationship 
between Agda and MLTT before and I owe you a response.  But I do not 
really have an answer.

First of all, MLTT appears to me as a soup of formalisms based on 
dependent types with the distinctive element of predicativity.  MLTT is 
a moving target.  As I understand, Martin-L"of's original idea is that 
of an open system in which you add data types and recursion principles 
that you can informally explain in a satisfactory manner.  Following 
this idea, Agda would not take any responsibility that your data and 
function definitions make sense, such things as positivity and 
termination checkers would not be necessary.  Probably you would not 
want to work this way, at least I would not.

So the first thing necessary to reach your goal of a "core Agda" that is 
faithful for "MLTT" would be to write down what should be understood 
under MLTT.  You seem to think of some theory without first-class 
recursion but instead a set of dedicated recursion operators for each 
type.  The next step would be to develop a compiler from Agda into MLTT. 
  One the way, one would probably identify the fragment of Agda which is 
justifiable in MLTT.  The whole enterprise has the volume of a PhD 
thesis, at least.

Personally, I am not so concerned about the connection of Agda to MLTT. 
  My personal take is Agda should be come a practical programming 
language based on dependent types and Curry-Howard, with all the 
proof-theoretic power that is predicatively justifiable.  I don't mind 
someone to add pragmas and options to Agda that restrict it to MLTT, but 
I myself lack time and interest to do so.  I am interested in a core 
language for Agda, but that would not be recursion combinators, but more 
something like type-based termination.

Some comments on your points:

(0) I do not understand.

(2)--(3) The termination checker has not been justified for 
induction-recursion, at least I never looked at these types formally.

Cheers,
Andreas

On 08.03.13 11:38 PM, Martin Escardo wrote:
> 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).
>>>
>>
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/