Functional programming and reliability: ADTs, safety, critical infrastructure(blog.rastrian.dev)
blog.rastrian.dev
Functional programming and reliability: ADTs, safety, critical infrastructure
https://blog.rastrian.dev/post/why-reliability-demands-functional-programming-adts-safety-and-critical-infrastructure
187 comments
Amen. I've been coding a big hobby project in Rust since July, after having spent years using Haskell for such things. I chose Rust because the primary DB I wanted to use (TypeDB) only had drivers for Rust and Python at the time. Rust is popular relative to Haskell, so I thought others might be more likely to sign on, and the type system seemed almost as expressive.
But since purity is not encoded in Rust's type system, any function might do any kind of IO -- in particular, read from or write to disk or one of the DBs. That makes the logic much harder to reason about.
(Also, Rust's syntax is so noisy and verbose that it's harder to see what's going on, and less context fits in my head at one time. I'm getting better at paying that cost, but I wish it weren't there.)
I can't say I made the wrong decision, but I often fantasize about moving most of the logic into Haskell and just calling Rust from Haskell when I need to call TypeDB from Rust.
But since purity is not encoded in Rust's type system, any function might do any kind of IO -- in particular, read from or write to disk or one of the DBs. That makes the logic much harder to reason about.
(Also, Rust's syntax is so noisy and verbose that it's harder to see what's going on, and less context fits in my head at one time. I'm getting better at paying that cost, but I wish it weren't there.)
I can't say I made the wrong decision, but I often fantasize about moving most of the logic into Haskell and just calling Rust from Haskell when I need to call TypeDB from Rust.
Db access in rust typically needs some sort of handle and a mutex. Limiting access to the handle makes the rest of the code pure with respect to the db. The handle plays a similar role to the IO type.
Actor-like patterns makes this nice. Message-objects can be passed to/from a module with db-access or other io.
Actor-like patterns makes this nice. Message-objects can be passed to/from a module with db-access or other io.
this makes me want to move to a haskell (or any hard fp language) shop in 2026..
I've been using Haskell professionally for the last 5 years, I definitely hope I can continue!
Genuinely curious on the types of projects you use Haskell for! I’ve been thinking of learning it beyond the lightweight treatment I got during my CS degree.
Mostly “boring” stuff where the type system pays rent fast:
- Domain/state machines (payments/fulfillment-style workflows): modeling states + transitions so “impossible” states literally can’t be represented. - Parsers/DSLs & config tooling: log parsers, small interpreters, schema validation, migration planners. - Internal CLIs / automation: batch jobs, release helpers, data shapers, anything you want to be correct and easy to refactor later. - Small backend services when the domain is gnarly (Servant / Yesod style) rather than huge monoliths.
If you’re learning it beyond CS exposure, I’d start with a CLI + a parser (JSON/CSV/logs), then add property-based tests (QuickCheck). That combo teaches types, purity, effects, and testing in one project without needing to “go full web stack” on day 1.
- Domain/state machines (payments/fulfillment-style workflows): modeling states + transitions so “impossible” states literally can’t be represented. - Parsers/DSLs & config tooling: log parsers, small interpreters, schema validation, migration planners. - Internal CLIs / automation: batch jobs, release helpers, data shapers, anything you want to be correct and easy to refactor later. - Small backend services when the domain is gnarly (Servant / Yesod style) rather than huge monoliths.
If you’re learning it beyond CS exposure, I’d start with a CLI + a parser (JSON/CSV/logs), then add property-based tests (QuickCheck). That combo teaches types, purity, effects, and testing in one project without needing to “go full web stack” on day 1.
happy to hear that, do you happen to know good places to connect with haskell teams ?
Interesting experience and perhaps not entirely surprising given that type-hole driven development was already a thing prior to LLMs. Like how many ways are there to implement "[a] -> [b] -> [(a,b)]", let alone when you provide a vague description of what that is supposed to do.
minikanren folks were already experimenting with program synthesis given a test suite that needs to be fully satisfied.
I've found it useful in limited cases for writing optics which can be incredibly obtuse, sometimes boilerplatey, and yet ultimately accomplish what in other languages might be considered utterly trivial use cases... consider the following prompt and output:
I suppose LLMs are good for this and other extremely constrained forms of boilerplate production. I consider it an incremental improvement over go codegen. Everything else I still tend to hand-write, because I don't consider source code production the bottleneck of software development.
reply with one-line haskell source code ONLY: implement the function projectPair :: (Field1 s s a a, Field2 s s b b) => Lens s s (a, b) (a, b)
lens (\s -> (s^._1, s^._2)) (\s (a,b) -> s & _1 .~ a & _2 .~ b)
I suppose LLMs are good for this and other extremely constrained forms of boilerplate production. I consider it an incremental improvement over go codegen. Everything else I still tend to hand-write, because I don't consider source code production the bottleneck of software development.
[deleted]
>In banking, telecom, and payments, reliability is not a nice to have. It is table stakes.
This reliability isn't done by being perfect 100% of the time. Things like being able to handle states where transactions don't line up allowing for payments to eventually be settled. Or for telecom allowing for single parts of the system to not take down the whole thing or adding redundancy. Essentially these types of businesses require fault tolerance to be supported. The real world is messy, there is always going to be faults, so investing heavily into correctness may not be worth it compared to investing into fault tollerance.
This reliability isn't done by being perfect 100% of the time. Things like being able to handle states where transactions don't line up allowing for payments to eventually be settled. Or for telecom allowing for single parts of the system to not take down the whole thing or adding redundancy. Essentially these types of businesses require fault tolerance to be supported. The real world is messy, there is always going to be faults, so investing heavily into correctness may not be worth it compared to investing into fault tollerance.
Agree with the framing: in payments/telecom, reliability is often achieved via fault tolerance + reconciliation more than “perfect correctness.”
My point is narrower: those mechanisms still benefit from making illegal transitions unrepresentable (e.g. explicit state machines) so your retries/idempotency don’t create new failure modes. It’s not correctness vs tolerance, it’s correctness inside tolerant designs.
My point is narrower: those mechanisms still benefit from making illegal transitions unrepresentable (e.g. explicit state machines) so your retries/idempotency don’t create new failure modes. It’s not correctness vs tolerance, it’s correctness inside tolerant designs.
False dichotomy.. if reliability matters, you have to invest in both. Fault tolerance is not a replacement for correctness.
You'd like to know your fault tolerance is reliable and possibly even correct.
Not if proving so is more expensive to do than not. Reliability is only a means. Not the end. Also the human parts of the business would need to be simplified in order to model them. If deviate from the model that could invalidate it.
Agree on the economics. I’m not arguing for full formal proofs; I’m arguing for low-cost enforcement of invariants (ADTs/state machines/exhaustiveness) that makes refactors safer and prevents silent invalid states. Human processes will always drift, so you enforce what you can at the system boundary and rely on reconciliation/observability for the rest.
In the banking subdomain of credit/debit/fleet/stored-value card processing, over time when considering regulation and format evolution, services provided by banks/ISOs/VARs will effectively exhibit FP traits regardless the language(s) used to implement them.
Savvy processors recognize the immutability of each API version published to Merchants, along with how long each must be supported, and employ FP techniques both in design and implementation of their Merchant gateways.
Of course, the each bank's mainframes "on the rails" do not change unless absolutely necessary (and many times not even then).
Savvy processors recognize the immutability of each API version published to Merchants, along with how long each must be supported, and employ FP techniques both in design and implementation of their Merchant gateways.
Of course, the each bank's mainframes "on the rails" do not change unless absolutely necessary (and many times not even then).
You can also argue that debugging time can be expensive but static checks reduce debugging. This is much more true when it's concurrency errors.
This article seems to conflate strong type systems with functional programming, except in point 8. It makes sense why- OCaml and Haskell are functional and were early proponents of these type systems. But, languages like Racket don’t have these type systems and the article doesn’t do anything to explain why they are _also_ better for reliability.
Thank you for saying that. I regularly attend the International Conference on Functional Programming, which grew out of the LISP and Functional Programming conference. Except for the Scheme Workshop, which is the reason I attend, it might as well be called the International Conference on Static Types. Almost all of the benefits of functional programming come from functional programming itself, not from static types, but one would never get that impression from the papers presented there. The types are all that anyone talks about.
I get your point about ICFP drifting into “types, types, types.” I don’t think FP benefits are only static typing or immutability, pure-ish core/imperative shell, and explicit effects matter a lot even in dynamic languages.
My angle was narrower: static types + ADTs improve the engineering loop (refactors, code review, test construction) by turning whole classes of mistakes into compiler errors. That’s not “what FP is”, it’s one very effective reliability layer that many FP ecosystems emphasize.
My angle was narrower: static types + ADTs improve the engineering loop (refactors, code review, test construction) by turning whole classes of mistakes into compiler errors. That’s not “what FP is”, it’s one very effective reliability layer that many FP ecosystems emphasize.
Static types and ADTs are orthogonal to being FP, as Rust clearly shows. But to speak in terms of FP when those are the important things for you is just wrong since even non FP languages now have ADT, including also mainstream languages like Java, Kotlin, Dart, C# and more.
Even purity is not something exclusive to FP, D and Nim also support separating pure from impure functions. And if you ask me, the reason not many other languages have support for that is that in practice, it has been demonstrated again and again that it’s just not nearly as useful as you may think. Effects, as in Unison and Flix, generalizes the concept to include many more concepts than just purity and may perhaps prove more useful in general purpose programming, but the jury is still out on this.
Even purity is not something exclusive to FP, D and Nim also support separating pure from impure functions. And if you ask me, the reason not many other languages have support for that is that in practice, it has been demonstrated again and again that it’s just not nearly as useful as you may think. Effects, as in Unison and Flix, generalizes the concept to include many more concepts than just purity and may perhaps prove more useful in general purpose programming, but the jury is still out on this.
Help me with a tl;dr here, but are effects just monads?
Great question! But no, they are not the same, despite some similarities.
In Unison, effects are called abilities, and they wrote a very good post explaining the differences!
https://www.unison-lang.org/docs/fundamentals/abilities/for-...
In summary: both have advantages and disadvantages. Which one is "better" depends on which factors you value more.
In Unison, effects are called abilities, and they wrote a very good post explaining the differences!
https://www.unison-lang.org/docs/fundamentals/abilities/for-...
In summary: both have advantages and disadvantages. Which one is "better" depends on which factors you value more.
I worked through https://htdp.org (which uses untyped Racket), and funny enough, that's what really for me thinking about type driven development. The book gets you to think about and manually annotate the types coming in and out of functions. FP just makes it so natural to think about putting functions together and thinking about the "type" of data that comes in and out, even if you're using a dynamically typed language.
You don't need a strong type system or even really ANY compile-time type system for this strategy to work! I use all these techniques in plain JS and I can still get the benefits of correct-by-construction code style just by freezing objects and failing fast.
You're about a decade too late with that argument. The best argument for dynamic types systems, is enjoying debugging in production.
In dynamic languages, you are the type system.
In dynamic languages, you are the type system.
> The best argument for dynamic types systems, is enjoying debugging in production.
This comment is either severe snark or severe ignorance.
This comment is either severe snark or severe ignorance.
Please, do elaborate...
If you remove passes of a compiler, you, looking at it whilst running, are the compiler.
If you remove passes of a compiler, you, looking at it whilst running, are the compiler.
I agree. So I write tests. I use architecture to defend against the risk of super-rare code paths where I wouldn't rapidly notice if they broke. I dogfood so I find prod bugs before users do.
None of this seems that new. Even people who write TS code still write tests and still ship bugs and still have to think about good architecture patterns, like the ones in the linked post.
None of this seems that new. Even people who write TS code still write tests and still ship bugs and still have to think about good architecture patterns, like the ones in the linked post.
It's a bit ironic that now we went down the static rabbit hole so much that we don't realize it's more the opposite: by adding more to your language and compiler to enforce static checks, you turn the compiler itself more and more into a runtime that you are just going to run ahead of time, according to a potentially vastly different set of rules compared to your real runtime. There is no reason why you couldn't do something like this by will but it's just not worth it after a certain point clearly.
Is this a methodology you use at work or only for personal projects ? I'm curious how common this culture is among companies/teams.
I'm not personally aware of any companies doing this in plain JS aside from my own (I am co-founder/CEO of a two-person startup). I really like working in plain JS. It feels malleable where TS code feels brittle, almost crystalline. Even though I don't have compile-time types there's still only a small handful of different shapes of objects in the core of my software (far fewer than the average TS codebase, I'd wager), and it shouldn't take long at all for people to learn the highly consistent naming conventions that tip you off to what type of data is being handled. The result is that I'd expect that it would only be a handful of days learning the mental model for the codebase before the average person would find it far easier to read the JS code as opposed to TS code, thanks to the lower amount of visual clutter.
I also ship code super fast. When I find bugs I just fix them on the spot. When I find variables named wrong, I just rename them. The result that I often smash bugfixes and features and cleanup together and have a messy git history, but on the flip side you'll never find bugs or naming deceptions that I've left sitting for years. If something is wrong and I can reproduce it (usually easy in functional code), the debugger and I are going to get to the bottom of it, and quickly. Always and only forward!
I also ship code super fast. When I find bugs I just fix them on the spot. When I find variables named wrong, I just rename them. The result that I often smash bugfixes and features and cleanup together and have a messy git history, but on the flip side you'll never find bugs or naming deceptions that I've left sitting for years. If something is wrong and I can reproduce it (usually easy in functional code), the debugger and I are going to get to the bottom of it, and quickly. Always and only forward!
> […] it shouldn't take long at all for people to learn the highly consistent naming conventions that tip you off to what type of data is being handled.
I’ve used languages with an approach like this. The difference in what I’ve used is that you separate the conventional part from the rest of the name with a space (or maybe a colon), then only refer to the value by the non-conventional part for the rest of the scope. Then the language enforces this convention for all of my co-workers! It’s pretty neat.
I’ve used languages with an approach like this. The difference in what I’ve used is that you separate the conventional part from the rest of the name with a space (or maybe a colon), then only refer to the value by the non-conventional part for the rest of the scope. Then the language enforces this convention for all of my co-workers! It’s pretty neat.
I don't get your 2nd sentence: "The difference in what I’ve used" ...
Can you give an example, and name the language used?
Sure! Let’s say I want to enforce that a variable only ever holds an integer. Rather than put the conventional prefix and the name together, like this:
(I hope this makes the joke more obvious.)
var intValue = 3;
int value = 3;
(I hope this makes the joke more obvious.)
I wasn't talking about Hungarian notation. I meant more like if you see a variable named `user` or `activeUser` you know that it's going to contain a predictably-shaped data object that describes a user. E.g. it will always have a `user.id` property. I would never call an string-ish ID a user, then. I would call it `activeUserId` or `userId` or just `id` if the distinction between those was already obvious from context... But that's very different from writing `strUserId` which I never do: I try to make sure my names always convey semantic distinctions.
Mhm! Exactly! In the system those other languages use, once you see the variable’s declaration:
User activeUser
Haha I knew you'd say that. I'm not pretending there aren't advantages to strict systems of declared types. There are many! But my point is simple to the point of stupidity: there's just more stuff on screen when you have to write `User` twice. In this simple example it looks trivially simple to write the word "user" twice, but in a reasonably-complex real example the difference will be far more noticeable.
I should add a few more things: much of how I got here was exposure to Facebook's culture. Move fast and break things. React with prop types. Redux. Immutable.js. I did UI there on internal tools for datacenter operators and it was a drinking-from-the-firehose experience with exposure to new programming philosophies, tools, and levels of abstraction and refactoring velocity beyond anything I had previously encountered. Problems which in other companies I had learn to assume would never be resolved would actually consistently get fixes! Well, at that time. This was before the algorithm was fully enshittified and before the disastrous technopolitical developments in the way facebook and facebook messenger interact with each other.
Perhaps the most direct inspiration I took from there though was from the wonderful "opaque types" feature that Flow supports (https://flow.org/en/docs/types/opaque-types/) which for reasons known only to Hejlsberg and God, Typescript has never adopted; thus most people are unfamiliar with that way of thinking.
Perhaps the most direct inspiration I took from there though was from the wonderful "opaque types" feature that Flow supports (https://flow.org/en/docs/types/opaque-types/) which for reasons known only to Hejlsberg and God, Typescript has never adopted; thus most people are unfamiliar with that way of thinking.
Yes, I am wondering if opaque types would be difficult to implement somehow in TypeScript? It should really be part of TypeScript if at all reasonably possible.
I'm not that familiar with the TS internals. They'd have to add a keyword to the language which could break stuff. The smart move would be to reserve the `opaque` word a few versions in advance of introducing the feature that gives it a meaning
I don't think the keyword is the problem, I am wondering more about the internals of their type inference algorithm.
godspeed with that :)
I've seen it pointed out that the main point of functional programming is immutability, and that the benefits mostly flow from that. I haven't really learned much of any lisp dialect, but my (admittedly fuzzy) general perception is that this is also the preferred way to work in them, so my guess is that's where the benefit in reliability might come from.
Correct. If things are mutable, then in most languages, there can be spooky action at a distance, that mutates some field of some other object or does so indirectly via some calls. This then can change how the thing behaves in other circumstances. This style of programming quickly becomes hard to fully grasp and leads to humans making many mistakes. Avoiding mutation therefore avoids these kinds of faults and mistakes.
Agreed, I conflated FP with “typed FP.” My claim is mainly about static types + ADTs/exhaustiveness improving refactors/review/tests. Racket can get FP benefits, but absent static typing you rely more on contracts/tests (or Typed Racket), which is a different reliability tradeoff.
The term "functional programming" is so ill-defined as to be effectively useless in any kind of serious conversation. I'm not aware of any broadly accepted consensus definition. Sometimes people want to use this category to talk about purity and control of side effects and use the term "functional programming" to refer to that. I would advocate the more targeted term "pure functional programming" for that definition. But in general I try to avoid the term altogether, and instead talk about specific language features / capabilities.
> The term "functional programming" is so ill-defined as to be effectively useless in any kind of serious conversation.
This is important. I threw my hands up and gave up during the height of the Haskell craze. You'd see people here saying things like LISP wasn't real FP because it didn't match their Haskell-colored expectations. Meanwhile for decades LISP was *the* canonical example of FP.
Similar to you, now I talk about specific patterns and concepts instead of calling a language functional. Also, as so many of these patterns & concepts have found their way into mainstream languages now, that becomes even more useful.
This is important. I threw my hands up and gave up during the height of the Haskell craze. You'd see people here saying things like LISP wasn't real FP because it didn't match their Haskell-colored expectations. Meanwhile for decades LISP was *the* canonical example of FP.
Similar to you, now I talk about specific patterns and concepts instead of calling a language functional. Also, as so many of these patterns & concepts have found their way into mainstream languages now, that becomes even more useful.
To your point, but lispers like the author of Let Over Lambda specifically called Lisp non-functional.
to add a grain of salt, some of the lisp world is not functional, a lot of code is straight up imperative / destructive. but then yeah a lot of the lisp culture tended to applicative idioms and function oriented, even without the static explicit generic type system of haskell.
Sure, but that's part of my point in agreeing that definitions of "functional programming" are muddy at best. If one were to go back to say 1990 and poll people to name the first "functional programming" language that comes to mind, I'd wager nearly all of them would say something like LISP or Scheme. It really wasn't until the late aughts/early teens when that started to shift.
Yeah sorry i wasn't bringing much by commenting this above. And yeah lisp was the historical soil for FP (schemers took the lead on this).
No I think your point is good, it just wasn't contradictory and I think that was your intent. Defining FP is a dark art :)
maybe FP should be explained as `rules not values`. in scheme it's common to negate the function to be applied, or curry some expression or partially compose / thread rules/logic to get a potential future value that did nothing yet
I like it. I think I said this in a separate post in here but I've taken to breaking it down to different archetypes and discussing them separately.
I usually define functional programming as "how far away a language is from untyped lambda calculus". By that definition, different languages would fall in different parts of that spectrum.
Yeah, I know Rust isn’t everyone’s favorite but I’d expect at least some awareness that we’ve seen a lot of reliability improvements due to many of these ideas in a language which isn’t focused on FP. I ended up closing the tab when they had the example in TypeScript pretending the fix was result types rather than validation: that idea could be expressed as preferring that style, an argument that it makes oversights less likely, etc. but simply ignoring decades and decades of prior art suggests the author either isn’t very experienced or is mostly motivated by evangelism (e.g. COBOL didn’t suffer from the example problem before the first FP language existed so a far more interesting discussion would be demonstrating awareness of alternatives and explaining why this one is better).
Rust certainly isn't a pure fp language, but the borrow checkerbl is a lot kinder when you use fp style.
Sure, my point was simply that it’s not as simple as the author assumes. This is a common failure mode in FP advocacy and it’s disappointing because it usually means that a more interesting conversation doesn’t happen because most readers disengage.
I get why it reads like FP evangelism, but I don’t think it’s “ignoring decades of prior art.” I’m not claiming these ideas are exclusive to FP. I’m claiming FP ecosystems systematized a bundle of practices (ADT/state machines, exhaustiveness, immutability, explicit effects) that consistently reduce a specific failure mode: invalid state transitions and refactor breakage.
Rust is actually aligned with the point: it delivers major reliability wins via making invalid states harder to represent (enums, ownership/borrowing, pattern matching). That’s not “FP-first,” but it’s very compatible with functional style and the same invariants story.
If the TS example came off as “types instead of validation,” that’s on me to phrase better, the point wasn’t “types eliminate validation,” it’s “types make the shape explicit so validation becomes harder to forget and easier to review.”
Rust is actually aligned with the point: it delivers major reliability wins via making invalid states harder to represent (enums, ownership/borrowing, pattern matching). That’s not “FP-first,” but it’s very compatible with functional style and the same invariants story.
If the TS example came off as “types instead of validation,” that’s on me to phrase better, the point wasn’t “types eliminate validation,” it’s “types make the shape explicit so validation becomes harder to forget and easier to review.”
I would keep in mind how much the title communicates your intentions on future posts. The conversation about preventing invalid states has to be somewhat inferred when it could have been explicitly stated, and that’d be really useful comparing other approaches - e.g. the classic OOP style many people learned in school also avoid these problems as would something like modern Python using Pydantic/msgspec so it’d be useful to discuss differences in practice, and especially with a larger scope so people who don’t already agree with you can see how you came to that position.
For example, using the input parsing scenario, a Java 1.0 tutorial in 1995 would have said that you should create a TimeDuration class which parses the input and throws an exception when given an invalid value like “30s”. If you say that reliability requires FP, how would you respond when they point out that their code also prevents running with an invalid value? That discussion can be far more educational, especially because it might avoid derails around specific issues which are really just restating the given that JavaScript had lots of footgun opportunities for the unwary developer, even compared to some languages their grandmother might have used.
For example, using the input parsing scenario, a Java 1.0 tutorial in 1995 would have said that you should create a TimeDuration class which parses the input and throws an exception when given an invalid value like “30s”. If you say that reliability requires FP, how would you respond when they point out that their code also prevents running with an invalid value? That discussion can be far more educational, especially because it might avoid derails around specific issues which are really just restating the given that JavaScript had lots of footgun opportunities for the unwary developer, even compared to some languages their grandmother might have used.
Once you accept Curry-Howard, untyped FP languages are hard to take seriously as a foundation for reliability. Curry-Howard changes the entire game. FP and strong types were clearly meant for each other.
Untyped FP languages can be productive, flexible, even elegant (I guess) but they are structurally incapable of expressing large classes of correctness claims that typed FP makes routine.
That doesn’t make them useless, just, you know. Inferior.
Untyped FP languages can be productive, flexible, even elegant (I guess) but they are structurally incapable of expressing large classes of correctness claims that typed FP makes routine.
That doesn’t make them useless, just, you know. Inferior.
> In banking, telecom, and payments, reliability is not a nice to have. It is table stakes.
Haha as someone who has worked in one of these domains using FP even - I wish the people in charge agreed with you!
Reliability is a cost center and Product-oriented Builders treat it as such.
Haha as someone who has worked in one of these domains using FP even - I wish the people in charge agreed with you!
Reliability is a cost center and Product-oriented Builders treat it as such.
Yep, in practice a lot of orgs treat reliability as a cost center until an outage becomes a headline or a regulatory incident. I’ve seen the same tension in payments/banking: product pressure wins until the risk is visible.
Part of why I like “make invalid states unrepresentable” approaches is exactly that: it’s one of the few reliability investments that can pay back during feature work (safer refactors, fewer regressions), not only during incidents.
Part of why I like “make invalid states unrepresentable” approaches is exactly that: it’s one of the few reliability investments that can pay back during feature work (safer refactors, fewer regressions), not only during incidents.
I've seen reliability become incident level and then 3mo later execs are on our ass because we didn't fix another crisis fast enough.
and this company is hugely successful. so i've learned that the biggest competitive advantage in fintech is flagrant disregard for correctness and compliance.
i'm glad i have a csuite with the stones to execute that. i am way too principled.
and this company is hugely successful. so i've learned that the biggest competitive advantage in fintech is flagrant disregard for correctness and compliance.
i'm glad i have a csuite with the stones to execute that. i am way too principled.
Honestly, as someone else who does a lot of data plumbing, there is so much FTP servers with excel sheets being used as the means for official clearance processes.
There are constant data bugs in the feeds provided by major exchanges, market makers, etc, and so many iffy business rules that are basically all encoded in 100+ tab excel sheets.
Maybe this article focuses on a very specific niche of banking, but most of it is tied together with FTP and excel sheets.
I think the author would be shocked just how flaky a fundamental banking protocol like SWIFT is.
There are constant data bugs in the feeds provided by major exchanges, market makers, etc, and so many iffy business rules that are basically all encoded in 100+ tab excel sheets.
Maybe this article focuses on a very specific niche of banking, but most of it is tied together with FTP and excel sheets.
I think the author would be shocked just how flaky a fundamental banking protocol like SWIFT is.
I’ve worked in Brazilian banking stacks that were literally FTP + spreadsheets for years. So yes, the ecosystem is often messy and protocols can be flaky.
That’s exactly why I argue for stronger internal modeling: when the boundary is dirty, explicit state machines/ADTs + exhaustiveness + idempotency/reconciliation help ensure bad feeds don’t silently create invalid internal states.
That’s exactly why I argue for stronger internal modeling: when the boundary is dirty, explicit state machines/ADTs + exhaustiveness + idempotency/reconciliation help ensure bad feeds don’t silently create invalid internal states.
I totally agree as a fellow fintech engineer. It was a battle getting approval for all that from Product for us. While we were battling for it, we rushed multiple projects without literally any of it. And then spent a year+ each time cleaning up the mess.
And your pockets were being filled in that year while you were just doing cleanups. Mission accomplished.
Perhaps someone can enlighten me on this. I never quite understood the sentiment of treating money-related tech as somehow more critical than others. The effects of large SaaS services failing and the bank failing can be quite similar - businesses interrupted, money lost, etc. but it’s typically not life and death, so the importance of reliability should be similar.
I can understand treating social network sites as less critical, of course.
I can understand treating social network sites as less critical, of course.
I mostly agree: for many businesses, a big SaaS outage and a payments outage can look similar in impact (lost revenue, interrupted operations). It’s not “life or death” most of the time.
The reason money-related systems often get singled out is the combination of irreversibility and auditability: a bad state transition can mean incorrect balances/settlement, messy reconciliation, regulatory reporting, and long-tail customer harm that persists after the outage is over.
That said, my point isn’t “finance is special therefore FP.” It’s “build resilience and correctness by design early”, explicit state machines/invariants, idempotency/reconciliation, and making invalid states hard to represent. Doing this from the beginning also improves the developer experience: safer refactors, clearer reviews, fewer ‘tribal knowledge’ bugs.
The reason money-related systems often get singled out is the combination of irreversibility and auditability: a bad state transition can mean incorrect balances/settlement, messy reconciliation, regulatory reporting, and long-tail customer harm that persists after the outage is over.
That said, my point isn’t “finance is special therefore FP.” It’s “build resilience and correctness by design early”, explicit state machines/invariants, idempotency/reconciliation, and making invalid states hard to represent. Doing this from the beginning also improves the developer experience: safer refactors, clearer reviews, fewer ‘tribal knowledge’ bugs.
Losses with money are easiest to prove thus easiest to litigate. And then also potentially prosecute. Money is in the end most of time reconcilable at the end. So any mistakes can be proven.
In other areas like lost sales or failures of the system there is lot more arguments. On other hand if you are rich enough and can prove the other side is off by sufficiently large amount of money you can bring the hammer down with facts.
In other areas like lost sales or failures of the system there is lot more arguments. On other hand if you are rich enough and can prove the other side is off by sufficiently large amount of money you can bring the hammer down with facts.
Compare discussions about banking with discussions about evoting ! One is totally fine for software to handle, the other is absolutely not!! That tells you which one people really consider critical.
It's acceptable to state, without evidence, that functional programming and static typing make things more reliable.
But this isn't a falsifiable claim. We cannot possibly know if this is true or not.
- Not all of banking and telecom use functional programming or even static typing.
- Functional programming often leads to write-only incomprehensible code; the exact opposite of what you need to have a reliable system.
- There's no hard evidence that static typing improves reliability. Only vibes and feels.
But this isn't a falsifiable claim. We cannot possibly know if this is true or not.
- Not all of banking and telecom use functional programming or even static typing.
- Functional programming often leads to write-only incomprehensible code; the exact opposite of what you need to have a reliable system.
- There's no hard evidence that static typing improves reliability. Only vibes and feels.
Wait. This doesn’t make sense to me. Statically typed programming languages cannot be deployed nor can they run with a type error that happens at runtime. Untyped languages CAN run and error out with a type error AT runtime. The inevitable consequence of that truth is this:
In the spectrum of runtime errors statically typed languages mathematically and logically HAVE less errors. That by itself is the definition of more reliable. This isn’t even a scientific thing related to falsifiability. This comes from pure mathematical logic. In science nothing can be proven, things can only be falsified. But in math and logic things can be proven and it is provable that static types are more reliable than untyped.
It is definitely not vibes and feels. Not all of banking uses statically typed languages but they are as a result living with a less reliable system then the alternative and that is a logical invariant.
There are many reasons why someone would choose untyped over typed but reliability is not a reason why they would do this unless they are ignorant.
In the spectrum of runtime errors statically typed languages mathematically and logically HAVE less errors. That by itself is the definition of more reliable. This isn’t even a scientific thing related to falsifiability. This comes from pure mathematical logic. In science nothing can be proven, things can only be falsified. But in math and logic things can be proven and it is provable that static types are more reliable than untyped.
It is definitely not vibes and feels. Not all of banking uses statically typed languages but they are as a result living with a less reliable system then the alternative and that is a logical invariant.
There are many reasons why someone would choose untyped over typed but reliability is not a reason why they would do this unless they are ignorant.
> Statically typed programming languages cannot be deployed nor can they run with a type error that happens at runtime.
This is so completely untrue that I'm confused as to why anyone would try to claim it. Type Confusion is an entire class of error and CVE that happens in statically typed languages. Java type shenanigans are endless if you want some fun but baseline you can cast to arbitrary types at runtime and completely bypass all compile time checks.
I think the disagreement would come additionally by saying a language like Ruby doesn't actually have any type errors. Like how it can be said that GC languages can't have memory leaks. And that this model is stronger than just compile time checking. Sure you get a thing called TypeError in Ruby but because of the languages dynamism that's not an error the way it would be in C. You can just catch it and move. It doesn't invalidate the program's correctness. Ruby is so safe in it's execution model that Syntax Errors don't invalidate the running program's soundness.
This is so completely untrue that I'm confused as to why anyone would try to claim it. Type Confusion is an entire class of error and CVE that happens in statically typed languages. Java type shenanigans are endless if you want some fun but baseline you can cast to arbitrary types at runtime and completely bypass all compile time checks.
I think the disagreement would come additionally by saying a language like Ruby doesn't actually have any type errors. Like how it can be said that GC languages can't have memory leaks. And that this model is stronger than just compile time checking. Sure you get a thing called TypeError in Ruby but because of the languages dynamism that's not an error the way it would be in C. You can just catch it and move. It doesn't invalidate the program's correctness. Ruby is so safe in it's execution model that Syntax Errors don't invalidate the running program's soundness.
> Java type shenanigans are endless if you want some fun but baseline you can cast to arbitrary types at runtime and completely bypass all compile time checks.
For this reason Java is a bad example of a typed language. It gives static typing a bad rep because of its inflexible yet unreliable type system (only basic type inference, no ADTs, many things like presence of equality not checked at compile time etc ) Something like ocaml or fsharp have much more sound and capable type systems.
For this reason Java is a bad example of a typed language. It gives static typing a bad rep because of its inflexible yet unreliable type system (only basic type inference, no ADTs, many things like presence of equality not checked at compile time etc ) Something like ocaml or fsharp have much more sound and capable type systems.
Like other people replying to you C++ and Java gave types a bad rep by being so error prone and having a weak type system.
What I am saying is not untrue. It is definitive. Java just has a broken type system and it has warped your view. The article is more talking about type systems from functional programming languages where type errors are literally impossible.
You should check out elm. It’s one of the few languages (that is not a toy language and is deployed to production) where the type system is so strong that run time errors are impossible. You cannot crash an elm program because the type system doesn’t allow it. If you used that or Haskell for a while in a non trivial way it will give you deeper insight into why types matter.
> Ruby is so safe in it's execution model that Syntax Errors don't invalidate the running program's soundness.
This isn’t safety. Safety is when the program doesn’t even run or compile with a syntax error. Imagine if programs with syntax errors still tried their best effort to run… now you have a program with unknown behavior because who knows what that program did with the syntax error? Did it ignore it? Did it try to correct it? Now imagine that ruby program controlling a plane. That’s not safe.
What I am saying is not untrue. It is definitive. Java just has a broken type system and it has warped your view. The article is more talking about type systems from functional programming languages where type errors are literally impossible.
You should check out elm. It’s one of the few languages (that is not a toy language and is deployed to production) where the type system is so strong that run time errors are impossible. You cannot crash an elm program because the type system doesn’t allow it. If you used that or Haskell for a while in a non trivial way it will give you deeper insight into why types matter.
> Ruby is so safe in it's execution model that Syntax Errors don't invalidate the running program's soundness.
This isn’t safety. Safety is when the program doesn’t even run or compile with a syntax error. Imagine if programs with syntax errors still tried their best effort to run… now you have a program with unknown behavior because who knows what that program did with the syntax error? Did it ignore it? Did it try to correct it? Now imagine that ruby program controlling a plane. That’s not safe.
There are different levels of static typing
> Wait. This doesn’t make sense to me. Statically typed programming languages cannot be deployed nor can they run with a type error that happens at runtime. Untyped languages CAN run and error out with a type error AT runtime. The inevitable consequence of that truth is this
There is nothing inevitable about the consequence you’re imagining because statically typed languages also reject correct programs.
There is nothing inevitable about the consequence you’re imagining because statically typed languages also reject correct programs.
It is 100 percent inevitable. Your reasoning here is illogical.
How does a statically typed language rejecting a correct program affect reliability? The two concepts are orthogonal. You’re talking about flexibility of a language but the topic is on reliability.
Let me be clear… as long as a language is Turing complete you can get it to accomplish virtually any task. In a statically typed language you have less ways to accomplish the same task then a dynamically typed language; but both languages can accomplish virtually any task. By logic a dynamically typed language is categorically more flexible than a static one but it is also categorically less reliable.
How does a statically typed language rejecting a correct program affect reliability? The two concepts are orthogonal. You’re talking about flexibility of a language but the topic is on reliability.
Let me be clear… as long as a language is Turing complete you can get it to accomplish virtually any task. In a statically typed language you have less ways to accomplish the same task then a dynamically typed language; but both languages can accomplish virtually any task. By logic a dynamically typed language is categorically more flexible than a static one but it is also categorically less reliable.
>How does a statically typed language rejecting a correct program affect reliability?
Because in some cases it will reject code that is simple and obviously correct, which will then need to be replaced by code that is less simple and less obviously correct (but which satisfies the type checker). I don't think this happens most of the time, but it does mean that static typing isn't a strict upgrade in terms of reliability. You are paying for the extra guarantees on the code you can write by giving up lots of correct programs that you could otherwise have written.
Because in some cases it will reject code that is simple and obviously correct, which will then need to be replaced by code that is less simple and less obviously correct (but which satisfies the type checker). I don't think this happens most of the time, but it does mean that static typing isn't a strict upgrade in terms of reliability. You are paying for the extra guarantees on the code you can write by giving up lots of correct programs that you could otherwise have written.
>I don't think this happens most of the time, but it does mean that static typing isn't a strict upgrade in terms of reliability.
It is a strict upgrade in reliability. You're arguing for other benefits here, like readability and simplicity. The metric on topic is reliability and NOT other things like simplicity, expressiveness or readability. Additionally, like you said, it doesn't happen "most" of the time, so even IF we included those metrics in the topic of conversation your argument is not practical.
>You are paying for the extra guarantees on the code you can write by giving up lots of correct programs that you could otherwise have written.
Again the payment is orthogonal to the benefit. The benefit is reliability. The payment is simplicity, flexibility, expressiveness, and readability. For me, personally, (and you as you've seem to indicate) programs actually become more readable and more simple when you add types. Expressiveness and flexibility is actually a foot gun, but that's not an argument I'm making as these are more opinions and therefore unprovable. You're free to feel differently.
My argument is that in the totality of possible errors, statically typed programs have provably LESS errors and thus are definitionally MORE reliable than untyped programs. I am saying that there is ZERO argument here, and that it is mathematical fact. No amount of side stepping out of the bounds of the metric "reliability" will change that.
It is a strict upgrade in reliability. You're arguing for other benefits here, like readability and simplicity. The metric on topic is reliability and NOT other things like simplicity, expressiveness or readability. Additionally, like you said, it doesn't happen "most" of the time, so even IF we included those metrics in the topic of conversation your argument is not practical.
>You are paying for the extra guarantees on the code you can write by giving up lots of correct programs that you could otherwise have written.
Again the payment is orthogonal to the benefit. The benefit is reliability. The payment is simplicity, flexibility, expressiveness, and readability. For me, personally, (and you as you've seem to indicate) programs actually become more readable and more simple when you add types. Expressiveness and flexibility is actually a foot gun, but that's not an argument I'm making as these are more opinions and therefore unprovable. You're free to feel differently.
My argument is that in the totality of possible errors, statically typed programs have provably LESS errors and thus are definitionally MORE reliable than untyped programs. I am saying that there is ZERO argument here, and that it is mathematical fact. No amount of side stepping out of the bounds of the metric "reliability" will change that.
Your definition of reliability seems different to how people use the word. I think most would consider a program that was statically checked, but often produces a wrong result as less reliable than a dynamically checked program that produces the right result.
>My argument is that in the totality of possible errors, statically typed programs have provably LESS errors and thus are definitionally MORE reliable than untyped programs. I am saying that there is ZERO argument here, and that it is mathematical fact. No amount of side stepping out of the bounds of the metric "reliability" will change that.
Making such broad statements about the real world with 100% confidence should already raise some eyebrows. Even through the lens of math and logic, it is unclear how to interpret your argument. Are you claiming that sum of all possible errors in all runnable programs in a statically checked language is less than sum of all possible errors in all runnable programs in an equivalent dynamically checked language? Both of those numbers are infinity, although i remember from school that some infinities are greater than others, I'm not sure how to prove that. And if such statement was true, how does it affect programs written in the real world?
Or is your claim that a randomly picked program from the set of all runnable statically checked programs is expected to have less errors than randomly picked program from the set of all runnable dynamically checked programs? Even this statement doesn't seem trivial, due to correct programs being rejected by type checker.
If your claim is about real world programs being written, you also have to consider that their distribution among the set of all runnable programs is not random. The amount of time, attention span and other resources is often limited. Consider the act of twisting an already correct program in various ways to satisfy the type checker, Consider the time lost that could be invested in further verifying the logic. The result will be much less clear cut, more probabilistic, more situation-dependent etc.
>My argument is that in the totality of possible errors, statically typed programs have provably LESS errors and thus are definitionally MORE reliable than untyped programs. I am saying that there is ZERO argument here, and that it is mathematical fact. No amount of side stepping out of the bounds of the metric "reliability" will change that.
Making such broad statements about the real world with 100% confidence should already raise some eyebrows. Even through the lens of math and logic, it is unclear how to interpret your argument. Are you claiming that sum of all possible errors in all runnable programs in a statically checked language is less than sum of all possible errors in all runnable programs in an equivalent dynamically checked language? Both of those numbers are infinity, although i remember from school that some infinities are greater than others, I'm not sure how to prove that. And if such statement was true, how does it affect programs written in the real world?
Or is your claim that a randomly picked program from the set of all runnable statically checked programs is expected to have less errors than randomly picked program from the set of all runnable dynamically checked programs? Even this statement doesn't seem trivial, due to correct programs being rejected by type checker.
If your claim is about real world programs being written, you also have to consider that their distribution among the set of all runnable programs is not random. The amount of time, attention span and other resources is often limited. Consider the act of twisting an already correct program in various ways to satisfy the type checker, Consider the time lost that could be invested in further verifying the logic. The result will be much less clear cut, more probabilistic, more situation-dependent etc.
I think the disagreement here comes from overcomplicating what is actually a very simple claim.
I am not reasoning about infinities, cardinalities of infinite sets, or expectations over randomly sampled programs. None of that is needed. You do not need infinities to see that one set is smaller than another. You only need to show that one set contains everything the other does, plus more.
Forget “all possible programs” and forget randomness entirely. We only need to reason about possible runtime outcomes under identical conditions.
Take a language and hold everything constant except static type checking. Same runtime, same semantics, same memory model, same expressiveness. Now ask a very concrete question: what kinds of failures can occur at runtime?
In the dynamically typed variant, there exist programs that execute and then fail with a runtime type error. In the statically typed variant, those same programs are rejected before execution and therefore never produce that runtime failure. Meanwhile, any program that executes successfully in the statically typed variant also executes successfully in the dynamic one. Nothing new can fail in the static case with respect to type errors.
That is enough. No infinities are involved. No counting is required. If System A allows a category of runtime failure that System B forbids entirely, then the set of possible runtime failure states in B is strictly smaller than in A. This is simple containment logic, not higher math.
The “randomly picked program” framing is a red herring. It turns this into an empirical question about distributions, likelihoods, and developer behavior. But the claim is not about what is likely to happen in practice. It is about what can happen at all, given the language definition. The conclusion follows without measuring anything.
Similarly, arguments about time spent satisfying the type checker or opportunity cost shift the discussion to human workflow. Those may matter for productivity, but they are not properties of the language’s runtime behavior. Once you introduce them, you are no longer evaluating reliability under identical technical conditions.
On the definition of reliability: the specific word is not doing the work here. Once everything except typing is held constant, all other dimensions are equal by assumption. There is literally nothing else left to compare. What remains is exactly one difference: whether a class of runtime failures exists at all. At that point, reliability reduces to failure modes not by preference or definition games, but because there is no other remaining axis. I mean everything is the same! What else can you compare if not the type errors? Then ask the question which one is more reliable? Well… everything is the same except one has run time type errors, while the other doesn’t… which one would you call more “reliable”? The answer is obvious.
So the claim is not that statically typed languages produce correct programs or better engineers. The claim is much narrower and much stronger: holding everything else fixed, static typing removes a class of runtime failures that dynamic typing allows. That statement does not rely on infinities, randomness, or empirical observation. It follows directly from what static typing is.
I am not reasoning about infinities, cardinalities of infinite sets, or expectations over randomly sampled programs. None of that is needed. You do not need infinities to see that one set is smaller than another. You only need to show that one set contains everything the other does, plus more.
Forget “all possible programs” and forget randomness entirely. We only need to reason about possible runtime outcomes under identical conditions.
Take a language and hold everything constant except static type checking. Same runtime, same semantics, same memory model, same expressiveness. Now ask a very concrete question: what kinds of failures can occur at runtime?
In the dynamically typed variant, there exist programs that execute and then fail with a runtime type error. In the statically typed variant, those same programs are rejected before execution and therefore never produce that runtime failure. Meanwhile, any program that executes successfully in the statically typed variant also executes successfully in the dynamic one. Nothing new can fail in the static case with respect to type errors.
That is enough. No infinities are involved. No counting is required. If System A allows a category of runtime failure that System B forbids entirely, then the set of possible runtime failure states in B is strictly smaller than in A. This is simple containment logic, not higher math.
The “randomly picked program” framing is a red herring. It turns this into an empirical question about distributions, likelihoods, and developer behavior. But the claim is not about what is likely to happen in practice. It is about what can happen at all, given the language definition. The conclusion follows without measuring anything.
Similarly, arguments about time spent satisfying the type checker or opportunity cost shift the discussion to human workflow. Those may matter for productivity, but they are not properties of the language’s runtime behavior. Once you introduce them, you are no longer evaluating reliability under identical technical conditions.
On the definition of reliability: the specific word is not doing the work here. Once everything except typing is held constant, all other dimensions are equal by assumption. There is literally nothing else left to compare. What remains is exactly one difference: whether a class of runtime failures exists at all. At that point, reliability reduces to failure modes not by preference or definition games, but because there is no other remaining axis. I mean everything is the same! What else can you compare if not the type errors? Then ask the question which one is more reliable? Well… everything is the same except one has run time type errors, while the other doesn’t… which one would you call more “reliable”? The answer is obvious.
So the claim is not that statically typed languages produce correct programs or better engineers. The claim is much narrower and much stronger: holding everything else fixed, static typing removes a class of runtime failures that dynamic typing allows. That statement does not rely on infinities, randomness, or empirical observation. It follows directly from what static typing is.
Readability and simplicity can increase reliability, because simple readable code is easier to review.
From a practical perspective, most programmers will agree with me when I say that static types are more readable.
Sure. That’s a different kind of argument from the absolutist argument you were making earlier.
Right and it’s completely off topic. This is a tangent you decided to turn the conversation toward. Tangents are fine, I’m just saying that you are wrong on both the main topic and the tangent, which is also fine.
The point is that a dynamic language will in some cases enable code that is simpler and more readable (and hence probably more reliable) because sometimes the simplest code is code that wouldn’t type check. Even if statically typed languages are more readable on average, this fact invalidates your claim that statically typed languages are strictly better in terms of reliability. This can only be true if you artificially restrict attention to the subset of programs in the dynamic language that could have been statically typed.
By the way, could you tone down the rhetoric a notch?
By the way, could you tone down the rhetoric a notch?
My claim is not invalid. It’s just being evaluated against a different question.
The original post says that claims like “static typing improves reliability” are unfalsifiable and therefore just vibes. That’s false, because the claim being made is not empirical to begin with. It’s a statement about language semantics.
Holding everything else constant, static typing eliminates a class of runtime failures by construction. Programs that would fail at runtime with type errors in a dynamic language are rejected before execution in a statically typed one. That is not a hypothesis about the real world, teams, or productivity. It’s a direct consequence of what static typing is. No evidence or falsification is required.
When you argue that dynamic languages can sometimes enable simpler or more readable code that may be more reliable in practice, you’ve changed the claim. That’s a discussion about human factors and development process. It may be true, but it does not invalidate the original claim, because it addresses a different level of analysis.
Additionally in practice it isn’t true. Your entire argument flips context and is trying to point out a niche corner case to show that my overall correct argument is not absolute. You’re already wrong practically, and you’re also wrong absolutely.
So the correct framing is:
- At the language level, static typing is strictly more reliable with respect to runtime type errors.
- At the human/process level, tradeoffs exist, and outcomes can vary.
Calling the first claim “invalid” only works if you silently replace it with the second. That’s the source of the disagreement.
The original post says that claims like “static typing improves reliability” are unfalsifiable and therefore just vibes. That’s false, because the claim being made is not empirical to begin with. It’s a statement about language semantics.
Holding everything else constant, static typing eliminates a class of runtime failures by construction. Programs that would fail at runtime with type errors in a dynamic language are rejected before execution in a statically typed one. That is not a hypothesis about the real world, teams, or productivity. It’s a direct consequence of what static typing is. No evidence or falsification is required.
When you argue that dynamic languages can sometimes enable simpler or more readable code that may be more reliable in practice, you’ve changed the claim. That’s a discussion about human factors and development process. It may be true, but it does not invalidate the original claim, because it addresses a different level of analysis.
Additionally in practice it isn’t true. Your entire argument flips context and is trying to point out a niche corner case to show that my overall correct argument is not absolute. You’re already wrong practically, and you’re also wrong absolutely.
So the correct framing is:
- At the language level, static typing is strictly more reliable with respect to runtime type errors.
- At the human/process level, tradeoffs exist, and outcomes can vary.
Calling the first claim “invalid” only works if you silently replace it with the second. That’s the source of the disagreement.
Also Did you read what I wrote? I Covered your argument here DIRECTLY in my response. It's like you read the first sentence and then responded while ignoring the next paragraph.
This logic is both too broad and rigid to be of much practical use[1]. It needs to be tightened to compare languages that are identical except for static type checks, otherwise the statically typed language could admit other kinds of errors (memory errors immediately come to mind) that many dynamic languages do not have and you would need some way of weighing the relative cost to reliability of the different categories of errors.
Even if the two languages are identical except for the static types, then it is clearly possible to write programs that do not have any runtime type errors in the dynamic language (I'll leave it as an exercise to the reader to prove this but it is very clearly true) so there exist programs in any dynamic language that are equally reliable to their static counterpart.
[1] I also disagree with your definition of reliability but I'm granting it for the sake of discussion.
Even if the two languages are identical except for the static types, then it is clearly possible to write programs that do not have any runtime type errors in the dynamic language (I'll leave it as an exercise to the reader to prove this but it is very clearly true) so there exist programs in any dynamic language that are equally reliable to their static counterpart.
[1] I also disagree with your definition of reliability but I'm granting it for the sake of discussion.
You’re objecting on the wrong axis.
The claim was about reliability and lack of empirical evidence. Once framed that way, definitions matter. My argument is purely ceteris paribus: take a language, hold everything constant, and add strict static type checking. Once you do that, every other comparison disappears by definition. Same runtime, same semantics, same memory model, same expressiveness. The only remaining difference is the runtime error set.
Static typing rejects at compile time a strict subset of programs that would otherwise run and fail with runtime type errors. That is not an empirical claim; it follows directly from the definition of static typing. This is not hypothetical either. TypeScript vs JavaScript, or Python vs Python with a sound type checker, are real examples of exactly this transformation. The error profile is identical except the typed variant admits fewer runtime failures.
Pointing out that some dynamic programs have no runtime type errors does not contradict this. It only shows that individual programs can be equally reliable. The asymmetry is at the language level: it is impossible to deploy a program with runtime type errors in a sound statically typed language, while it is always possible in a dynamically typed one. That strictly reduces the space of possible runtime failures.
Redefining “reliability” does not change the result. Suppose reliability is expanded to include readability, maintainability, developer skill, team discipline, or development velocity. Those may matter in general, but they are not variables in this comparison. By construction, everything except typing is held constant. There is literally nothing else left to compare. All non-type-related factors are identical by assumption. What remains is exactly one difference: the presence or absence of runtime type errors. At that point, reliability reduces to failure count not as a philosophical choice, but because there is no other dimension remaining.
Between two otherwise identical systems, the one that can fail in fewer ways at runtime is more reliable. That conclusion is not empirical, sociological, or debatable. It follows directly from the setup.
The claim was about reliability and lack of empirical evidence. Once framed that way, definitions matter. My argument is purely ceteris paribus: take a language, hold everything constant, and add strict static type checking. Once you do that, every other comparison disappears by definition. Same runtime, same semantics, same memory model, same expressiveness. The only remaining difference is the runtime error set.
Static typing rejects at compile time a strict subset of programs that would otherwise run and fail with runtime type errors. That is not an empirical claim; it follows directly from the definition of static typing. This is not hypothetical either. TypeScript vs JavaScript, or Python vs Python with a sound type checker, are real examples of exactly this transformation. The error profile is identical except the typed variant admits fewer runtime failures.
Pointing out that some dynamic programs have no runtime type errors does not contradict this. It only shows that individual programs can be equally reliable. The asymmetry is at the language level: it is impossible to deploy a program with runtime type errors in a sound statically typed language, while it is always possible in a dynamically typed one. That strictly reduces the space of possible runtime failures.
Redefining “reliability” does not change the result. Suppose reliability is expanded to include readability, maintainability, developer skill, team discipline, or development velocity. Those may matter in general, but they are not variables in this comparison. By construction, everything except typing is held constant. There is literally nothing else left to compare. All non-type-related factors are identical by assumption. What remains is exactly one difference: the presence or absence of runtime type errors. At that point, reliability reduces to failure count not as a philosophical choice, but because there is no other dimension remaining.
Between two otherwise identical systems, the one that can fail in fewer ways at runtime is more reliable. That conclusion is not empirical, sociological, or debatable. It follows directly from the setup.
> There's no hard evidence that static typing improves reliability.
I'm curious how you came to that conclusion?
https://pleiad.cl/papers/2012/kleinschmagerAl-icpc2012.pdf
https://www.deepdyve.com/lp/springer-journals/an-empirical-s...
I'm curious how you came to that conclusion?
https://pleiad.cl/papers/2012/kleinschmagerAl-icpc2012.pdf
https://www.deepdyve.com/lp/springer-journals/an-empirical-s...
The benefits of static typing with regard to reliability are unclear, at best:
https://danluu.com/empirical-pl/
https://danluu.com/empirical-pl/
I don't consider a human subjects study to be "hard evidence".
So, we can safely disregard these papers. They got exactly the result that they sought out to get, and the papers were published because they confirmed the preexisting groupthink.
So, we can safely disregard these papers. They got exactly the result that they sought out to get, and the papers were published because they confirmed the preexisting groupthink.
Interesting, so you consider the entire scientific field of medicine to work without hard evidence?
You mean psychology? There’s no hard evidence there. The papers you’re citing are using human subjects in that sort of way. It’s pseudoscience at best
Medicine that involves testing human subject response to treatments is very different from the papers you’re citing and does involve falsifiable theses (usually, definitely not always).
Medicine that involves testing human subject response to treatments is very different from the papers you’re citing and does involve falsifiable theses (usually, definitely not always).
I didn't link any studies. I'm not the person you originally replied to. I was trying to engage in your point that studies involving human subjects cannot contain hard evidence. And no I wasn't referring to psychology in my comment.
Then you’re changing context for no reason.
My point about human subjects is in the context of the linked studies.
I’m not super interested in further debating human subjects in science generally
My point about human subjects is in the context of the linked studies.
I’m not super interested in further debating human subjects in science generally
If you're going to start citing research, you should look at the Cooley finding on verilog vs VHDL.
That's certainly an interesting data point, but it was a 90 minute programming contest, not peer-reviewed research.
The second paper shown above is firewalled.
The first paper shown above was presented at ICPC, which has a history of bias in reviewing, and typically only assigns one or two reviewers in any case.
Which makes it not surprising that the paper itself doesn't really prove anything, except that the authors themselves are good at creating dissimilar situations.
Subjects had to modify existing systems, which were provided by the experimenters.
The experimenters deliberately removed any semblance of anything that might hint at types (comments, variable names, etc.) and did who the fuck knows what else to the dynamically typed code to make it difficult to work with.
They also provided their own IDE and full environment which the participants had to use.
Now, of course, we've all seen the graphs which show that for simple problems, dynamic is better, and there's a crossover point, and, of course Cooley's experiment is on the far left of that graph, so it certainly doesn't prove that strict static typing isn't better for large programs, but it's at least honest in its approach and results, using self-selected working practitioners (and there was never any shortage of working practioners swearing by how much better VHDL is).
https://danluu.com/verilog-vs-vhdl/
The first paper shown above was presented at ICPC, which has a history of bias in reviewing, and typically only assigns one or two reviewers in any case.
Which makes it not surprising that the paper itself doesn't really prove anything, except that the authors themselves are good at creating dissimilar situations.
Subjects had to modify existing systems, which were provided by the experimenters.
The experimenters deliberately removed any semblance of anything that might hint at types (comments, variable names, etc.) and did who the fuck knows what else to the dynamically typed code to make it difficult to work with.
They also provided their own IDE and full environment which the participants had to use.
Now, of course, we've all seen the graphs which show that for simple problems, dynamic is better, and there's a crossover point, and, of course Cooley's experiment is on the far left of that graph, so it certainly doesn't prove that strict static typing isn't better for large programs, but it's at least honest in its approach and results, using self-selected working practitioners (and there was never any shortage of working practioners swearing by how much better VHDL is).
https://danluu.com/verilog-vs-vhdl/
I was searching for the Stefik article to argue here, thank you.
> Functional programming often leads to write-only incomprehensible code; the exact opposite of what you need to have a reliable system.
In what language?
In what language?
Functional programming makes DSLs easier/possible, so you express your domain in natural domain language/constructs leading to easier comprehension, standardization, reuse, and testing, thereby improving reliability. This is the exact opposite of write-only code, DSLs are comprehensible/editable to non-programmers. With a strong enough type system these benefits accrue while ensuring the program in stays a subset of more correct programs than allowed by other compilers.
… I mean, if we’re just making global assertions :)
Gimme the “write only” compiler verified exhaustively pattern matched non-mutable clump in a language I can mould freely any day of the week. I will provide the necessary semantic layer for progress backed with compiler guarantees. That same poop pile in a lesser language may be unrecoverable.
… I mean, if we’re just making global assertions :)
Gimme the “write only” compiler verified exhaustively pattern matched non-mutable clump in a language I can mould freely any day of the week. I will provide the necessary semantic layer for progress backed with compiler guarantees. That same poop pile in a lesser language may be unrecoverable.
> ... functional programming and static typing make things more reliable.
> But this isn't a falsifiable claim.
Saying "this isn't falsifiable" is a wild claim. Indeed the claim "functional programming and static typing make things more reliable" is falsifiable, as long as you admit a statistical understanding. The world is messy and experiments have noise, so what would you use if not statistics? Anecdotes?: no. Purely deductive methods?: no; we should not expect any single technique to be a silver bullet.
Good studies and analyses lay out a causal model and use strong methodologies for showing that some factor has a meaningful impact on some metric of interest. I recommend this as a starting point [1]
[1]: https://yanirseroussi.com/2016/05/15/diving-deeper-into-caus...
> But this isn't a falsifiable claim.
Saying "this isn't falsifiable" is a wild claim. Indeed the claim "functional programming and static typing make things more reliable" is falsifiable, as long as you admit a statistical understanding. The world is messy and experiments have noise, so what would you use if not statistics? Anecdotes?: no. Purely deductive methods?: no; we should not expect any single technique to be a silver bullet.
Good studies and analyses lay out a causal model and use strong methodologies for showing that some factor has a meaningful impact on some metric of interest. I recommend this as a starting point [1]
[1]: https://yanirseroussi.com/2016/05/15/diving-deeper-into-caus...
It improves reliability at compile time, certainly
Citation needed.
All the line items are decent things, worth doing, but the claim about how much following the line items would improve reliability is super exaggerated.
> [Most production incidents] are due to the code entering a state that should never have been possible.
I have never seen evidence that this is even remotely true, and I've been looking at software reliability research in the last few months.
Instead, it is more true that most production incidents are due to the system entering into one of thousands of unsafe states which were possible and latent in production potentially for years. In a sufficiently complex system—all interesting and important software projects—functional programming is not strong enough a tool to prevent even a sliver of potential accidents.
> Arguments that these degraded conditions should have been recognized before the overt accident are usually predicated on naïve notions of system performance. System operations are dynamic, with components (organizational, human, technical) failing and being replaced continuously. — https://how.complexsystems.fail/
> [Most production incidents] are due to the code entering a state that should never have been possible.
I have never seen evidence that this is even remotely true, and I've been looking at software reliability research in the last few months.
Instead, it is more true that most production incidents are due to the system entering into one of thousands of unsafe states which were possible and latent in production potentially for years. In a sufficiently complex system—all interesting and important software projects—functional programming is not strong enough a tool to prevent even a sliver of potential accidents.
> Arguments that these degraded conditions should have been recognized before the overt accident are usually predicated on naïve notions of system performance. System operations are dynamic, with components (organizational, human, technical) failing and being replaced continuously. — https://how.complexsystems.fail/
Hmm, it seems you actually agree with the OP:
OP says (your quote):
> [Most production incidents] are due to the code entering a state that should never have been possible.
You say:
> [...] it is more true that most production incidents are due to the system entering into one of thousands of unsafe states which were possible and latent in production potentially for years
I see you both agree that a broken system enters an "unsafe state" (your words) or a "state that should never have been possible" (OP's words).
"Unsafe state" and "state that should not have been possible" are, in practice in a real system, the same practical thing. I suspect you both would agree "system confuses a string for an integer and acts based on erroneous value" or "system acts on internal state that indicates the valve is both open and closed" would be states that a system should not be in. Outside pedantry, your descriptions are practically synonymous with each other.
OP says (your quote):
> [Most production incidents] are due to the code entering a state that should never have been possible.
You say:
> [...] it is more true that most production incidents are due to the system entering into one of thousands of unsafe states which were possible and latent in production potentially for years
I see you both agree that a broken system enters an "unsafe state" (your words) or a "state that should never have been possible" (OP's words).
"Unsafe state" and "state that should not have been possible" are, in practice in a real system, the same practical thing. I suspect you both would agree "system confuses a string for an integer and acts based on erroneous value" or "system acts on internal state that indicates the valve is both open and closed" would be states that a system should not be in. Outside pedantry, your descriptions are practically synonymous with each other.
The crux is in the "never have been possible" bit. In complex systems, it is impossible to eliminate these potential states with functional programming or any other technique, unsafe states are always potentialities that must be actively controlled.
Another way of casting it is like this. The goal may be:
1. Eliminate possibility code can enter invalid state 2. Control parameters of the system so that it remains in a safe condition
Those are very different goals.
Another way of casting it is like this. The goal may be:
1. Eliminate possibility code can enter invalid state 2. Control parameters of the system so that it remains in a safe condition
Those are very different goals.
Right, I understand your meaning better.
I agree with you: no matter how good of a job the code (by construction or types or otherwise) does of “making unsafe states unrepresentable”, that in no way makes a real world complex system “safe” by itself.
Code can be structured so that valves may only be open OR closed, but nothing stops the real world from returning a sensor reading that says “the valve is <undefined>”. To remain a “safe” system, the system must deal with inconsistent states like “heisen-valves”.
I agree with you: no matter how good of a job the code (by construction or types or otherwise) does of “making unsafe states unrepresentable”, that in no way makes a real world complex system “safe” by itself.
Code can be structured so that valves may only be open OR closed, but nothing stops the real world from returning a sensor reading that says “the valve is <undefined>”. To remain a “safe” system, the system must deal with inconsistent states like “heisen-valves”.
heisen-valves are a perfect comparison, thank you.
I'm wary of absolute statements about programming.
I want to be a contrarian and argue with this, but my daily praxis is generally to take a betteridges law approach to most argumentative absolutes and also false dichotomous headlines and question them. Reading the other comments to the effect that the conferences are now strong typing gabfests and insufficiently about FP per se reinforced this feeling.
Reliability should be simpler with FP but so much depends on correctness of the runtime and IO.
Erlang and the "run correctly or die" comes to mind as well. The system is either working or is off. When being off is fatal, Erlang seems to shrug and say "maybe next karmic cycle" maybe this too is a better approach?
Reliability should be simpler with FP but so much depends on correctness of the runtime and IO.
Erlang and the "run correctly or die" comes to mind as well. The system is either working or is off. When being off is fatal, Erlang seems to shrug and say "maybe next karmic cycle" maybe this too is a better approach?
Strong types: yes, it’s definitely better
Functional programming: no, functional programming as in: the final program consists in piping functions together and calling the pipe. In my opinion, that tends to get in the way of complex error handling.
The problem being that raising Exceptions at a deep level and catching them at some higher level is not pure functional programming. So your code has to deal with all the cases. It is more reliable if you can do it, but large systems have way too many failure points to be able to handle them all in a way that is practical.
Functional programming: no, functional programming as in: the final program consists in piping functions together and calling the pipe. In my opinion, that tends to get in the way of complex error handling.
The problem being that raising Exceptions at a deep level and catching them at some higher level is not pure functional programming. So your code has to deal with all the cases. It is more reliable if you can do it, but large systems have way too many failure points to be able to handle them all in a way that is practical.
That's only a problem when you decide that the way to do error handling is exceptions. When you go with a strongly typed functional programming language, you throw exceptions away, and the fact that something can error, and what kinds of errors it can produce, are encoded into the type system.
So yes, generating errors at a deep level and catching them at a higher one is a normal pard of the system design, it's purely functional, ando nothing strange happens, in very large systems. You ADT the errors, pipe up entire families of them, and select what you manage. It's significantly easier than exceptions, in the sense that I can be sure when I've validated the error.
It's practical, and typically one dedicates less code to the error handling than, say, yor typical enterprise Java program that is terrified of runtime exceptions and null checks every step of the way. In fact, I'd argue this is the main selling point of strongly typed FP.
So yes, generating errors at a deep level and catching them at a higher one is a normal pard of the system design, it's purely functional, ando nothing strange happens, in very large systems. You ADT the errors, pipe up entire families of them, and select what you manage. It's significantly easier than exceptions, in the sense that I can be sure when I've validated the error.
It's practical, and typically one dedicates less code to the error handling than, say, yor typical enterprise Java program that is terrified of runtime exceptions and null checks every step of the way. In fact, I'd argue this is the main selling point of strongly typed FP.
> When you go with a strongly typed functional programming language, you throw exceptions away, and the fact that something can error, and what kinds of errors it can produce, are encoded into the type system.
You’ve just reinvented checked exceptions, good job.
You’ve just reinvented checked exceptions, good job.
Return type DUs are so much better than checked exceptions.
> that tends to get in the way of complex error handling.
Agree. In Java, Streams allow you to process collections in a functional style. This feature enables concise, expressive data manipulation with operations like map, filter, and reduce.
Some people point out that Java's checked exceptions spoil the simplicity and elegance of Streams by forcing you to handle exceptions.
But that's not a reason to not have checked exceptions, it is a reason to not do functional style composition when methods can throw exceptions. Streams was invented for collections, which tend not to throw exceptions. If proper error handling is important don't do Streams.
Agree. In Java, Streams allow you to process collections in a functional style. This feature enables concise, expressive data manipulation with operations like map, filter, and reduce.
Some people point out that Java's checked exceptions spoil the simplicity and elegance of Streams by forcing you to handle exceptions.
But that's not a reason to not have checked exceptions, it is a reason to not do functional style composition when methods can throw exceptions. Streams was invented for collections, which tend not to throw exceptions. If proper error handling is important don't do Streams.
The Java streams are cool and I like them, but they're not a replacement for a functional type system or a functional language.
`map` is a lot more than a fancy for-loop for lists and arrays; it's about abstracting away the entire idea of context. Java streams aren't a substitute for what you have in Haskell.
`map` is a lot more than a fancy for-loop for lists and arrays; it's about abstracting away the entire idea of context. Java streams aren't a substitute for what you have in Haskell.
Yes, they are really a poor emulation of scala which makes it a bit more usable.
If you have strong types, it is still possible to make a mutable thing, that will be mutated from the other end of the program and that will introduce bugs, that can be hard to find. If you are doing FP on the other hand, at least change always results in new objects, with structural sharing at most. This excludes a whole category of bugs.
> If you are doing FP on the other hand, at least change always results in new objects, with structural sharing at most. This excludes a whole category of bugs.
Not if you program it with a mutable god object to mimic creating a new big state, then you have exactly the same kind of issues.
The issue is if you try to program a transaction flow using object oriented programming, that is not very good, and most work programmers do revolves around involves flows. But when it doesn't then functional programming isn't a very good or reliable solution.
Not if you program it with a mutable god object to mimic creating a new big state, then you have exactly the same kind of issues.
The issue is if you try to program a transaction flow using object oriented programming, that is not very good, and most work programmers do revolves around involves flows. But when it doesn't then functional programming isn't a very good or reliable solution.
> Not if you program it with a mutable god object to mimic creating a new big state, then you have exactly the same kind of issues.
Have you done any FP? That's not how you do FP.
Have you done any FP? That's not how you do FP.
Mr. Error Monad enters the chat...
A few mention on tests, but I expected more. The main value of pure functions is that now their behavior is representative in tests. In fact, I'd argue that all you need for reliability is determinism and tests of all equivalent scenarios. functional programming (and immutability) are only helpful to the extent that it's easier to have representative tests, but not necessarily required.
> In fact, I'd argue that all you need for reliability is determinism and tests of all equivalent scenarios.
Any insights as to how to get effective determinism without pure functions?
Pure functions win here because we only have to reason about the function arguments. Reasoning is easier when you have to less of it! Without pure functions, the state space explodes, because anything anywhere could have a side-effect — madness, I say! — so how would you figure out equivalent states? Special case inspection I suppose?
There is a continuum between "anything goes" and "pure functions". From a certain light, all the varieties of encapsulation can be seen as explorations of this theme. (An idea: perhaps there are languages where side-effects can be circumscribed in ways that don't rely on the high bar of pure functions?)
The arguments against pure functions appear to be somewhat contingent: current adoption levels, practice, convenience, and taste. Things that are contingent have a way of changing over time as new methods emerge and new values take hold.
I don't hold shallow human preferences in high regard. As an example, many humans and organizations in practice trade security for convenience, at significant cost — especially when that cost is external to them.
At the same time, onerous tasks encourage work-arounds. This is the crux of it I think: unless people perceive the value of pure functions (to do what they want to do), some will seek shortcuts. So we need some combination of (1) making them easier to work with; (2) motivating people to aspire to higher principles; namely, high quality software that does not open to door to exploitation, misuse, botnets, etc; and/or (3) internalize the external costs.
As an example of (3), if people and companies faced predictable and commensurate costs when their flawed software inflicts harm on others, they would be more inclined to care about correctness.
Any insights as to how to get effective determinism without pure functions?
Pure functions win here because we only have to reason about the function arguments. Reasoning is easier when you have to less of it! Without pure functions, the state space explodes, because anything anywhere could have a side-effect — madness, I say! — so how would you figure out equivalent states? Special case inspection I suppose?
There is a continuum between "anything goes" and "pure functions". From a certain light, all the varieties of encapsulation can be seen as explorations of this theme. (An idea: perhaps there are languages where side-effects can be circumscribed in ways that don't rely on the high bar of pure functions?)
The arguments against pure functions appear to be somewhat contingent: current adoption levels, practice, convenience, and taste. Things that are contingent have a way of changing over time as new methods emerge and new values take hold.
I don't hold shallow human preferences in high regard. As an example, many humans and organizations in practice trade security for convenience, at significant cost — especially when that cost is external to them.
At the same time, onerous tasks encourage work-arounds. This is the crux of it I think: unless people perceive the value of pure functions (to do what they want to do), some will seek shortcuts. So we need some combination of (1) making them easier to work with; (2) motivating people to aspire to higher principles; namely, high quality software that does not open to door to exploitation, misuse, botnets, etc; and/or (3) internalize the external costs.
As an example of (3), if people and companies faced predictable and commensurate costs when their flawed software inflicts harm on others, they would be more inclined to care about correctness.
> The arguments against pure functions appear to be somewhat contingent: current adoption levels, practice, convenience, and taste.
At least with many GUIs, the time it would take to know, document and/or test all combinations of UI behaviors quickly exceeds the time available to humans. It's at least tractable to start with vastly more states than could ever be measured, and then gate or special-case certain ones to try to make things minimally safe/sane/reliable for the user.
At least with many GUIs, the time it would take to know, document and/or test all combinations of UI behaviors quickly exceeds the time available to humans. It's at least tractable to start with vastly more states than could ever be measured, and then gate or special-case certain ones to try to make things minimally safe/sane/reliable for the user.
I can't tell if you are agreeing (by elaborating) or disagreeing (by giving a counter-example) or saying something else. Mind hitting me over the head with it?
Agree, I didn’t give testing enough space. A proper treatment would’ve doubled the post, so I’m writing a separate follow-up on testing.
Pure functions/immutability help a lot because tests become representative and cheap. I’d only push back on “tests of all equivalent scenarios” being sufficient, the space explodes and many real failures live at I/O/concurrency/distributed boundaries. My intended claim is that FP/ADTs/types reduce the state space and improve the ROI of tests, not replace them.
Pure functions/immutability help a lot because tests become representative and cheap. I’d only push back on “tests of all equivalent scenarios” being sufficient, the space explodes and many real failures live at I/O/concurrency/distributed boundaries. My intended claim is that FP/ADTs/types reduce the state space and improve the ROI of tests, not replace them.
Most of the musings on enforcing invalid states with ADTs are impractical when working with real data that needs runtime validation when it enters the system.
Using a schema/spec/type library at runtime that is even more powerful than ADTs is a better investment - or to be less controversial - is an additional investment on top of types.
Yes, it means the compiler can't help you as much, but who has time waiting for a compiler anyways ;)
I find the "make illegal state unrepresentable via types" idea great for software that needs to fly a plane, but for enterprise software not so much. The cost/benefit is not justifiable.
Using a schema/spec/type library at runtime that is even more powerful than ADTs is a better investment - or to be less controversial - is an additional investment on top of types.
Yes, it means the compiler can't help you as much, but who has time waiting for a compiler anyways ;)
I find the "make illegal state unrepresentable via types" idea great for software that needs to fly a plane, but for enterprise software not so much. The cost/benefit is not justifiable.
In the Cents example, why are they using throw instead of Result?
Tup: Use interface for structural types in TypeScript, not type.
Of course you can do this with Typescript but what about Python if you're stuck using it for $dayjob. Any tips?
You can get most of the “ADT/state-machine reliability” benefits in Python by combining static checking + tagged unions + boundary validation:
Model states as tagged unions (Union + Literal + dataclass(frozen=True)), use match (Py3.10+) and add assert_never so type checkers complain when you forget a case.
Run Pyright (strict) or mypy –strict in CI so “illegal states” show up as build failures, not incidents.
Validate/parsing at boundaries (HTTP/queues) with Pydantic discriminated unions (tagged unions at runtime), then keep internals typed.
For expected failures, prefer an explicit Result (e.g., returns) over exceptions-as-control-flow.
Use Ruff for lint/consistency (it’s not a type checker, but pairs well with one).
References here:
Pyright: https://microsoft.github.io/pyright/ mypy --strict: https://mypy.readthedocs.io/en/stable/getting_started.html PEP 634 (match): https://peps.python.org/pep-0634/ assert_never & exhaustiveness guide: https://typing.python.org/en/latest/guides/unreachable.html typing_extensions (backports): https://typing-extensions.readthedocs.io/ Pydantic discriminated unions: https://docs.pydantic.dev/latest/concepts/unions/ returns Result: https://returns.readthedocs.io/en/latest/pages/result.html Ruff FAQ: https://docs.astral.sh/ruff/faq/
Model states as tagged unions (Union + Literal + dataclass(frozen=True)), use match (Py3.10+) and add assert_never so type checkers complain when you forget a case.
Run Pyright (strict) or mypy –strict in CI so “illegal states” show up as build failures, not incidents.
Validate/parsing at boundaries (HTTP/queues) with Pydantic discriminated unions (tagged unions at runtime), then keep internals typed.
For expected failures, prefer an explicit Result (e.g., returns) over exceptions-as-control-flow.
Use Ruff for lint/consistency (it’s not a type checker, but pairs well with one).
References here:
Pyright: https://microsoft.github.io/pyright/ mypy --strict: https://mypy.readthedocs.io/en/stable/getting_started.html PEP 634 (match): https://peps.python.org/pep-0634/ assert_never & exhaustiveness guide: https://typing.python.org/en/latest/guides/unreachable.html typing_extensions (backports): https://typing-extensions.readthedocs.io/ Pydantic discriminated unions: https://docs.pydantic.dev/latest/concepts/unions/ returns Result: https://returns.readthedocs.io/en/latest/pages/result.html Ruff FAQ: https://docs.astral.sh/ruff/faq/
I think there is a strong case that ADTs (algebraic data types) aren't so great after all. Specifically, the "tagged" unions of ADT languages like Haskell are arguably pretty clearly inferior to the "untagged" unions of TypeScript or Scala 3. Because the latter actually behave like a logical "or" rather than an artificial construct that needs to be wrapped and unwrapped.
While others have addressed the programming case for tagged unions, I want to add that, to a logician, tagged unions are the natural construct corresponding to "logical or".
In intuitionistic logic (which is the most basic kind from which to view the Curry-Howard or "propositions-as-types" correspondence), a proof of "A or B" is exactly a choice of "left" or "right" disjunct together with a corresponding proof of either A or B. The "choice tag" is part of the "constructive data" telling us how to build our proof of "A or B". Translated back into the language of code, the type "A | B" would be exactly a tagged union.
In intuitionistic logic (which is the most basic kind from which to view the Curry-Howard or "propositions-as-types" correspondence), a proof of "A or B" is exactly a choice of "left" or "right" disjunct together with a corresponding proof of either A or B. The "choice tag" is part of the "constructive data" telling us how to build our proof of "A or B". Translated back into the language of code, the type "A | B" would be exactly a tagged union.
When A and B are disjoint, you don't need the tag unless you for some reason you require that `Maybe<Maybe<T>> != Maybe<T>` holds true and don't like the collapsing semantics of unions where `Maybe<Maybe<T>> == Maybe<T>`
In practice, the cohabitants in Option/Result types are almost always disjoint. So you spend time wrapping/unwrapping Some/Ok/Err for no value add.
In practice, the cohabitants in Option/Result types are almost always disjoint. So you spend time wrapping/unwrapping Some/Ok/Err for no value add.
I disagree. Something of type "A" should, according to basic propositional logic, also be of type "A or B". That's the case for an untagged union, but not for a tagged union (because of wrapping), which is decidedly illogical.
Well, I have outlined the usual story of logic as it corresponds to programming (as has been accepted for at least some five decades now); it strains credulity to claim that logic is illogical.
Now I do see where you are coming from; under a set-theoretic interpretation with "implies" as "subset", "or" as "union", and "and" as "intersection", the fact that "A implies (A or B)" tells us that an element of the set A is also an element of the set "A union B".
However, this is not the interpretation that leads to a straightforward correspondence between logic and programming. For example, we would like "A and B" to correspond to the type of pairs of elements of A with elements of B, which is not at all the set-theoretic intersection. And while "(A and B) implies A", we do not want to say a value of type "(A, B)" also has type "A". (E.g., if a function expects an "A" and receives an "(A, A)", we are at an impasse.)
So "implies" should not be read programmatically as a subtyping relation; instead, "A implies B" tells us that there is a function taking a value of type A to a value of type B. In the case of "A implies (A or B)", that function takes its input and tags it as belonging to the left disjunct!
Another perspective I must mention: given a proof of "A or B" and another of "(A or B) implies C", how can we combine these into a simpler proof of just "C"? A proof of "(A or B) implies C" must contain both a proof a "A implies C" and a proof of "B implies C", and we could insert into one those proofs a proof of A or a proof of B. But we have to know which one we have! (This is a very short gloss of a much deeper story, where, under Curry-Howard, proof simplification corresponds to computation, and this is another way of describing a function call that does a case-analysis of a tagged union (or "sum type").)
Now "union and intersection" types with the set-theoretic properties you are hinting at have indeed been studied (see, for example, Section 15.7 of Pierce's "Types and Programming Languages"). But they do not replace the much more familiar "sum and product types", and do not play the central role of "or" and "and" in the correspondence of programming to logic.
Now I do see where you are coming from; under a set-theoretic interpretation with "implies" as "subset", "or" as "union", and "and" as "intersection", the fact that "A implies (A or B)" tells us that an element of the set A is also an element of the set "A union B".
However, this is not the interpretation that leads to a straightforward correspondence between logic and programming. For example, we would like "A and B" to correspond to the type of pairs of elements of A with elements of B, which is not at all the set-theoretic intersection. And while "(A and B) implies A", we do not want to say a value of type "(A, B)" also has type "A". (E.g., if a function expects an "A" and receives an "(A, A)", we are at an impasse.)
So "implies" should not be read programmatically as a subtyping relation; instead, "A implies B" tells us that there is a function taking a value of type A to a value of type B. In the case of "A implies (A or B)", that function takes its input and tags it as belonging to the left disjunct!
Another perspective I must mention: given a proof of "A or B" and another of "(A or B) implies C", how can we combine these into a simpler proof of just "C"? A proof of "(A or B) implies C" must contain both a proof a "A implies C" and a proof of "B implies C", and we could insert into one those proofs a proof of A or a proof of B. But we have to know which one we have! (This is a very short gloss of a much deeper story, where, under Curry-Howard, proof simplification corresponds to computation, and this is another way of describing a function call that does a case-analysis of a tagged union (or "sum type").)
Now "union and intersection" types with the set-theoretic properties you are hinting at have indeed been studied (see, for example, Section 15.7 of Pierce's "Types and Programming Languages"). But they do not replace the much more familiar "sum and product types", and do not play the central role of "or" and "and" in the correspondence of programming to logic.
> However, this is not the interpretation that leads to a straightforward correspondence between logic and programming. For example, we would like "A and B" to correspond to the type of pairs of elements of A with elements of B, which is not at all the set-theoretic intersection. And while "(A and B) implies A", we do not want to say a value of type "(A, B)" also has type "A". (E.g., if a function expects an "A" and receives an "(A, A)", we are at an impasse.)
Intersection types in TypeScript and Scala 3 do work like conventional intersections / conjunctions. Something of type A&B is of type A. For example, a Set&Iterable is a Set. This makes perfect sense and is coherent with how unions work. A&A is then obviously equivalent to A. I'm not sure where you see the problem.
Intersection types in TypeScript and Scala 3 do work like conventional intersections / conjunctions. Something of type A&B is of type A. For example, a Set&Iterable is a Set. This makes perfect sense and is coherent with how unions work. A&A is then obviously equivalent to A. I'm not sure where you see the problem.
I suppose I erroneously assumed some familiarity with the correspondence between product types (i.e., types of pairs) and the constructive logical interpretation of "and".
Suffice it to say for now: there is an interpretation of logic that gives a tighter correspondence to programming than the set-theoretic one, under the name "Curry-Howard" or "propositions as types, proofs as programs", and which has been known and cherished by logicians, programming language theorists, and also category theorists for a long time. The logic is constructive as it must be: a program of type A tells us how to build a value of type A, a proof of proposition A tells us how to construct evidence for A. From here we get things like "a proof of A and B is a proof of A together with a proof of B" (the "BHK interpretation"), which connects "and" to product types...
I spoke up because I could not leave untouched the idea that "tagged unions are illogical". On the contrary, tagged unions (aka "disjoint unions", "sum types", "coproducts", etc.) arise forthwith from an interpretation of logic that is not the set-theoretical one, but is a more fruitful one from which programming language theory begins. You are not wrong that there is also a correspondence between (untagged) union and intersection types and a set-theoretical interpretation of propositional logic, and that union and intersection types can also be used in programming, but you are missing a much bigger and very beautiful picture (which you will find described in most any introductory course or text on PL theory).
Suffice it to say for now: there is an interpretation of logic that gives a tighter correspondence to programming than the set-theoretic one, under the name "Curry-Howard" or "propositions as types, proofs as programs", and which has been known and cherished by logicians, programming language theorists, and also category theorists for a long time. The logic is constructive as it must be: a program of type A tells us how to build a value of type A, a proof of proposition A tells us how to construct evidence for A. From here we get things like "a proof of A and B is a proof of A together with a proof of B" (the "BHK interpretation"), which connects "and" to product types...
I spoke up because I could not leave untouched the idea that "tagged unions are illogical". On the contrary, tagged unions (aka "disjoint unions", "sum types", "coproducts", etc.) arise forthwith from an interpretation of logic that is not the set-theoretical one, but is a more fruitful one from which programming language theory begins. You are not wrong that there is also a correspondence between (untagged) union and intersection types and a set-theoretical interpretation of propositional logic, and that union and intersection types can also be used in programming, but you are missing a much bigger and very beautiful picture (which you will find described in most any introductory course or text on PL theory).
But I'm pretty sure that even in intuitionistic logic, "A" implies "A or B". Which is not the case with tagged unions (as I said, because of wrapping).
It's true that in intuitionistic logic "A implies (A or B)"; the usual computational interpretation of that is that "there is a function taking a value of type A and returning a value of type A + B", where + is the tagged union, and, per above, that function is exactly the one which tags its input as belonging to the left disjunct.
I suspect you are still reading "A implies B" as "A is a subtype of B", derived from a set-theoretic interpretation of propositional logic. But the constructive interpretation is that a proof of "A implies B" is a method to take a proof of A and transform it into a proof of B. Computationally, a value of type "A implies B" (typically rewritten "A -> B") is a function that takes values of type A and returns values of type B.
Well, everything I've said here is standard and widely-taught; go forth and check if you're inclined to. A good introduction is the one by Philip Wadler, https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as... (tagged unions appear in Section 3, though it's all worth reading). A much more to-the-point and programming-focused account is in this OCaml book: https://cs3110.github.io/textbook/chapters/adv/curry-howard.... (very little OCaml syntax is used). You can find countless more.
I suspect you are still reading "A implies B" as "A is a subtype of B", derived from a set-theoretic interpretation of propositional logic. But the constructive interpretation is that a proof of "A implies B" is a method to take a proof of A and transform it into a proof of B. Computationally, a value of type "A implies B" (typically rewritten "A -> B") is a function that takes values of type A and returns values of type B.
Well, everything I've said here is standard and widely-taught; go forth and check if you're inclined to. A good introduction is the one by Philip Wadler, https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as... (tagged unions appear in Section 3, though it's all worth reading). A much more to-the-point and programming-focused account is in this OCaml book: https://cs3110.github.io/textbook/chapters/adv/curry-howard.... (very little OCaml syntax is used). You can find countless more.
Thanks. I think in the end the question will be: which is better, an algebraic or a set-theoretic type system? Which is more practical to use? Which is more elegant? Should both be mixed?
(One complicating aspect is that there doesn't yet exist a mainstream language with full set-theoretic type system. TypeScript and Scala 3 currently only support intersections and unions, but no complements, making certain complex types not definable. E.g. "Int & ~0", integers without zero.)
(One complicating aspect is that there doesn't yet exist a mainstream language with full set-theoretic type system. TypeScript and Scala 3 currently only support intersections and unions, but no complements, making certain complex types not definable. E.g. "Int & ~0", integers without zero.)
I at first thought it was nice to save the wrapping, but you save yourself sooo much pain, ugliness and mistakes pattern matching trying to distinguish the types once you just use tagged unions.
I think you’re both pointing at the same tradeoff: “untagged” unions feel lighter, but you often pay it back in ad-hoc narrowing (shape checks/heuristics) and ambiguity once variants overlap.
Tagged unions/ADTs make the discriminant explicit, which is exactly why they tend to be reliability-friendly: exhaustive matches + explicit constructors reduce “guessing” and refactor breakage.
That said, I agree the ergonomics matter, TS-style discriminated unions are basically “tagged” too once you add a kind field, for example.
Tagged unions/ADTs make the discriminant explicit, which is exactly why they tend to be reliability-friendly: exhaustive matches + explicit constructors reduce “guessing” and refactor breakage.
That said, I agree the ergonomics matter, TS-style discriminated unions are basically “tagged” too once you add a kind field, for example.
Most of the time when I use untagged unions, I end up adding a tag and logic to case on it anyway…
> "tagged" unions of ADT languages like Haskell are arguably pretty clearly inferior to the "untagged" unions of TypeScript
dude .. wut?? Explain to me exactly how this is true, with a real world example.
From where I stand, untagged unions are useful in an extremely narrow set of circumstances. Tagged unions, on the other hand, are incredibly useful in a wide variety of applications.
dude .. wut?? Explain to me exactly how this is true, with a real world example.
From where I stand, untagged unions are useful in an extremely narrow set of circumstances. Tagged unions, on the other hand, are incredibly useful in a wide variety of applications.
Example: Option<> types. Maybe a function returns an optional string, but then you are able to improve the guarantee such that it always returns a string. With untagged unions you can just change the return type of the function from String|Null to String. No other changes necessary. For the tagged case you would have to change all(!) the call sites, which expect an Option<String>, to instead expect a String. Completely unnecessary for untagged unions.
A similar case applies to function parameters: In case of relaxed parameter requirements, changing a parameter from String to String|Null is trivial, but a change from String to Option<String> would necessitate changing all the call sites.
> From where I stand, untagged unions are useful in an extremely narrow set of circumstances. Tagged unions, on the other hand, are incredibly useful in a wide variety of applications.
Any real world example?
A similar case applies to function parameters: In case of relaxed parameter requirements, changing a parameter from String to String|Null is trivial, but a change from String to Option<String> would necessitate changing all the call sites.
> From where I stand, untagged unions are useful in an extremely narrow set of circumstances. Tagged unions, on the other hand, are incredibly useful in a wide variety of applications.
Any real world example?
I think your Option/String example is a real-world tradeoff, but it’s not a slam-dunk “untagged > tagged.”
For API evolution, T | null can be a pragmatic “relax/strengthen contract” knob with less mechanical churn than Option<T> (because many call sites don’t care and just pass values through). That said, it also makes it easier to accidentally reintroduce nullability and harder to enforce handling consistently, the failure mode is “it compiles, but someone forgot the check.”
In practice, once the union has more than “nullable vs present”, people converge to discriminated unions ({ kind: "ok", ... } | { kind: "err", ... }) because the explicit tag buys exhaustiveness and avoids ambiguous narrowing. So I’d frame untagged unions as great for very narrow cases (nullability / simple widening), and tagged/discriminated unions as the reliability default for domain states.
For reliability, I’d rather pay the mechanical churn of Option<T> during API evolution than pay the ongoing risk tax of “nullable everywhere.
My post argues for paying costs that are one-time and compiler-enforced (refactors) vs costs that are ongoing and human-enforced (remembering null checks).
For API evolution, T | null can be a pragmatic “relax/strengthen contract” knob with less mechanical churn than Option<T> (because many call sites don’t care and just pass values through). That said, it also makes it easier to accidentally reintroduce nullability and harder to enforce handling consistently, the failure mode is “it compiles, but someone forgot the check.”
In practice, once the union has more than “nullable vs present”, people converge to discriminated unions ({ kind: "ok", ... } | { kind: "err", ... }) because the explicit tag buys exhaustiveness and avoids ambiguous narrowing. So I’d frame untagged unions as great for very narrow cases (nullability / simple widening), and tagged/discriminated unions as the reliability default for domain states.
For reliability, I’d rather pay the mechanical churn of Option<T> during API evolution than pay the ongoing risk tax of “nullable everywhere.
My post argues for paying costs that are one-time and compiler-enforced (refactors) vs costs that are ongoing and human-enforced (remembering null checks).
I believe there is a misunderstanding. The compiler can check untagged unions just as much as it can check tagged unions. I don't think there is any problem with "ambiguous narrowing", or "reliability". There is also no risk of "nullable everywhere": If the type of x is Foo|Null, the compiler forces you to write a null check before you can access x.bar(). If the type of x is Foo, x is not nullable. So you don't have to remember null checks (or checks for other types): the compiler will remember them. There is no difference to tagged unions in this regard.
I think we mostly agree for the nullable case in a sound-enough type system: if Foo | null is tracked precisely and the compiler forces a check before x.bar, then yes, you’re not “remembering” checks manually, the compiler is.
Two places where I still see tagged/discriminated unions win in practice:
1. Scaling beyond nullability. Once the union has multiple variants with overlapping structure, “untagged” narrowing becomes either ambiguous or ends up reintroducing an implicit tag anyway (some sentinel field / predicate ladder). An explicit tag gives stable, intention-revealing narrowing + exhaustiveness.
2. Boundary reality. In languages like TypeScript (even with strictNullChecks), unions are routinely weakened by any, assertions, JSON boundaries, or library types. Tagged unions make the “which case is this?” explicit at the value level, so the invariant survives serialization/deserialization and cross-module boundaries more reliably.
So I’d summarize it as: T | null is a great ergonomic tool for one axis (presence/absence) when the type system is enforced end-to-end. For domain states, I still prefer explicit tags because they keep exhaustiveness and intent robust as the system grows.
If you’re thinking Scala 3 / a sound type system end-to-end, your point is stronger; my caution is mostly from TS-in-the-wild + messy boundaries.
Two places where I still see tagged/discriminated unions win in practice:
1. Scaling beyond nullability. Once the union has multiple variants with overlapping structure, “untagged” narrowing becomes either ambiguous or ends up reintroducing an implicit tag anyway (some sentinel field / predicate ladder). An explicit tag gives stable, intention-revealing narrowing + exhaustiveness.
2. Boundary reality. In languages like TypeScript (even with strictNullChecks), unions are routinely weakened by any, assertions, JSON boundaries, or library types. Tagged unions make the “which case is this?” explicit at the value level, so the invariant survives serialization/deserialization and cross-module boundaries more reliably.
So I’d summarize it as: T | null is a great ergonomic tool for one axis (presence/absence) when the type system is enforced end-to-end. For domain states, I still prefer explicit tags because they keep exhaustiveness and intent robust as the system grows.
If you’re thinking Scala 3 / a sound type system end-to-end, your point is stronger; my caution is mostly from TS-in-the-wild + messy boundaries.
I think the real promise of "set-theoretic type systems" comes when don't just have (untagged) unions, but also intersections (Foo & Bar) and complements/negations (!Foo). Currently there is no such language with negations, but once you have them, the type system is "functionally complete", and you can represent arbitrary Boolean combination of types. E.g. "Foo | (Bar & !Baz)". Which sounds pretty powerful, although the practical use is not yet quite clear.
> For the tagged case you would have to change all(!) the call sites
Yeah, that's exactly why I want a tagged union; so when I make a change, the compiler tells me where I need to go to do updates to my system, instead of manually hunting around for all the sites.
---
The only time an untagged union is appropriate is when the tag accounts for an appreciable amount of memory in a system that churns through a shit-ton of data, and has a soft or hard realtime performance constraint. Other than that, there's just no reason to not use a tagged union, except "I'm lazy and don't want to", which, sometimes, is also a valid reason. But it'll probably come back to bite you, if it stays in there too long.
Yeah, that's exactly why I want a tagged union; so when I make a change, the compiler tells me where I need to go to do updates to my system, instead of manually hunting around for all the sites.
---
The only time an untagged union is appropriate is when the tag accounts for an appreciable amount of memory in a system that churns through a shit-ton of data, and has a soft or hard realtime performance constraint. Other than that, there's just no reason to not use a tagged union, except "I'm lazy and don't want to", which, sometimes, is also a valid reason. But it'll probably come back to bite you, if it stays in there too long.
> > For the tagged case you would have to change all(!) the call sites
> Yeah, that's exactly why I want a tagged union; so when I make a change, the compiler tells me where I need to go to do updates to my system, instead of manually hunting around for all the sites.
You don't have to do anything manually. There is nothing to do. Changing the return type of a function from String|Null to String is completely safe, the compiler knows that, so you don't have to do any "manual hunting" at call sites.
> Yeah, that's exactly why I want a tagged union; so when I make a change, the compiler tells me where I need to go to do updates to my system, instead of manually hunting around for all the sites.
You don't have to do anything manually. There is nothing to do. Changing the return type of a function from String|Null to String is completely safe, the compiler knows that, so you don't have to do any "manual hunting" at call sites.
The String|null example is just a nullable type; it's not an interesting use of unions either way. The conversation starts when it's Foo|Bar|Baz
I'm unfamiliar with typescript, so in that language I don't have an opinion either way, but in C, you pretty much always want the tag
I'm unfamiliar with typescript, so in that language I don't have an opinion either way, but in C, you pretty much always want the tag
C doesn't support any untagged unions (or intersections) in the modern sense. In a set-theoretic type system, if you want to call a method of Foo, and the type of your variable is Foo|Bar|Baz, you have to do a type check for Bar and Baz first, otherwise the compiler won't compile.
Okay .. so, riddle me this Batman.
If I have an untagged union in <language_of_your_choice>, and I'm iterating over an array of elements of type `Foo|Bar|Baz`, and I have to do a dynamic cast before accessing the element (runtime typecheck) .. I believe that must actually be a tagged union under the hood, whether or not you call it a tagged union or not... right? ie. How would the program possibly know at runtime what the type of a heterogeneous set of elements is without a tag value to tell it?
If I have an untagged union in <language_of_your_choice>, and I'm iterating over an array of elements of type `Foo|Bar|Baz`, and I have to do a dynamic cast before accessing the element (runtime typecheck) .. I believe that must actually be a tagged union under the hood, whether or not you call it a tagged union or not... right? ie. How would the program possibly know at runtime what the type of a heterogeneous set of elements is without a tag value to tell it?
That sounds plausible. Just like functional programming languages are imperative under the hood. It's all magic as far as I'm concerned.
> but in C, you pretty much always want the tag
We aren't discussing unions in memory layout, but in type systems. This also clearly indicates you aren't qualified for this discussion.
We aren't discussing unions in memory layout, but in type systems. This also clearly indicates you aren't qualified for this discussion.
I believe that, by the description provided, most languages that you're talking about must actually represent 'untagged unions' as tagged unions under the hood. See my sibling comment. I'm curious
To be fair, even Wikipedia talks about "untagged unions" only in the context of C. The terminology is confusing and the literature often out of date.
See also the type-state pattern. It is commonly used in Rust along with the builder pattern [1]. Quoting:
"""The typestate pattern is an API design pattern that encodes information about an object’s run-time state in its compile-time type. In particular, an API using the typestate pattern will have:
- Operations on an object (such as methods or functions) that are only available when the object is in certain states,
- A way of encoding these states at the type level, such that attempts to use the operations in the wrong state fail to compile,
- State transition operations (methods or functions) that change the type-level state of objects in addition to, or instead of, changing run-time dynamic state, such that the operations in the previous state are no longer possible.
This is useful because:
- It moves certain types of errors from run-time to compile-time, giving programmers faster feedback.
- It interacts nicely with IDEs, which can avoid suggesting operations that are illegal in a certain state.
- It can eliminate run-time checks, making code faster/smaller."""
Some other languages can do it as well: see [2] for a discussion.
[1]: https://cliffle.com/blog/rust-typestate/
[2]: https://www.reddit.com/r/rust/comments/17l8eez/is_there_any_...
"""The typestate pattern is an API design pattern that encodes information about an object’s run-time state in its compile-time type. In particular, an API using the typestate pattern will have:
- Operations on an object (such as methods or functions) that are only available when the object is in certain states,
- A way of encoding these states at the type level, such that attempts to use the operations in the wrong state fail to compile,
- State transition operations (methods or functions) that change the type-level state of objects in addition to, or instead of, changing run-time dynamic state, such that the operations in the previous state are no longer possible.
This is useful because:
- It moves certain types of errors from run-time to compile-time, giving programmers faster feedback.
- It interacts nicely with IDEs, which can avoid suggesting operations that are illegal in a certain state.
- It can eliminate run-time checks, making code faster/smaller."""
Some other languages can do it as well: see [2] for a discussion.
[1]: https://cliffle.com/blog/rust-typestate/
[2]: https://www.reddit.com/r/rust/comments/17l8eez/is_there_any_...
The type-state pattern is really just OOP implementation inheritance in a type-theoretic trench coat. The relevant difference is simply that most uses of type-state are not trying to span multiple modules like the OOP design approach does; the "state" variations are contained such that they don't impact modularity throughout the program, unlike the OOP inheritance approach.
I like good type systems, too, but they won't save you from bugs that are better addressed by fuzz testing, fault injection testing and adversarial mindset shifts.
Luckily these aren't exclusive! You can do all of those things with a strong type system as well, and get the benefits of all of them.
These arguments unfortunately fail flat in front of industrial use. AWS could be considered "critical" by most metrics and what is is it written in? Java
Modern Java supports everything in the blogpost, so nothing stops AWS from adopting the style.
I really don’t like the argument calling “industrial usage” just because a main company or FAANG aren’t using the tech stack, but arbitrary under the hood are doing basically the same stuff with internal toolings that should be entirely under the language features, not under a system design library.
But your take about modern Java is correctly, and they adopt this style under internal projects for some workflows.
But your take about modern Java is correctly, and they adopt this style under internal projects for some workflows.
Yes.
Something I haven't seen talked about, though, is how powerful the type system is for constraining LLMs when using them to generate code. I was recently trying to get LLMs to generate code for a pretty vague and complex task in Haskell. I wasn't having much luck until I defined a very clear set of types and organized them into a very clear and constrained interface that I asked the LLM to code to. Then the results were much better!
Sure, you can use these same techniques in less strongly typed languages like Rust, and you can probably also use a similar approach in dynamically typed languages, but Haskell's pure functions allow you to create much stronger guard rails constraining what kinds of code the LLM can write.