Type Theory and Functional Programming (1999) [pdf]

The programming paradigms (functional, imperative, declarative) as implemented generally don't have strong theories behind them. We have no sharp line to detect when a language sits in any of those categories for any major language apart from SQL. One can write something that is recognised as functional in an imperative language for example. And even the best example of purity, SQL, in practice needs to be hosted in an imperative or functional environment to get useful results. The declarative part of the language isn't competent at getting complex performance-friendly results.

One of the interesting things about being a member of the functional programming community is I genuinely can't tell what the claim to fame of the community actually is beyond a sort of club-like atmosphere where people don't like mutability. Are we claiming that C++ programmers don't know how to write pure functions? I hope not, they clearly know. Many are good at it.

Lambdas are now a requirement for any modern programming language. Monadic promises are how asynchronous programming is done. Rust is basically OCaml except with typeclasses and without a GC.

Inch by inch, ideas from FP bubble up into mainstream programming.

I predict that algebraic effects (a la Koka) are next, but it'll be a while before the industry is ready for it.

...except they aren't. The world is gradually slipping towards nosql databases and stepping away from normalized data stores, to the point where tried and true RDBMS are shoehorning support for storing and querying JSON documents.

All flagship database services from major cloud providers are nosql databases.

Perhaps you're confusing pervasiveness with representing gold standard. Yes, RDBMS are pervasive, but so are non-compliance with the standard and vendor-specific constructs. The biggest factor was not what was the theoretical background behind each implementation but ease of use and ease of adoption. SQLite is an outstanding database not because of its compliance with SQL standards and adherence to theoretical purity, but because it's FLOSS and trivial to setup and use.

I expect the same factors to be relevant in adoption of functional programming. This stuff exists for decades on end but mass adoption was between negligible to irrelevant. What started to drive adoption was the inception of modules and components that solved real-world problems and helped developers do what they wanted to do with less effort. In JavaScript the use of map, filter and reduce is not driven by any new-founded passion for function programming but because it's right there and it's concise and simple and readable and capable. In C#, linq is gaining traction for the same reasons but is largely kept back by performance issues.

The key aspect is pragmatism, and theoretical elegance is by far a mere nice-to-have.

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.

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...

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.

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.

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.

That said, the book is very dense; for me it was just too much the first time I tried to read it. After circling back to it after a while it gets much easier, because you know what parts you really need (which is a common pattern for me at least with everything academic).