<p>Having a recursive record type with eta-equality wouldn't destroy consistency of the theory, but it would destroy decidability of typechecking.</p>

<p>For example, let's define your <code>out</code> type as a record type in Agda:</p>

<pre><code>record Out : Set where
  inductive
  constructor cons
  field
    in : Out
</code></pre>

<p>Agda doesn't use eta-equality for this type. Suppose it did, then Agda's typechecker would loop whenever it tries to solve an equation of the form <code>x = y : Out</code> (where <code>x</code> and <code>y</code> are two variables or neutral terms): <code>x = y</code> iff <code>in x = in y</code> iff <code>in (in x) = in (in y)</code> iff <code>in (in (in x)) = in (in (in y))</code> ... </p>

CC BY-SA 4.0
2019-03-31T02:23:42.077Z
Is this just true for Agda or generally all implementations? If we don't have meta variable and unification, can we don't eta-expand when both side are generic value, and just return `x != y`?
molikto
CC BY-SA 4.0
2019-03-31T17:21:59.503Z
This argument only shows that a certain typechecking strategy isn’t termination, but it doesn’t seem to prove that typechecking is undecidable, or do I miss something?
@molikto even without type inference, type checking needs to decide if terms are judgmentally/definitionally equal.
Blaisorblade
CC BY-SA 4.0
2019-04-06T10:24:03.740Z
This is true in general, see [this paper](http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf) by Berger and Setzer.
Henning Basold
CC BY-SA 4.0
2019-04-07T10:52:08.853Z
@HenningBasold I don't think this paper is related. it deals with coinductive types without eta rules, the recursive record type I mentioned is a special case of inductive type
molikto
CC BY-SA 4.0
2019-04-19T11:29:03.810Z
I now understand that the above is even true without meta variables. The "equations" is just type directed conversion checking algorithm. But still, one choice is turn off eta for non-guarded recursive record. Another one is simply say all items of a non-guarded recursive record is equal. They are empty anyway. Not sure if this is sound. (practically this doesn't matter, because these types has not much use?)
molikto
CC BY-SA 4.0
2019-03-30T21:46:48.047Z
2019-03-30T21:46:48.047Z
Jesper
<p>In the context of Agda like dependent type theory:</p>

<p>This short paper <a href="https://jesper.sikanda.be/files/vectors-are-records-too.pdf" rel="noreferrer">https://jesper.sikanda.be/files/vectors-are-records-too.pdf</a> says some inductive type can be seen as records, for example <code>Vector</code> of fixed-length list can be seen as inductively-defined family of <strong>non-recursive</strong> types.</p>

<p>But they argue that for example natural number type should not have a eta rule because it is a recursive type (the original paper says <code>N = Unit \/ N</code> is non-terminating.)</p>

<p>So what will go wrong if we have this type:</p>

<pre><code>data out where
  cons : out =&gt; out

in : out =&gt; out
in (cons a) = a
</code></pre>

<p>and give it a negative eta-rule:</p>

<p><code>(a: out)</code>  then  <code>a = cons (in a)</code> judgementally</p>

<p>Can it proof <code>False</code>? Or just this is a bad idea....?</p>

<hr>

<p>edit: It seems Agda has eta-rule for recursive records? but not for the one previously defined, see this issue <a href="https://github.com/agda/agda/issues/402" rel="noreferrer">https://github.com/agda/agda/issues/402</a> . but the previously defined one is ruled out I think by implementation issues, not theoretical one?</p>

CC BY-SA 4.0
2019-03-30T15:25:57.447Z
Note that `out` is an empty type in Agda.
András Kovács
CC BY-SA 4.0
2019-03-30T15:41:05.593Z
@AndrásKovács Yes this is explained in the issue. So if Agda permits this eta rule, where can I found a semantical justification? or is it trivial?
molikto
<type-theory><dependent-type>
What will go wrong if a recursive record type has a negative eta rule?
molikto
# What will go wrong if a recursive record type has a negative eta rule?

(Asked by: username_0 on 2019-03-30)

In the context of Agda like dependent type theory:
This short paper https://jesper.sikanda.be/files/vectors-are-records-too.pdf says some inductive type can be seen as records, for example Vector of fixed-length list can be seen as inductively-defined family of non-recursive types.
But they argue that for example natural number type should not have a eta rule because it is a recursive type (the original paper says N = Unit \/ N is non-terminating.)
So what will go wrong if we have this type:
data out where
  cons : out => out

in : out => out
in (cons a) = a

and give it a negative eta-rule:
(a: out)  then  a = cons (in a) judgementally
Can it proof False? Or just this is a bad idea....?

edit: It seems Agda has eta-rule for recursive records? but not for the one previously defined, see this issue https://github.com/agda/agda/issues/402 . but the previously defined one is ruled out I think by implementation issues, not theoretical one?

**Tags:** type-theory, dependent-type

> **Comments:**
> **username_1**: Note that `out` is an empty type in Agda.  
> **username_0**: @AndrásKovács Yes this is explained in the issue. So if Agda permits this eta rule, where can I found a semantical justification? or is it trivial?  

---

## 1 answers

### Answer by username_2 on 2019-03-30. Score: 3 | Accepted answer

Having a recursive record type with eta-equality wouldn't destroy consistency of the theory, but it would destroy decidability of typechecking.
For example, let's define your out type as a record type in Agda:
record Out : Set where
  inductive
  constructor cons
  field
    in : Out

Agda doesn't use eta-equality for this type. Suppose it did, then Agda's typechecker would loop whenever it tries to solve an equation of the form x = y : Out (where x and y are two variables or neutral terms): x = y iff in x = in y iff in (in x) = in (in y) iff in (in (in x)) = in (in (in y)) ...

> **Comments:**
> **username_0**: Is this just true for Agda or generally all implementations? If we don't have meta variable and unification, can we don't eta-expand when both side are generic value, and just return `x != y`?  
> **username_3**: This argument only shows that a certain typechecking strategy isn’t termination, but it doesn’t seem to prove that typechecking is undecidable, or do I miss something? @username_0 even without type inference, type checking needs to decide if terms are judgmentally/definitionally equal.  
> **username_4**: This is true in general, see [this paper](http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf) by Berger and Setzer.  
> **username_0**: @HenningBasold I don't think this paper is related. it deals with coinductive types without eta rules, the recursive record type I mentioned is a special case of inductive type  
> **username_0**: I now understand that the above is even true without meta variables. The "equations" is just type directed conversion checking algorithm. But still, one choice is turn off eta for non-guarded recursive record. Another one is simply say all items of a non-guarded recursive record is equal. They are empty anyway. Not sure if this is sound. (practically this doesn't matter, because these types has not much use?)  

---

