---
title: "Transcript of my impredicativity chat with ChatGPT"
author: Bob Rubbens
template: template/page.mako
---

[Original conversation](https://chatgpt.com/share/68e763c2-597c-8011-ac9a-384893d7c122), 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.