The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hello Jason,

On 18.08.12 6:58 PM, Jason Gross wrote:
> Hi,
> I have two related questions:
> Given a record like
>    Record foo := { bar : Type }.
> (or a more complicated one with arguments and multiple fields, or
> possibly even any inductive type with one constructor which lives in
> [Type]),

Agda has eta-conversion for records.  There are no theoretical problems, 
it can be dealt with in type checking, unification [Norell PhD; 
Abel/Pientka TLCA 2011], and semantic models [Abel/Coquand FundInf 2007].

However, adding eta-conversion for inductive types with just one 
constructor may break termination.  Here is a hypothetical case:

  data Empty : Set where
    c : (d : Empty) -> Empty

  f : Empty -> Empty
  f (c x) = c (f x)

f is structurally recursive, however, we have

  f x = f (c (d x)) = c (f (d x)) = c (f (c (d (d x)))) = c (c (f (d (d 
x))))

You see where this leads to...

In particular, we do not want eta for the type Acc...

Cheers,
Andreas

> First, would it break CIC (or cause any other problems) if [f : foo]
> were made convertible with [Build_foo (bar f) : foo]?  (Is this properly
> named "eta conversion of records", or is it called something else?)  I
> suspect it wouldn't cause any problems, because I can always do
> something like
>    let t := fresh in destruct f as [ t ];
>      change (Build_foo (bar (Build_foo t))) with (Build_foo t) in *;
>        set (f := Build_foo t) in *;
>          clearbody f; clear t.
> in any proof in which I want [f] and [Build_foo (bar f)] to be
> convertible.  Admittedly, this adds an extra [match] in the
> proof/construction, but I don't think this is a big deal, because I
> think we can always "get rid "of the match by [destruct f] in any
> proof/construction (that is, after [intros], we can always move the
> match up to top level, I think).
> However, I'm not completely confident in my argument, because I know
> that allowing this kind of match-less conversion on inductive types not
> in [Type] (such as [@eq]) leads to ill-typed terms and being able to
> prove proof irrelevance.
>
> Second: Assuming that this would not cause problems, are there any plans
> to add this to Coq?
>
> Thanks.
>
> -Jason

--
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/