Church-encodings are cute but closures take space, more specifically an unbounded amount of it (for the code, unless you defunctionalize it)! Hence it is much m

Church-encodings are cute but closures take space, more specifically an unbounded amount of it (for the code, unless you defunctionalize it)! Hence it is much more practical to have a primitive notion of inert data that can be inspected and which has a fixed or at least predictable size. Although there are also other more efficient lambda-encodings like Scott-encoding / Mendler-style algebras. See https://firsov.ee/efficient-lambda/ https://firsov.ee/efficient-lambda/, it's a very cool paper. But it also shows it's very tricky to give a type to these encodings. In the end you're almost always better off building "real" datatypes with records and ADTs unless your only goal is to have a minimal theory.