# Why do record based inductive types with primitive projections lack an eta law?

In Coq there is ongoing work to shore up some weaknesses in subject reduction and coinductive types. Primitive projections are part of that effort for better behaviour.

I get why there might be complications with eta reduction for coinductive types with primitive projections but what's the problem with inductive types?

For context I'm playing with a minor variant of W types and I basically have to decide between

Inductive W {A: Set} (B: A -> Set) :=
| sup s (p: B s -> W B).


and

Inductive W {A: Set} (B: A -> Set) := sup {
tag: A ;
field (ix: B tag): W B ;
}.


With primitive projections the latter lacks an eta law. You can do a sort of variant of an induction principle here but it's more than a little awkward and I don't really understand the how and whys here.

I don't have any evidence for my intuition and the record encoding is a little awkward to use sometimes but my intuition just says the record encoding looks prettier. It definitely might not be the best choice though.

Reduction will not terminate if you give W an eta law. Fixpoints only reduce when applied to constructors. However, if you have F : W B -> C such that F (sup t f) reduces to F_step t f (fun x => F (f x)), then F x would reduce to F (sup x.(tag) x.(field)) which would reduce to F_step x.(tag) x.(field) (fun y => F (x.(field) y)). Reduction would then continue under binders ad infinitum.
We can also consider restricting our attention to just conversion. Consider a Turing Machine runner that uses @W unit (fun _ => unit) for termination fuel and computes whether the Turing Machine halts. Even though the type is uninhabited, fun fuel => does_it_halt TM fuel will be convertible with fun _ => true whenever TM halts. Hence the eta rule forces conversion to decide the halting problem.
• I am not sure I understand your answer, since eta laws in Coq are not part of reduction, only in conversion, so I do not think your example would manifest in practice. Also, what should the type of  F_step be? Jun 10 at 9:48
• If the eta law exposes new opportunities for reduction, then reduction cannot be considered complete without the eta law. That is, if a term of type unit is convertible with tt but does not reduce to tt then we do not have strong normalization. But my answer works just as well (perhaps even better) if you replace "reduction" with "conversion". With the eta rule you suggest, you cannot decide in finite time whether or not a given term is convertible with fun _ => true. Jun 12 at 1:42
• Consider a Turing Machine runner that uses @W unit (fun _ => unit) for termination fuel and computes whether the Turing Machine halts. Even though the type is uninhabited, fun fuel => does_it_halt TM fuel will be convertible with fun _ => true whenever TM halts. Hence the eta rule forces conversion to decide the halting problem. Jun 12 at 1:45
• And F_step is roughly the argument to the induction principle for W, it would have type forall (t : A), (B t -> W B) -> (B t -> C) -> C (the dependently typed version is of type forall (t : A) (f : B t -> W B), (forall b : B t, C (f b)) -> C (sup t f)) Jun 12 at 1:49