The Groovy Commutator in Lambda Calculus

Setup

For λ-terms Λ:

• D: one-step β-reduction
• I: application (MN)
• C: inequivalence check

What G ≠ 0 Detects

Terms where evaluation order matters—the difference between strict and lazy evaluation.

Type Theory Extension

Using McBride's "derivative of a type" (one-hole contexts / zippers):

• D: ∂ type derivative
• I: × product type
• C: ≅ isomorphism

Examples:

• ∂(List A) = List A × List A (before and after the hole)
• ∂(T^n) = n · T^(n-1) (the power rule!)

G(T) ≠ 0 detects types with computational content—where navigation structure is non-trivial.

Related: Evaluation Order, Zippers, Conor McBride