The Blog of Bob Rubbens
Original conversation, hosted here for longevity. I removed a few references that ChatGPT from the transcript.
Me:
In the context of church encoding, is the predecessor function typable in dependent type theory?
ChatGPT:
Short answer: it depends on impredicativity.
In a predicative dependent type theory (e.g. MLTT/Agda/Coq’s Type hierarchy), the usual Church encoding
CNat ≜ ∀A:Type. (A → A) → A → A
makes pred : CNat → CNat not typable in general. The definition of pred needs to instantiate the quantified type with a type that itself quantifies over types (a kind of self-application), which predicativity forbids. Coq lecture notes make this precise: addition/multiplication can be arranged to type-check with Type, but the typing problem reappears for predecessor and cannot be avoided.
In an impredicative setting (System F; or a DTT with an impredicative universe like Coq’s Prop), the standard Church predecessor is typable using higher-rank polymorphism; the classic term
λn f x. n (λr i. i (r f)) (λf. x) (λu. u)
type-checks there.
Related context: Church numerals make destructors like predecessor possible but costly (linear time), whereas Scott/Church–Scott encodings give constant-time destructors or require recursive types.
Bottom line: With Church numerals, pred is typable in impredicative (System-F-like) dependent type theories, but not in predicative ones without extra machinery or a different encoding.
Generated with BYOB.
License: CC-BY-SA.
This page is designed to last.
