Type Theory and Functional Programming (1999) [pdf]

I agree. It's happening.

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.

> Concepts that have a strong theory behind them tend to last longer.

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.

> Similar to how relational databases and SQL are still the gold standard today.

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

That seems improbable. Pure functional languages are very unpopular according to TIOBE. In particular, interest in Haskell seems to be in decline. Functional features are mostly just an add-on to programming languages with mutable state. By far the most popular language, Python, doesn't even have static typing.

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.

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.

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.

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.

It's out-of-print.

TTOP is the standard work on the topic. Some parts I would say fell out of fashion (using Miranda for example), but many parts are either timeless or still just as relevant.

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

Sure, why not. It seems to be a pretty good exposition of the material. When I got interested in this stuff many years ago I worked my way through the 'typing rules' in the coq (nowadays rocq) manual. That is a 'slightly' higher friction way of learning this stuff. This document seems to be more pedagogical.

A related book (seems to be more often cited) is Types and Programming Languages by Benjamin C. Pierce. That seems to be more concrete (as opposed to theoretical), with chapter titles like "An ML Implementation of {some concept}".