Transcript of my impredicativity chat with ChatGPT
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.