FP has a small set of primitives that encode everything you can computationally do. One of the first thing you'd learn is how to use those primitives, to 'emulate' anything an imperative language does.

Most definitions of imperative include "unpure editing of global state", which is just the equivalent of passing along a state object implicitly to every function, which is just extra verbose for whatever fundamental type-theory point you're trying to make and would not affect the argument in terms of those fundamental primitives.

Not necessarily, in our compiler design lectures we also used for type systems in imperative languages.

Eiffel reference is one of the few manuals to fully specify the type system with denotational semantics, for example.

Here is an example of type theory in OOP languages,

https://www.sciencedirect.com/science/article/abs/pii/009605...

I am guessing, that it is, because imperative processes are very hard to describe properly using type theory. For example: If you have an object, that has some members, that are initially not set, that is a different type than when they are set. So you cannot say that object has exactly one type. After every setting of a member, you have a new type. That's not something that you can statically work with easily. Mutation destroys the type guarantees. The type system can only be on a more limited level, that is rougher and doesn't give as many guarantees, unless you restrict yourself in what you do to your objects. Like for example not mutating them. Or not having nullable members. Things like that.

So I think FP is more suitable for type theory research and pondering, and people who are researching in the matter will not even consider doing that for imperative languages, because they have understood long ago, that these languages lack the guarantees, that you can get with FP, and therefore are not worth spending the time on.

I think it comes down historically to Church's https://en.m.wikipedia.org/wiki/Simply_typed_lambda_calculus . It originated the most popular form of type theory and also used the simplest functional programming language, lambda calculus.

I recently started to look at this the other way around. A functional paradigm allows to describe very precisely what a function does through its type. In imperative languages, OTOH, the type signature of a function (which really should be called a procedure) only gives you little information to what happens when you call it, due to mutable state, side effects, etc.

It's very simple, it's because pure, typed functional programming is not arbitrary but rather fundamental. Natural deduction from logic corresponds to various typed lambda calculi, and functional programming is but a practical manifestation of lambda-calculus.

Under Curry-Howard correspondence simply typed lambda calculus is the term calculus for intuitionistic propositional logic. System F (polymorphic lambda calculus) corresponds to impredicative second-order propositional logic. System Fω corresponds to a kind of higher-order logic. Dependent types correspond to intuitionistic predicate logic, etc.

Other correspondences that are based on sequent calculus instead of natural deduction are more exotic, for example classical logic corresponds to μ~μ-calculus, a calculus of continuations which (very) roughly can be understood as continuation-passing style (but in a principled and careful way). Classical linear logic corresponds to a form of session-typed process calculus. Intuitionistic linear logic corresponds to either a process calculus or to a lambda calculus that is using futures (which can be though as mutable shared memory concurrency using write-once cells).

Note however that languages corresponding to sequent calculus, especially ones that come from a dual calculus (classical logic or classical linear logic) contain some sort of commands, choices that you request from a value, which more or less makes them object-oriented languages, albeit without imperative, mutable assignment. In some sense you can escape functional programming by moving to a dual calculus, but you can't escape purity as long as you care about having propositions as types.

From a Curry-Howard point of view no logic corresponds to a general imperative calculus. Imperative programming is simply not fundamental and generally undesirable when doing logic (so when doing type theory). Mutable state with imperative updates can easily be encoded into FP when needed, e.g. via monads, by using linear types, or by having algebraic effects.

That doesn't mean that types are not useful to imperative languages, of course they are. But types in imperative programming are very weak and logically not very interesting however useful they might be for engineering purposes. Also note that type theory does not mean type system. Many languages have type systems, some more ad-hoc than others, but type theories are special, very specific mathematical objects that embody logic (under the Curry-Howard correspondence). All programs written in a type theory terminate, and this is fundamental. Usual programs, which are not concerned with mathematical proofs certainly don't always terminate.

Of course understanding type theory is a very good way of producing (weaker) type systems that are useful in practical programming, including imperative programming (see for example Rust, which does not employ an ad-hoc type system). Occasionally new logic correspondences are discovered which illuminate certain language features of existing languages. For example Rust's borrowing system was thought to be ad hoc, but now we understand that shared borrows correspond to a logic that arises from semi-axiomatic sequent calculus. The cuts that remain after evaluation (normalization), called snips, are precisely shared borrows, while general cut is memory allocation.

The book in the link is a book about Martin-Löf type theory, which means it is a book about a certain kind of lambda calculus by necessity, there is no other choice.

Type theory absolutely can enhance imperative languages! In fact, we're seeing this happen:

Rust is the prime example - it uses affine types (linear logic) to track ownership and borrowing in imperative code. The type system prevents memory safety bugs at compile time without garbage collection.

C++ concepts (C++20) bring dependent typing to template metaprogramming. You can express "this function works for any type T that satisfies these type-level constraints."

Refinement types in languages like Dafny let you encode invariants directly in the type system for imperative code: int{x | x > 0} for positive integers.

The challenge isn't technical compatibility - it's that imperative programming often emphasizes mutation and side effects, while type theory shines at reasoning about pure transformations. But when you can encode the "shape" of your mutations in types (like Rust's ownership), you get incredible safety guarantees.

The real question might be: why don't more imperative languages adopt these ideas? Legacy compatibility and learning curves are probably the main barriers.