Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Functional programming and reliability: ADTs, safety, critical infrastructure

blog.rastrian.dev

Post reply on HN
Print view View original

161–170 of 191 posts

Re: Functional programming and reliability: ADTs, safety, critical infrastructure

#161

Post by rastrian »

fud101 wrote: post #155

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/

Re: Functional programming and reliability: ADTs, safety, critical infrastructure

#162

Post by rastrian »

tariqshams wrote: post #159
kephasp wrote: post #148

Earlier quoted context omitted.

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.

Re: Functional programming and reliability: ADTs, safety, critical infrastructure

#163

Post by rastrian »

int08h wrote: post #157
thundergolfer wrote: post #150

Earlier quoted context omitted.

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…

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 ”. To remain a…

heisen-valves are a perfect comparison, thank you.

Re: Functional programming and reliability: ADTs, safety, critical infrastructure

#164

Post by rastrian »

wiseowise wrote: post #98
jatins wrote: post #69

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.

Re: Functional programming and reliability: ADTs, safety, critical infrastructure

#165

Post by rastrian »

brabel wrote: post #128
rastrian wrote: post #43

Earlier quoted context omitted.

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 i…

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 man…

Take a look at Algebraic Effects concept, I think you would like it.

Re: Functional programming and reliability: ADTs, safety, critical infrastructure

#167

Post by bitcompost »

threethirtytwo wrote: post #142
foldr wrote: post #123

Earlier quoted context omitted.

>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 reliabi…

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

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.

Re: Functional programming and reliability: ADTs, safety, critical infrastructure

#168

Post by cubefox »

jonlong wrote: post #134
cubefox wrote: post #81

Earlier quoted context omitted.

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…

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

Re: Functional programming and reliability: ADTs, safety, critical infrastructure

#169

Post by cubefox »

jesse__ wrote: post #137
cubefox wrote: post #80

Earlier quoted context omitted.

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 , 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 heterogen…

That sounds plausible. Just like functional programming languages are imperative under the hood. It's all magic as far as I'm concerned.

Re: Functional programming and reliability: ADTs, safety, critical infrastructure

#170

Post by threethirtytwo »

thefaux wrote: post #151
threethirtytwo wrote: post #51

Earlier quoted context omitted.

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 m…

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 categori…

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.

Post reply on HN