===

Short answer: yes, many type-theory folks prize a “pure core,” but the community is not monolithic—lots of work is explicitly about modeling effects safely.

What “purity” usually means in type theory

• Totality / termination. In Martin-Löf style dependent type theory (Agda/Coq), all programs must terminate. That guarantees consistency (by Curry–Howard, non-terminating programs would be “proofs” of anything).
• Referential transparency. No hidden side effects inside the core logic; effects are represented as data (monads, effects-and-handlers, linear resources, etc.).
• Normalization/canonicity/decidable checking. These technical ideals push designs toward a pure, strongly normalizing core.

Why people like it: it makes proofs-as-programs possible, keeps the logic sound, and supports trustworthy extraction to executable code.

But lots of type theory

is about effects

Purity in the core doesn’t mean “no effects.” It means effects are explicit and controlled:

• Monads / indexed & graded monads (Moggi, Wadler, Atkey) to track state, IO, probability, cost.
• Algebraic effects & handlers (Plotkin–Pretnar) to represent effectful operations with modular semantics.
• Call-by-push-value (Levy) to factor evaluation order and effects cleanly.
• Linear/quantitative types (Girard → Wadler, McBride, Gaboardi, etc.) to model resources, mutation, and concurrency while staying principled.
• Guarded/corecursion (Nakano, et al.) to allow infinite reactive processes but preserve productivity.

So: lots of “purity,” but also lots of effect systems—the point is disciplined effects, not their absence.

MIRI / Nate Soares and the “purity” vibe