[HN Gopher] Functional programming and reliability: ADTs, safety...
___________________________________________________________________
Functional programming and reliability: ADTs, safety, critical
infrastructure
Author : rastrian
Score : 140 points
Date : 2025-12-28 00:05 UTC (22 hours ago)
(HTM) web link (blog.rastrian.dev)
(TXT) w3m dump (blog.rastrian.dev)
| mlavrent wrote:
| 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.
| conartist6 wrote:
| 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.
| bdangubic wrote:
| godspeed with that :)
| agumonkey wrote:
| Is this a methodology you use at work or only for personal
| projects ? I'm curious how common this culture is among
| companies/teams.
| conartist6 wrote:
| 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!
| conartist6 wrote:
| 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.
| auggierose wrote:
| 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.
| conartist6 wrote:
| 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
| chrisoverzero wrote:
| > [...] 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.
| fuzztester wrote:
| I don't get your 2nd sentence: "The difference in what
| I've used" ... Can you give an example, and name the
| language used?
| chrisoverzero wrote:
| 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:
| var intValue = 3;
|
| ...I separate the conventional prefix with a space:
| int value = 3;
|
| ...so now my co-workers don't need to remember the
| convention - it's enforced by the language.
|
| (I hope this makes the joke more obvious.)
| conartist6 wrote:
| 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.
| keyle wrote:
| 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.
| zephen wrote:
| > The best argument for dynamic types systems, is enjoying
| debugging in production.
|
| This comment is either severe snark or severe ignorance.
| aag wrote:
| 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.
| rastrian wrote:
| 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.
| brabel wrote:
| 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.
| yunnpp wrote:
| Help me with a tl;dr here, but are effects just monads?
| brabel wrote:
| 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.
| acdha wrote:
| 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).
| galangalalgol wrote:
| Rust certainly isn't a pure fp language, but the borrow
| checkerbl is a lot kinder when you use fp style.
| acdha wrote:
| 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.
| rastrian wrote:
| 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."
| acdha wrote:
| 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.
| saghm wrote:
| 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.
| zelphirkalt wrote:
| 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.
| adamddev1 wrote:
| 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.
| rastrian wrote:
| 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.
| mightybyte wrote:
| 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.
| jghn wrote:
| > 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.
| agumonkey wrote:
| 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.
| jghn wrote:
| 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.
| agumonkey wrote:
| 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).
| jghn wrote:
| 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 :)
| agumonkey wrote:
| 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
| jghn wrote:
| 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.
| submain wrote:
| 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.
| charcircuit wrote:
| >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.
| discarded1023 wrote:
| You'd like to know your fault tolerance is reliable and
| possibly even correct.
| charcircuit wrote:
| 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.
| rastrian wrote:
| 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.
| nickpsecurity wrote:
| 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.
| rastrian wrote:
| 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.
| cloudhead wrote:
| False dichotomy.. if reliability matters, you have to invest in
| both. Fault tolerance is not a replacement for correctness.
| wewewedxfgdf wrote:
| I'm wary of absolute statements about programming.
| ggm wrote:
| 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?
| henning wrote:
| 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.
| saghm wrote:
| 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.
| rastrian wrote:
| 100%. Types don't replace fuzzing, property tests, chaos, or
| adversarial thinking. They just move one slice of bugs from
| runtime to compile time and make refactors safer.
|
| In hindsight I should have positioned types/ADTs as one layer
| in the reliability toolbox, not the toolbox.
| d--b wrote:
| 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.
| zelphirkalt wrote:
| 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.
| Jensson wrote:
| > 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.
| zelphirkalt wrote:
| > 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.
| breadwinner wrote:
| > _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.
| tombert wrote:
| 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.
| dionian wrote:
| Yes, they are really a poor emulation of scala which makes it
| a bit more usable.
| adamddev1 wrote:
| Mr. Error Monad enters the chat...
| hibikir wrote:
| 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.
| wiseowise wrote:
| > 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.
| cubefox wrote:
| 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.
| jesse__ wrote:
| > "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.
| cubefox wrote:
| 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?
| rastrian wrote:
| 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).
| cubefox wrote:
| 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.
| rastrian wrote:
| 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.
| cubefox wrote:
| 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.
| jesse__ wrote:
| > 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.
| cubefox wrote:
| > > 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.
| jesse__ wrote:
| 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
| cubefox wrote:
| 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.
| jesse__ wrote:
| 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?
| jadsfwasdfsd wrote:
| > 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.
| cubefox wrote:
| 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.
| jesse__ wrote:
| 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
| pastel8739 wrote:
| Most of the time when I use untagged unions, I end up adding a
| tag and logic to case on it anyway...
| adamddev1 wrote:
| 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.
| rastrian wrote:
| 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.
| jonlong wrote:
| 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.
| cubefox wrote:
| 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.
| jonlong wrote:
| 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.
| jadsfwasdfsd wrote:
| 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.
| whateveracct wrote:
| > 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.
| stingraycharles wrote:
| 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.
| rastrian wrote:
| 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.
| whateveracct wrote:
| 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.
| brabel wrote:
| And your pockets were being filled in that year while you
| were just doing cleanups. Mission accomplished.
| rastrian wrote:
| 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.
| whateveracct wrote:
| 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.
| squirrellous wrote:
| 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.
| rastrian wrote:
| 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.
| Ekaros wrote:
| 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.
| brabel wrote:
| 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.
| thundergolfer wrote:
| 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
| naive notions of system performance. System operations are
| dynamic, with components (organizational, human, technical)
| failing and being replaced continuously. --
| https://how.complexsystems.fail/
| int08h wrote:
| 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.
| FpUser wrote:
| Yet another silver bullet.
| rastrian wrote:
| Fair pushback. I agree the title and a couple of lines
| overshoot. My intent isn't "FP is a silver bullet" or "types
| replace operational reliability"
| pizlonator wrote:
| 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.
| dionian wrote:
| It improves reliability at compile time, certainly
| ux266478 wrote:
| > 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...
| rastrian wrote:
| I was searching for the Stefik article to argue here, thank
| you.
| pizlonator wrote:
| 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.
| rowanG077 wrote:
| Interesting, so you consider the entire scientific field of
| medicine to work without hard evidence?
| pizlonator wrote:
| 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).
| rowanG077 wrote:
| 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.
| pizlonator wrote:
| 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
| zephen wrote:
| If you're going to start citing research, you should look at
| the Cooley finding on verilog vs VHDL.
| therealcamino wrote:
| That's certainly an interesting data point, but it was a 90
| minute programming contest, not peer-reviewed research.
| zephen wrote:
| 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/
| patrickmay wrote:
| The benefits of static typing with regard to reliability are
| unclear, at best:
|
| https://danluu.com/empirical-pl/
| threethirtytwo wrote:
| 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.
| Spivak wrote:
| > 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.
| akkad33 wrote:
| > 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.
| shepherdjerred wrote:
| There are different levels of static typing
| threethirtytwo wrote:
| 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.
| pizlonator wrote:
| > 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.
| threethirtytwo wrote:
| 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.
| foldr wrote:
| >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.
| threethirtytwo wrote:
| >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.
| foldr wrote:
| Readability and simplicity can increase reliability,
| because simple readable code is easier to review.
| threethirtytwo wrote:
| 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.
| wiseowise wrote:
| > Functional programming often leads to write-only
| incomprehensible code; the exact opposite of what you need to
| have a reliable system.
|
| In what language?
| bonesss wrote:
| 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.
| xpe wrote:
| > ... 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...
| garethrowlands wrote:
| Citation needed.
| websiteapi wrote:
| 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.
| rastrian wrote:
| 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.
| xpe wrote:
| > 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.
| jancsika wrote:
| > 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.
| jatins wrote:
| 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
| wiseowise wrote:
| Modern Java supports everything in the blogpost, so nothing
| stops AWS from adopting the style.
| jschrf wrote:
| Tup: Use interface for structural types in TypeScript, not type.
| tasuki wrote:
| I'm impressed by the author having made so many sensible choices
| in their life, yet marrying their blog content to GitHub issues.
| rastrian wrote:
| lmao
| mightybyte wrote:
| Was just talking with someone the other day who used to write
| Haskell professionally but is now using Python. He said that in
| his experience when there are bugs the "blast radius" is much
| larger in a dynamic language like Python than in a static
| language like Haskell. That has been my experience as well.
|
| 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.
| Jeff_Brown wrote:
| 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.
| yobbo wrote:
| 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.
| kephasp wrote:
| How can you prevent code from creating a handle in a new
| place?
| ryandv wrote:
| 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: 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)
|
| ... which can be shown to satisfy the three lens laws. If you
| can understand the types it is generally true that the
| implementation falls out much more easily, in a similar vein as
| "show me your tables, and I won't usually need your flowchart;
| it'll be obvious."
|
| 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.
| agumonkey wrote:
| this makes me want to move to a haskell (or any hard fp
| language) shop in 2026..
| kephasp wrote:
| I've been using Haskell professionally for the last 5 years,
| I definitely hope I can continue!
| yunnpp wrote:
| 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.
| ryandv wrote:
| minikanren folks were already experimenting with program
| synthesis given a test suite that needs to be fully
| satisfied.
| xpe wrote:
| 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_...
| zozbot234 wrote:
| 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.
| northlondoner wrote:
| Yes.
| beders wrote:
| 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.
___________________________________________________________________
(page generated 2025-12-28 23:01 UTC)