Definitional equalities for universal properties?

Using Rocq
1

If we view user-defined types as having the universal properties of sums, products, intial algebras, terminal coalgebras, etc. as a category theoretic perspective would suggest, we might want definitional equalities like the following (when well-typed):

f ≡ λ x, match f x with
         | (a, b) => (a, b)
         end

f ≡ λ s, match s with
         | inl a => f (inl a)
         | inr b => f (inr b)
         end

f ≡ λ n, match n with
         | 0 => f 0
         | S n' => f (S n')
         end

f ≡ λ x, match f x with
         | co0 => co0
         | coS c => coS c
         end

etc.

Would it potentially be acceptable to add these equalities when a type is defined, presumably behind some flag? I’m guessing we’d want them in the same order as eta equivalence, i.e. expansion?

2

I can give some thoughts. Summary: Coq already has a version of this for products, I don’t believe sums pose any fundamental problems, but with generalizations, in particular terminal coalgebras or the initial object you often lose decidable type-checking.

The primitive projections feature allows products with definitional eta (so your first equation).

I think I remember reading a paper about a (non-dependent) type theory with this eta rule for sums (your second equation), maybe using binary decision diagrams as normal forms? But I can’t find it right now.

If you redefine nat as the (isomorphic) 1 + nat, your third equation reduces to the second (well, if you have definitional eta for 1, which Coq also doesn’t, because it’s internal conversion checking is untyped and getting strict eta for 1 in this setting appears impossible).
You may have meant a more recursive version where any fix rec n := match n with O => a | S n => h (rec n) end = f whenever f O = a and f (S n) = h (f n).

For conat, your proposed equation implies n = match n with co0 => co0 | coS c => coS c end, but then I believe decidable type checking is impossible by reduction to the halting problem.

Take a Turing machine, and define n by coinduction on the state to be coS (next state) when the machine steps, and infinity when the machine halts. Then ask if n = infinity. If the machine ever halts, then n = infinity after expanding both by the number of steps taken. If the machine never halts, then n and infinity will never be the same (I think, my reasoning here is fuzzy), since n will always be a cofixpoint over the state and infinity a cofixpoint over unit. I don’t think the other consequences of your fourth equation span the gap, but I could be wrong.

However, if you define conat as 1 + conat, then definitional eta for sum implies your fourth equation, modulo the same caveat as with nat.

For a more solid example of where strict eta for coinductive types can go wrong, see section 1 of “Grins from my Ripley Cupboard” by Conor McBride.

There is an obvous generalization from sums to the initial type 0 or void, which is that f = \x -> match x with end when f : 0 -> A. This also prevents decidable type checking, with the argument spelled out in section 3 of the above linked note by Conor McBride.

1 Like
3

Deciding equality with eta for sums in a simply typed setting is showed (not the earliest proof) in “Deciding equivalence with sums and the empty type” ,
Gabriel Scherer, POPL 2017.
But now that I’m re-reading Conor’s argument for the undecidability of conversion with eta for empty types, I’m wondering whether we could adapt part of it to the case of binary sums (in a dependent setting ofc).