more changes

Author: mstksg

copy/entries/five-point-haskell-1.md

@@ -18,9 +18,9 @@ With a new age of software development coming, what does it even mean to write
 good, robust, correct code? It is long overdue to clarify exactly the mindset
 on which we approach and define "good" coding principles.
 
-In this series, [*Five-Point Haskell*][Five-Point Haskell], let's set out to
-establish a five-point unified framework of the "Typed Functional Programming"
-(and Haskell-derived) programming philosophy aimed to create code that is
+In this series, *[Five-Point Haskell][]*, let's set out to establish a
+five-point unified framework of the "Typed Functional Programming" (and
+Haskell-derived) programming philosophy aimed to create code that is
 maintainable, correct, long-lasting, extensible, and beautiful to write and
 work with. We'll try to reference real world case studies with and actual
 examples when we can, and also attempt to dispel thought leader sound-bytes
@@ -338,10 +338,25 @@ and has been the source of many frustrating bug hunts.
 [sock_sendpage]: https://www.rapid7.com/db/modules/exploit/linux/local/sock_sendpage/
 [gcp]: https://www.thousandeyes.com/blog/google-cloud-outage-analysis-june-12-2025
 
-Why do we do this to ourselves? Because it is convenient. It's not easy to make
-a "integer or not found" type in C or javascript without some sort of
-side-channel. Imagine if javascript's `String.indexOf()` instead expected
-continuations on success and failure and became much less usable as a result:
+There's also [CVE-2008-5077][], because [EVP_VerifyInit][] returns `0` for
+false, `1` for true, and `-1` for error! So some OpenSSL code did a simple
+if-then-else check (`result != 0`) and treated error and true the same way.
+Whoops.
+
+[CVE-2008-5077]: https://www.invicti.com/web-application-vulnerabilities/openssl-improper-input-validation-vulnerability-cve-2008-5077
+[EVP_VerifyInit]: https://docs.openssl.org/1.1.1/man3/EVP_VerifyInit/
+
+Why do we do this to ourselves? Because it is convenient. In the case of
+`EVP_VerifyInit`, we can define an enum instead...
+
+```haskell
+data VerifyResult = Success | Failure | Error
+```
+
+However, it's not easy to make a "integer or not found" type in C or javascript
+without some sort of side-channel. Imagine if javascript's `String.indexOf()`
+instead expected continuations on success and failure and became much less
+usable as a result:
 
 ```haskell
 unsafeIndexOf :: String -> String -> Int
@@ -546,6 +561,54 @@ getUser conn uid = do
 Pushing it to the driver level will also unify everything with the driver's
 error-handling system.
 
+### Boolean Blindness
+
+At the heart of it, the previous examples' cardinal sin was "boolean
+blindness". If we have a predicate like `validUsername :: String -> Bool`, we
+will branch on that `Bool` once and throw it away. Instead, by having a
+function like `mkUsername :: String -> Maybe Username`, we _keep_ the proof
+alongside the value for the entire lifetime of the value. We basically pair
+the string with its proof forever, making them inseparable.
+
+There was another example of such a thing earlier: instead of using `null ::
+[a] -> Bool` and gating a call to `mean` with `null`, we instead use
+`nonEmpty :: [a] -> Maybe (NonEmpty a)`, and pass along the proof of
+non-emptiness alongside the value itself. And, for the rest of that list's
+life, it will always be paired with its non-emptiness proof.
+
+Embracing total depravity means always keeping these proofs together, with the
+witnesses bundled with the value itself, because if you don't, someone is going
+to assume it exists when it doesn't, or drop it unnecessarily.
+
+Boolean blindness also has another facet, which is where `Bool` itself is not a
+semantically meaningful type. This is "semantic boolean blindness".
+
+The classic example is `filter :: (a -> Bool) -> [a] -> [a]`. It might sound
+silly until it happens to you, but it is pretty easy to mix up if `True` means
+"keep" or "discard". After all, a "water filter" only lets water through, but a
+"profanity filter" only rejects profanity. Instead, how about `mapMaybe :: (a
+-> Maybe b) -> [a] -> [b]`? In that case, it is clear that `Just` results are
+kept, and the `Nothing` results are discarded.
+
+Sometimes, the boolean is ambiguous to what it means. You can sort of interpret
+the [1999 Mars Polar Lander][polar] crash this way. Its functions took a
+boolean based on the state of the legs:
+
+[polar]: https://en.wikipedia.org/wiki/Mars_Polar_Lander
+
+```haskell
+deployThrusters :: Bool -> IO ()
+```
+
+and `True` and `False` were misinterpreted. Instead, they could have considered
+semantically meaningful types: (simplified)
+
+```haskell
+data LegState = Extended | Retracted
+
+deployThrustrs :: LegState -> IO ()
+```
+
 ### Resource Cleanup
 
 Clean-up of finite system resources is another area that is very easy to assume

copy/entries/five-point-haskell-2.md

@@ -1,13 +1,41 @@
 ---
 title: "\"Five Point Haskell\" Part 2: Unconditional Election"
 categories: Haskell
-tags: functional programming, type safety
+tags: functional programming, type driven development
 create-time: 2026/01/01 21:51:17
 identifier: five-point-haskell-2
 slug: five-point-haskell-part-2-unconditional-election
 series: five-point-haskell
 ---
 
+Welcome back to my series, *[Five-Point Haskell][]*! This is my attempt to
+codify principles of writing robust, maintainable, correct, clear, and
+effective code in Haskell and to dispel common bad practices or heresies I have
+ran into in my time.
+
+[Five-Point Haskell]: https://blog.jle.im/entries/series/+five-point-haskell.html
+
+In the last post, we talked about [Total Depravity][], which is about treating
+any mentally-tracked constraint or condition as inevitably leading to a
+catastrophe and denouncing the reliance on our flawed mental context windows.
+Embracing the doctrine of total depravity helps us eliminate bugs and potential
+errors through our types.
+
+[Total Depravity]: https://blog.jle.im/entry/five-point-haskell-part-1-total-depravity.html
+
+But, types don't only prevent bugs: they also help us in the process of
+designing and structure our programs! So, let's jump right into our second
+point in five-point Haskell: **Unconditional Election**!
+
+> Unconditional Election: The _structure_ of your types fully determine the
+> values and states it will ever take. Nothing at runtime can ever circumvent
+> this.
+>
+> Therefore, take advantage and design the structure of your _types_ to
+> anticipate the logic you want to model. The program is pre-destined before
+> you even write any functions.
+
+
 <!-- ### Squished Pipeline -->
 
 <!-- Along the same lines, there is often the temptation to squish multiple stages -->

copy/entries/five-point-haskell-3.md

@@ -0,0 +1,12 @@
+---
+title: "\"Five Point Haskell\" Part 3: Limited Atonement"
+categories: Haskell
+tags: functional programming, type safety
+create-time: 2026/01/03 16:17:50
+identifier: five-point-haskell-3
+slug: five-point-haskell-part-3-limited-atonement
+series: five-point-haskell
+---
+
+> Limited Atonement: The goal in Haskell is not "universal purity", but the
+> correct partition of pure and impure.

copy/entries/five-point-haskell-4.md

@@ -0,0 +1,15 @@
+---
+title: "\"Five Point Haskell\" Part 4: Irresistible Grace"
+categories: Haskell
+tags: functional programming, type safety
+create-time: 2026/01/03 16:37:16
+identifier: five-point-haskell-4
+slug: five-point-haskell-part-4-irresistible-grace
+series: five-point-haskell
+---
+
+> Irresistible Grace: When you set up your type safety correctly, the compiler
+> forces you to handle all things appropriately. Create irresistible contracts,
+> and consumers are forced to be safe. Also mention auto-deriving instances
+> somehow I guess.
+

copy/entries/five-point-haskell.md

@@ -110,13 +110,19 @@ Theme: "Postmortems" of real world accidents, programming gore.
 *   Shotgun validation/parser inside database, accidentally save unvalidated
     data
 
+TODO:
+
+*   Boolean blindness
+*   Crash early: you're not going to catch every exception. don't use
+    `SomeException` either.
+
 Unconditional Election
 ----------------------
 
 Idea: The choice of the type's structure will fully determine the values
 allowed. Bad states are unrepresentable.
 
-Theme: Parse, don't validate type things
+Theme: Type-Driven Development, Prase Don't Validate
 
 *   Boolean blindness/multiple Maybe issues
 *   NonEmpty lists
@@ -125,6 +131,8 @@ Theme: Parse, don't validate type things
 *   Higher-kinded data
 *   Sized vectors
 
+*   Can we do parametric polymorphism here?
+
 Limited Atonement
 -----------------
 
@@ -151,6 +159,9 @@ Irresistible Grace
 Idea: When you set up your type-safety correctly, the compiler forces you to
 handle things appropriately
 
+Distinction from Unconditional election: happens when writing functions, not
+when writing types. I guess?
+
 Theme: Sum type branches, GADTs and witnsses, handler based programming,
 church encodings?