6
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Note that out is an empty type in Agda. $\endgroup$
    – András Kovács
    Commented Mar 30, 2019 at 15:25
  • $\begingroup$ @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? $\endgroup$
    – molikto
    Commented Mar 30, 2019 at 15:41

1 Answer 1

Reset to default
3
$\begingroup$

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

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$
    – molikto
    Commented Mar 31, 2019 at 2:23
  • $\begingroup$ 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. $\endgroup$
    – Blaisorblade
    Commented Mar 31, 2019 at 17:21
  • $\begingroup$ This is true in general, see this paper by Berger and Setzer. $\endgroup$
    – Henning Basold
    Commented Apr 6, 2019 at 10:24
  • $\begingroup$ @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 $\endgroup$
    – molikto
    Commented Apr 7, 2019 at 10:52
  • $\begingroup$ 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?) $\endgroup$
    – molikto
    Commented Apr 19, 2019 at 11:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.