# What will go wrong if a recursive record type has a negative eta rule?

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?

• Note that out is an empty type in Agda. Mar 30 '19 at 15:25
• @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? Mar 30 '19 at 15:41

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)) ...

• 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? Mar 31 '19 at 2:23
• 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. Mar 31 '19 at 17:21
• This is true in general, see this paper by Berger and Setzer. Apr 6 '19 at 10:24
• @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 Apr 7 '19 at 10:52
• 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?) Apr 19 '19 at 11:29