What is next after typed functional programming?

No, functional-first languages such as OCaml, Haskell, Scheme, or F# are not being ubiquitously used in industry. They actually account for a tiny percentage of software development.

But fortunately functional programming concepts have arrived to more mainstream languages such as C++, C#, Rust, Java, Python, and JavaScript. More importantly, a generation of programmers with a functional mindset, give or take, is now working in industry roles.

It feels that only 10-15 years ago, I would still hear everyone preach the virtues of OOP for anything. Thankfully, OOP is now confined to use cases where it actually works well, such as UIs, and maybe a few other places. Sure, Java and C# are still OO. Sure, there are still tons of over-engineered CRUD applications. Programmers are still organising their code in classes. But OOP ideas are not driving the design of their data structures. Not anymore.

In particular, and most importantly, the large majority of software shops now understand the value of immutability. Most applications today are distributed as some sort of services, and therefore most data is typically separated out as a database. This surely helps.

So functional programming has won, even if functional-first languages are not the norm. It is clear that more and more ideas from functional programming are being implemented in mainstream languages.

It is also becoming increasingly clear that static typing is winning. Untyped functional-first language, such as Lisp or Scheme, for all of the love they have been getting, are not winning. Instead, statically-untyped languages, such as Python and JavaScript, which have a functional flavour, are getting static type system. For Python static typing is still in its infancy, but TypeScript seems set to win the JavaScript battle.

But what is next?

My speculation is that type systems will become more and more advanced, with refinement type à la Liquid Haskell coming soon to your favourite language.

In the medium term, I estimate that more verification-based ideas such as invariants, preconditions, and postconditions (à la Dafny) will become integrated into mainstream languages. Interestingly enough, there have already been (failed) tries to get deductive verification into mainstream languages (remember Eiffel? .NET contracts?). I think that they were too early to the market. SMT solvers are becoming much better, hardware is getting fast enough, and programmers are now on average better prepared and ready for this step. Even “AI” assistants may help.

In the longer term, I can only guess that full dependently typed systems await for us.