What is a commuting conversion and why are they problematic?

Question

Off and on I have heard of the jargon "commuting conversion" but I don't really know what it means.

I've heard commuting conversions are problematic but I don't know why.

Answer 1

1. Syntactically, commuting conversions are part of the $\eta$-rules for left-invertible types -- i.e., types which have pattern-matching eliminators. So if $e : A + B$, the $\eta$-equation for it looks like:

   $$ \newcommand{\c}[1]{\mathsf{#1}} C[e] \equiv \c{case}(e, \c{inl}\,x \to C[ \c{inl}\,x], \c{inr}\,y \to C[ \c{inr}\,y]) $$

   This rule says that if you have a term with an $e : A+B$ occuring in it somewhere (this is the $C[e]$), then it is the same as matching on $e$ and running $C[\c{inl}\, x]$ in the left branch and $C[\c{inr}\, y]$ in the right branch.

   The algorithmic difficulty this poses is that this rules is extremely nondeterministic and non-syntax-directed -- if you have a term $t$, you can break it into a context $C$ and expression $e$ such that $C[e] = t$ in potentially many different ways. Moreover, since the context $C$ is duplicated in each branch of the case statement, the context in each can be independently transformed some more into terms which look radically different from one another.

2. Semantically, commuting conversions arise from the fact that the sum type can be viewed as a coproduct. Since coproducts are a kind of colimit, they satisfy both an existence property, and a uniqueness property.

   The existence property of coproducts says that for each $X$ and $Y$, we have a type $X + Y$ and injection maps $\c{inl} : X \to X + Y$ and $\c{inr} : Y \to X + Y$ such that for each $f : X \to Z$ and $g : Y \to Z$, we have a map $[f, g] : X + Y \to Z$ such that $[f,g] \circ \c{inl} = f$ and $[f,g] \circ \c{inr} = g$.

   You can see that these two equations correspond to the $\beta$-rules for sums:

   $$ \c{case}(\c{inl}\,z, \c{inl}\,x \to e_1, \c{inr}\,y \to e_2) \equiv [z/x]e_1 $$ $$ \c{case}(\c{inr}\,z, \c{inl}\,x \to e_1, \c{inr}\,y \to e_2) \equiv [z/y]e_2 $$

   The uniqueness property tells us this map is unique. In particular, uniqueness means that if you have a map $h : X+Y \to Z$, then $h \equiv [h \circ \c{inl}, h \circ \c{inr}]$. (This is easy to see if you draw the coproduct diagram for this.)

   This is exactly the $\eta$-law, once you remember that composition of morphisms and substitution of terms are the same thing:

   $$ \newcommand{\c}[1]{\mathsf{#1}} C[e] \equiv \c{case}(e, \c{inl}\,x \to C[ \c{inl}\,x], \c{inr}\,y \to C[ \c{inr}\,y]) $$

3. Colimits without the uniqueness property are called "weak colimits", and come up fairly often in category theory. But it is still weird that $\eta$ for projective tuples and lambdas is easy, but that it's so hard for sum types.

Answer 2

In the comments, it was elaborated that one possible interpretation of a "commuting conversion" refers to $F(G(x))$ vs $G(F(x))$ where one of $F$ or $G$ is a recursor.

The problem

Here's an example in Lean of where commuting function application with a recursor application causes two terms to not be definitionally equal:

import data.sum.basic

variables {α β : Type*} (f : α → β)

def foo_1 : α ⊕ α → β := sum.elim f f 
def foo_2 : α ⊕ α → β := λ x, f (sum.elim id id x)

example : foo_1 f = foo_2 f := rfl  -- fails
example : foo_1 f = foo_2 f := by { ext x, cases x; refl } -- ok

This causes problems if we're working with typeclass instances; consider wanting to put an addition operator on the type sum.elim A B x which just inherits the addition of A l when x = inl l and B r when x = inr r.

The naive approach looks something like:

import data.sum.basic
import algebra.group.basic

universes u
variables {α β : Type*} {A : α → Type u} {B : β → Type u}

instance sum.elim.has_add
  [ia : Π a, has_add (A a)] [ib : Π a, has_add (B a)] :
  Π x, has_add (sum.elim A B x) :=
@sum.rec _ _ (λ x, has_add (sum.elim A B x)) ia ib

instance sum.elim.add_semigroup
  [ia : Π a, add_semigroup (A a)] [ib : Π a, add_semigroup (B a)] :
  Π x, add_semigroup (sum.elim A B x) :=
@sum.rec _ _ (λ x, add_semigroup (sum.elim A B x)) ia ib

But this results in the two paths to the has_add instance not being definitionally equal:

example [Π a, add_semigroup (A a)] [Π a, add_semigroup (B a)] (x : α ⊕ β) :
  add_semigroup.to_has_add (sum.elim A B x) = sum.elim.has_add x := rfl  -- fails

which means lemmas about add_semigroup will not apply to sum.elim.has_add:

example [Π a, add_semigroup (A a)] [Π a, add_semigroup (B a)] (x : α ⊕ β)
  (a b c : sum.elim A B x) : a + b + c = a + (b + c) := add_assoc _ _ _  -- fails

The solution

The solution is to push the recursors inside the application of has_add.mk and add_semigroup.mk:

import data.sum.basic
import algebra.group.basic

universes u
variables {α β : Type*} {A : α → Type u} {B : β → Type u}

instance [ia : Π a, has_add (A a)] [ib : Π a, has_add (B a)] (x : α ⊕ β) :
  has_add (sum.elim A B x) :=
{ add := @sum.rec _ _ (λ x, sum.elim A B x → sum.elim A B x → sum.elim A B x)
           (λ l, (ia l).add) (λ r, (ib r).add) x }

instance
  [ia : Π a, add_semigroup (A a)] [ib : Π a, add_semigroup (B a)] (x : α ⊕ β) :
  add_semigroup (sum.elim A B x) :=
{ add := @sum.rec _ _ (λ x, sum.elim A B x → sum.elim A B x → sum.elim A B x)
        (λ l, (ia l).add) (λ r, (ib r).add) x,
  add_assoc := begin
    cases x,
    exact add_assoc,
    exact add_assoc,
  end }

which makes the problem go away:

example [Π a, add_semigroup (A a)] [Π a, add_semigroup (B a)] (x : α ⊕ β) :
  add_semigroup.to_has_add (sum.elim A B x) = sum.elim.has_add x := rfl  -- ok

example [Π a, add_semigroup (A a)] [Π a, add_semigroup (B a)] (x : α ⊕ β)
  (a b c : sum.elim A B x) : a + b + c = a + (b + c) := add_assoc _ _ _  -- ok