reframe part 2

Author: mstksg

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

@@ -23,17 +23,34 @@ 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**!
+However, picking good structures, making invalid states unrepreentable, etc.
+can only go so far.
 
-> Unconditional Election: The _structure_ of your types fully determine the
-> values and states it will ever take. Nothing at runtime can ever circumvent
-> this.
+Types aren't just about preventing bad behaviors. They're about designing good
+code. And there is one principle that helps guide this design by leveraging the
+unyielding properties of the universe _itself_ to take care of our fate, even
+when we are unable to structure our types well.
+
+Let's jump into the second point in five-point Haskell: **Unconditional
+Election**!
+
+> Unconditional Election: The power of the `forall` to elect or reprobate
+> instantiations and implementations through parametric polymorphism.
 >
-> 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.
+> Invariants and correctness are not based on the foreseen merits of the
+> structure of types you choose, or on runtime reflection and ad-hoc
+> polymorphim, but rather in the predestination of universal quantification.
+>
+> Therefore, surrender to your control to parametric polymorphism in all
+> things. In simple terms: add a type parameter.
+
+<!-- > 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 -->
@@ -58,7 +75,7 @@ point in five-point Haskell: **Unconditional Election**!
 <!-- ```haskell -->
 <!-- pay :: Checkout -> IO Checkout -->
 <!-- pay c = case address c of -->
-<!--   Just addr -> do --> 
+<!--   Just addr -> do -->
 <!--     tok <- processPayment (items c) addr -->
 <!--     pure $ c { payment = Just tok } -->
 <!--   Nothing -> -- uh.... -->

copy/entries/five-point-haskell.md

@@ -109,29 +109,49 @@ Theme: "Postmortems" of real world accidents, programming gore.
 *   Use-after-free --- continuations, Acquire, ResourceT
 *   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.
+<!-- Idea: The choice of the type's structure will fully determine the values -->
+<!-- allowed. Bad states are unrepresentable. -->
+
+<!-- Theme: Type-Driven Development, Prase Don't Validate -->
+
+<!-- *   Boolean blindness/multiple Maybe issues -->
+<!-- *   NonEmpty lists -->
+<!-- *   State machine requires each step (GADT enforced?) -->
+<!-- *   Authorization payloads -->
+<!-- *   Higher-kinded data -->
+<!-- *   Sized vectors -->
+
+Idea: Parametrically polymorphic code will pre-destine what functions are
+possible. Take advantage of it to enforce invariants and what you can write,
+instead of using ie refinement types or postconditions.
+
+Theme: Guessing game, what functions are allowed?
 
-Theme: Type-Driven Development, Prase Don't Validate
+Be careful to not frame the programmer as the person who is electing the terms.
+Frame it as the type system electing the valid terms
 
-*   Boolean blindness/multiple Maybe issues
-*   NonEmpty lists
-*   State machine requires each step (GADT enforced?)
-*   Authorization payloads
-*   Higher-kinded data
-*   Sized vectors
+Give away your free will -- just be elective! constraint is liberation.
 
-*   Can we do parametric polymorphism here?
+Oh that's the key: "Constraint is liberation"! it is not by works or foreseen
+faith! the more you surrender....the safer you are! principle of least
+strength! also can maybe combine with purity in multi-threaded. restrictions
+are better.
+
+Principle of Least Strength
+
+*   Parametric polymorphism --- guess the implementation
+    *   `[Int] -> [Int]` vs `[a] -> [a]`
+    *   Compare with refinement types
+*   higher-kinded data, parametric over functors
+*   Subtyping via parametric polymorphism
+*   Phantoms + parametric polymoirphism, restrictions, ST trick
+*   Princple of least strength, Monad vs Applicative
+    *   typeclass-based limitation of functions
 
 Limited Atonement
 -----------------
@@ -176,14 +196,23 @@ church encodings?
 Perseverance of the Saints
 ---------------------------
 
-Idea: Well-typed code will survive big refactoring
+Idea: Benefits of Immutability
+
+*   Immutability
+*   Sharing --- all new data structures
+*   Multi-threaded
+*   Locks, STM
+
+<!-- Idea: Well-typed code will survive big refactoring -->
+
+<!-- Theme: Hands-on refactoring, seeing how changes propagate. Build on chained -->
+<!-- successive refactors -->
+
+<!-- *   String -> Sum Type/Enum -->
+<!-- *   Add new constructor -->
+<!-- *   Add new field to record -->
+<!-- *   `ToJSON`/`Persist` change -->
+<!-- *   Refactor "reason" to be owned by the sum type -->
+<!-- *   Property tests to help it all out -->
 
-Theme: Hands-on refactoring, seeing how changes propagate. Build on chained
-successive refactors
 
-*   String -> Sum Type/Enum
-*   Add new constructor
-*   Add new field to record
-*   `ToJSON`/`Persist` change
-*   Refactor "reason" to be owned by the sum type
-*   Property tests to help it all out