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

181–190 of 191 posts

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

#181

Post by Iceland_jack »

jghn wrote: post #109
mightybyte wrote: post #87

Earlier quoted context omitted.

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

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

To your point, but lispers like the author of Let Over Lambda specifically called Lisp non-functional.

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

#182

Post by foldr »

threethirtytwo wrote: post #180
foldr wrote: post #179

Earlier quoted context omitted.

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

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

You can't "hold everything else constant" because the set of programs that satisfy whatever type system is a proper subset of the set of valid programs.

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

#183

Post by jonlong »

cubefox wrote: post #168
jonlong wrote: post #134

Earlier quoted context omitted.

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…

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

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

#184

Post by threethirtytwo »

foldr wrote: post #182
threethirtytwo wrote: post #180

Earlier quoted context omitted.

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

You can't "hold everything else constant" because the set of programs that satisfy whatever type system is a proper subset of the set of valid programs.

That’s a very long and indirect jump to make.

The claim that admitting a larger set of programs improves reliability goes through several speculative steps: that the extra programs are correct, that they are simpler, that simplicity leads to fewer mistakes, and that those mistakes would not have been caught elsewhere. None of that follows from the language semantics. It’s a human-factor argument layered on top of assumptions.

By contrast, static typing removing a class of runtime failures is immediate and unconditional. Programs that would fail at runtime with type errors simply cannot execute. No assumptions about developer skill, code style, review quality, or time pressure are needed.

Even in practice, this is why dynamic languages tend to reintroduce types via linters, contracts, or optional typing systems. The extra expressiveness doesn’t translate into higher reliability; it increases the error surface and then has to be constrained again.

So the expressiveness argument doesn’t invalidate the claim. It changes the topic. One side is a direct property of the language. The other is a speculative, multi-step causal story about human behavior. That’s why the original claim is neither unfalsifiable nor “just vibes.”

So regardless of speculative human factors, the claim stands: holding the language semantics constant, static typing strictly reduces the set of possible runtime failures, and therefore strictly increases reliability in the only direct, non-contingent sense available.

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

#185

Post by [deleted] »

threethirtytwo wrote: post #184
foldr wrote: post #182

Earlier quoted context omitted.

You can't "hold everything else constant" because the set of programs that satisfy whatever type system is a proper subset of the set of valid programs.

That’s a very long and indirect jump to make. The claim that admitting a larger set of programs improves reliability goes through several speculative steps: that the extra programs are correct, that they are simpler, that simplicity leads to fewer mistakes, and that those mistakes would not have been caught elsewhere. None of that follows from the language semantics. It’s a human-factor argument layered on top of ass…

[deleted]

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

#186

Post by xpe »

jancsika wrote: post #126
xpe wrote: post #103

Earlier quoted context omitted.

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

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

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?

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

#187

Post by siwatanejo »

wiseowise wrote: post #99
hibikir wrote: post #72

Earlier quoted context omitted.

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

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

Return type DUs are so much better than checked exceptions.

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

#188

Post by cubefox »

jonlong wrote: post #183
cubefox wrote: post #168

Earlier quoted context omitted.

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

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…

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

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

#189

Post by jonlong »

cubefox wrote: post #188
jonlong wrote: post #183

Earlier quoted context omitted.

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…

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.

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

#190

Post by cubefox »

jonlong wrote: post #189
cubefox wrote: post #188

Earlier quoted context omitted.

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…

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

Post reply on HN