"Five-Point Haskell": Unconditional Election (via Parametricity)
by Justin Le ♦
Welcome back to 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 run into in my time.
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.
However, stopping here gives us an incomplete picture. Firstly, types aren’t just about preventing bad behaviors. They’re about designing good code. Secondly, there is only so much you can do by picking careful structures and making invalid states unrepresentable. These are still human tools with human flaws.
The next point, to me, is about an aspect of the type system that I see little coverage of, but is a doctrine of design that I reach for in almost everything I write. It’s about leveraging the unyielding properties of math itself to take care of our fate, even when we are unable to structure our types well.
So, when writing Haskell, remember Unconditional Election.
Unconditional Election: The power of the
forallto elect or reprobate instantiations and implementations through parametric polymorphism. These properties aren’t based on any conditional ad-hoc aspect of types, but are truly unconditional, predestined by universal quantification.Surrender your control to parametric polymorphism in all things. Embrace the “free”-dom of “Free Theorems” from one of Haskell’s greatest unexpected strengths: the type parameter.
Choice is a Prison
Conditional Election
Learning Haskell can be a journey full of surprises, but this was one of the ones that blew my mind the most.
Let’s think of a polymorphic function in Java that takes a value of any type and returns something of that same type:
static <T> T foo(T x)What could that function do?
Well, it could do IO or throw an exception, mutate the input, or possibly be non-terminating, but let’s assume all it (and every other example here) does is purely return a value without mutation. What could it do?
The answer: pretty much anything. It could return the same value it was given, except if it is an Integer, in which case it negates it:
static <T> T foo(T x) {
if (x instanceof Integer i) {
return (T) Integer.valueOf(-i);
}
return x;
}Same deal in TypeScript or pretty much any other typed language without parametricity:
function foo<T>(x: T): TYet again, we have conditional election:
function foo<T>(x: T): T {
if (typeof x === "number") {
return (-x) as any as T;
}
return x;
}But how about Haskell?
foo :: a -> a(For the rest of this post, let’s ignore non-termination1 and other escape hatches2)
Because Haskell has type erasure and no runtime reflection, the only possible implementation is simply:
foo :: a -> a
foo x = xSo, there is an invariant that appeared somehow in our code: a function of type forall a. a -> a must leave its value unchanged!
But wait…says who? Did we insert some sort of const compiler annotation? Did we add some sort of annotation or pre- and post-condition that the value cannot change? Are we relying on any sort of foreseeable property of the value given?
No, this behavior is actually intrinsically fixed! We got this theorem for free. No need for any sort of work, no need for any foreseen faithfulness. We didn’t even have to write the function before knowing all it possibly could be.
This is the power of the forall. The above foo :: a -> a can be considered “sugar” for:
foo :: forall a. a -> aIf you don’t add a forall a, it is implicitly added. Some languages, like PureScript and Dhall, require the forall in every case to be explicit. You can think of the “forall” as like template <typename T> in C++, a declaration of what type variable is being quantified over.
Anyway, let’s consider another type signature:
static <T> String foo(T x)Even if we disallow IO (like getting the time, or system state), in Java (and most other languages), this again could literally be anything. You can serialize the object with toString, or you can get its class using getClass…
static <T> String foo(T x) { return "hello"; }
static <T> String foo(T x) { return x.toString(); }
static <T> String foo(T x) { return x.getClass().getSimpleName(); }In Haskell? A forall a. a -> String cannot use its input! It must be a constant string!
foo :: a -> String
foo _ = "hello"
-- or
foo _ = "goodbye"
-- or
foo _ = "i always ignore my input"In fact, there is an isomorphism between String and forall a. a -> String (fun exercise: write it!)
You can “selectively” bring in capabilities using typeclasses:
foo :: Show a => a -> String
foo _ = "hello"
-- or
foo x = show x
-- or
foo x = "reversed: " <> reverse (show x)But there are still properties you can enforce: the resulting string can only depend on the input as far as what is revealed in its Show instance. Any property not in its Show instance is off-limits.
Alternatively, you can think of foo :: Show a => a -> String as:
foo :: (a -> String) -> a -> String
foo showVal x = -- ...and you can see that the only way you can ever inspect a is through the singular inspection-lens a -> String that you are given. No getClass(), no back doors, etc.
The Guessing Game
One game Haskellers often play day-to-day is “guess the properties that the forall ensures” on different type signatures. Let’s try it out!
For example:
mystery :: a -> b -> amystery has to be \x _ -> x — there is no other option.
How about:
turmeric :: ((a, b) -> c) -> a -> b -> cIf you think about it, the only option is:
turmeric :: ((a, b) -> c) -> a -> b -> c
turmeric f x y = f (x, y)You can go pretty far down this lane using Haskell as a theorem prover, in that the type signature represents a proposition and the implementation represents a proof of that claim. But we’re not going to go down that route for now, since most practical code is not theorem-proving.
But let’s look at something a bit more structural. How about:
theThing :: [a] -> [a]What could this do?
Well, we know that all items from the result list must be from the input list. It must be a “subset” — but the ordering or multiplicity can change. And more importantly, it can’t depend on anything about the properties of any a. We also know that if the input is empty, so must be the output.
From this, we can derive what are called free theorems to look at properties that any implementation must have. Namely, mapping a function over the list and calling theThing must be equivalent to calling theThing and then mapping:
theThing . map f
== map f . theThingCan you see why? Think of any possible implementation — reverse, take 3, etc. — and see how this must be the case. However, this is not true for i.e. sort :: [Int] -> [Int]. Because sort depends on the actual properties of the items, map f could change the properties that sort depends on!
ghci> sort . map abs $ [5,-1,3,-7]
[1,3,5,7]
ghci> map abs . sort $ [5,-1,3,-7]
[7,1,3,5]Compared to an actual function with the polymorphic type, like take 3:
ghci> take 3 . map abs $ [5,-1,3,-7]
[5,1,3]
ghci> map abs . take 3 $ [5,-1,3,-7]
[5,1,3]How about:
doIt :: [a] -> Maybe aThink about what this can’t do. It clearly selects a single item, but:
- The single item cannot be determined based on any quality or merit of that item — it can’t be the smallest, the largest, etc.; it has to depend purely on the position in the list and the length of the list
- If given an empty list, it must return
Nothing
And again we have the same free theorem, doIt . map f == fmap f . doIt. No matter how you implement doIt, it is guaranteed to commute with map and fmap!
-- no free theorem: `minimumMay :: [Int] -> Maybe Int`
ghci> minimumMay . map abs $ [5,-1,3,-7]
Just 1
ghci> fmap abs . minimumMay $ [5,-1,3,-7]
Just 7
-- free theorem: `listToMaybe :: [a] -> Maybe a`
ghci> listToMaybe . map abs $ [5,-1,3,-7]
Just 5
ghci> fmap abs . listToMaybe $ [5,-1,3,-7]
Just 5
-- free theorem: `lastMay :: [a] -> Maybe a`
ghci> lastMay . map abs $ [5,-1,3,-7]
Just 7
ghci> fmap abs . lastMay $ [5,-1,3,-7]
Just 7Let’s try another one:
collapse :: [a] -> IntWhat could this possibly do? Well, we can rule out things like sum because we can’t use any property of the values themselves. The only things that this could return are constant functions and functions that depend on the length but not the contents of the list. We also have another free theorem, collapse . map f == collapse: mapping a function shouldn’t change the output, because none of the actual values matter.
-- no free theorem: `sum :: [Int] -> Int`
ghci> sum . map abs $ [5,-1,3,-7]
16
ghci> sum [5,-1,3,-7]
0
-- free theorem: `length :: [a] -> Int`
ghci> length . map abs $ [5,-1,3,-7]
4
ghci> length [5,-1,3,-7]
4
-- free theorem: `const 10 :: [a] -> Int`
ghci> const 10 . map abs $ [5,-1,3,-7]
10
ghci> const 10 [5,-1,3,-7]
10How about something in the opposite direction:
duper :: a -> [a]From this type signature, we can conclude that the final list must contain the same item! The only possible inhabitants are replicate n for some n, or repeat.3
Again, we have a free theorem: map f . duper == duper . f
-- no free theorem: `take 3 . iterate (+1) :: Int -> [Int]`
ghci> take 3 . iterate (+1) . negate $ 4
[-4,-3,-2]
ghci> map negate . take 3 . iterate (+1) $ 4
[-4,-5,-6]
-- free theorem: `replicate 3 :: Int -> [Int]`
ghci> replicate 3 . negate $ 4
[-4,-4,-4]
ghci> map negate . replicate 3 $ 4
[-4,-4,-4]How about continuations?
consumeInt :: forall r. (Int -> r) -> rThis might look exotic, but think about what it must do. It receives a function Int -> r and must produce an r. The only way to produce an r for all possible r is to apply the given function to some fixed Int chosen ahead of time. This type is actually isomorphic to Int itself: the only inhabitant is \f -> f x for some fixed x.4
consumeInt :: forall r. (Int -> r) -> r
consumeInt f = f 42 -- must be a fixed `Int`, cannot dynamically change
consumeString :: forall r. (String -> r) -> r
consumeString f = f "hello" -- must be a fixed `String`, cannot dynamically changeWhat’s better than one type variable? How about two?
mapMaybe :: (a -> Maybe b) -> [a] -> [b]Because this has to work for all a and b, we know that the only possible bs you can find in your result list are bs that you get from the a -> Maybe b function. So, you can be sure that the implementation doesn’t conjure out any arbitrary b except for the specific ones producible by your a -> Maybe b. For example, if you pass it a function that returns only even integers, the resulting list will only ever contain even integers!
One final one, with a higher-kinded type variable:
traverseIO :: (a -> IO b) -> [a] -> IO [b]
-- vs
traverse :: Applicative f => (a -> f b) -> [a] -> f [b]What invariant does the second add over the first? Even if you only ever plan on calling things with IO, the second gives you a new invariant: there won’t be any “stray” IO actions other than what is given in the a -> f b. In the first one, you never know if the resulting IO action might include a putStrLn "hello" or a launchMissiles. You definitely don’t want any functions doing sneaky IO behind your back!
The More you Surrender
Practically, this becomes similar to the principle of least power, the idea that you should use the tools with the least power necessary to do your job. Say you are writing a function that shuffles a list of items, important for your business logic. You can encode exactly what business logic is being done by adding more and more parametricity.
- If your type is
[Int] -> [Int], you know your function has pretty much no restriction on what it can do. It can even look at the machine representation of your values. - If your type is
Num a => [a] -> [a], you know that it can possibly numerically transform the items in your list, or even conjure up new items. - If your type is
Ord a => [a] -> [a], you know that your business logic is allowed to look at the ordering between items in the list, but cannot return any items that weren’t in the original list. - If your type is
[a] -> [a], you know that your logic can only affect the permutation and multiplicity of items in your list. - If your type is
Foldable t => t a -> [a], you know that results come from the input, but you can still reorder, duplicate, or drop elements. Furthermore, the resulting permutation is “pre-determined” before you receive any input items. - If your type is
Functor f => f Int -> f Int, if you call with[], you know that the length and ordering of the result will be preserved, and also any mappings ofInts will be done purely. - If your type is
Monad m => m a -> m a, if you call with[], you know that the lengths of your results will always be integer powers of the length of the input, and each input element will be duplicated the same number of times. So, if you give it[1,2,3], you know the result’s length has to be of the form3^kand must contain3^(k-1)copies of1,2, and3, in some order.
By switching from concrete types slowly to parametric types, you surrender control of what your functions can do, and create stronger and stronger guarantees. In other languages, or with refinement types, you might have to explicitly declare a post-condition like “the final values must all come from the original list”. With parametric polymorphism, this is already guaranteed and elected, no matter what the implementation is.
You can also play this game in the other direction: instead of writing a post-condition like “the length of the list must be preserved”, you can try to figure out the level of power you need to get that. For example, if you wanted to ensure “the result must have the same number of Int items (if you give it a list), but the order can depend on the actual inspection of the items”, how would you give that type?
And (spoilers) why does Traversable f => f Int -> f Int work? And, why, when you pass it a tree of Ints, does it even preserve the shape of the tree while freely allowing shuffling between actual leaves based on the Int values themselves?
It’s Only Natural
As an aside, did you wonder where I got those free theorems from? In the examples above, they come from naturality. Basically, any forall a. (Functor f, Functor g) => f a -> g a corresponds to a natural transformation in category theory, and so must commute with any fmap.
Basically, if you have a natural transformation h :: forall a. F a -> G a, with Functor F and Functor G, then we have:
h . fmap f
== fmap f . hThe above examples, forall a. [a] -> [a], forall a. [a] -> Maybe a, etc. all arise from this. But you might have to think carefully to see that forall a. a -> [a] is really forall a. Identity a -> [a]. And can you think of the Functor that gives us naturality for forall a. [a] -> Int?5
Maybe more surprising than the fact that these free theorems exist is the fact that their root is intrinsically tied to a branch of math as obscure and esoteric as “category theory”!
Add a Type Variable
Let’s say I had a data type like:
data User = User
{ userId :: Int
, userName :: String
, userAge :: Int
}And we have a function to process the user, like:
processUser :: User -> IO UserHow can we enforce that the userId is not changed?
Maybe if we were in C, we could have a const field:
struct User {
const int userId;
char userName[20];
int userAge;
};But, this applies to all usage of the User struct…what if we only wanted to preserve this property on a single function? You can’t declare struct-level const on a single argument!
Instead, we can enforce this by making userId’s type parameterized:
data User uid = User
{ userId :: uid
, userName :: String
, userAge :: Int
}
-- | Guaranteed not to change the ID
processUser :: User uid -> IO (User uid)Is this constraint enforced because we carefully designed the structure of our type? Is it constrained because we added compiler annotations or refinement types or static analysis? Not quite! It truly did come for free.
Or, consider a checklist item:
data Checklist = Checklist
{ updated :: UTCTime
, items :: [(Status, String)]
}What if I wanted to write a function that processed items without adding or removing any? Just each item in-place?
-- | Invariant: Preserves the ordering of items, and their number.
updateItems :: Checklist -> IO ChecklistHow can we make sure all our implementations are elected to only be implementations that don’t modify the length of items?
Again the answer can be: add quantification!
data Checklist t = Checklist
{ updated :: UTCTime
, items :: t (Status, String)
}
-- | Guaranteed to preseve the same number of `items` (or, number of item
-- "slots"), but can still perform IO to get the new Status and String
updateItems :: Traversable t => Checklist t -> IO (Checklist t)For an example of a possible implementation:
updateSingleItem :: (Status, String) -> IO (Status, String)
updateItems :: Traversable t => Checklist t -> IO (Checklist t)
updateItems c0 = do
newItems <- traverse updateSingleItem (items c0)
newUpdated <- getCurrentTime
pure (Checklist newUpdated newItems)Try as you might, you can’t make an implementation that gives you a different number of items than when you started (even though you can rearrange or replace them).
Note that we are not adding type parameters for abstraction or to be able to use “exotic checklists” (Checklist Maybe). Instead, we are intentionally using them universally quantified in functions that process them, in order to take advantage of these automatically enforced properties.
This intersects a lot with the Higher-Kinded Data pattern. Maybe we do have data we want to have multiple structural versions of:
data UserF f = User
{ userName :: f String
, userAge :: f Int
}
type User = UserF Identity
type NullableUser = UserF Maybe
type UserParser = UserF Parser
type UserDocs = UserF (Const Doc)
type UserPrinter = UserF (Op String)In this case, a function like
processUser :: Functor f => UserF f -> UserF fwill give you a different, unique guarantee for every “shape” your user has:
- For
UserF Maybe, the quantification ensures that the null-or-present property of each field is preserved - For
UserF Parser, it ensures that all of the “parsing” logic, and the set of strings that are validly parsed, is preserved - For
UserF (Const Doc), it ensures that the per-fieldDoc/documentation is never changed or updated.
For an example, we can write:
processUser :: Functor f => UserF f -> UserF f
processUser user = User
{ userName = fmap (map toUpper) (userName user)
, userAge = fmap (+ 1) (userAge user)
}This is guaranteed to keep nullable fields null if UserF Maybe, preserve all successful parses if UserF Parser, and leave any field-level documentation unchanged if UserF (Const Doc).
All of these properties are mathematically enforced, unconditionally. It doesn’t depend on any foreseen property of the types or values we use. These guarantees free us to be able to confidently use these functions without fear of invariants breaking.
This game becomes even stronger when you consider dependent typing, where we can express more complex relationships between type variables. For example, in the case where you have a phantom type (like in this singletons tutorial):
data DoorState = Opened | Closed | Locked
data Door (s :: DoorState)
processDoor :: Door s -> IO (Door s)processDoor, by virtue of taking forall s, must leave the door state unchanged! It can never open a closed door, unlock a locked door, etc.
For things like fixed length vectors, where the length n parameter is the size, what invariant do you think is preserved in:
something :: Vector n a -> Vector n aWe know that the length of the result must be the same as the length of the input. Furthermore, with the forall a, we know that every item in the result must come from the input, but we might rearrange or change the multiplicity of the occurrences as long as they add to the same original total number. This might be a good candidate for a function like reverse.
Or, consider:
somethingElse :: Vector n a -> Vector (n - 1) aFrom this, we know that the original vector must be non-empty! Because of how the types must flow for whatever n you give it, this requires n >= 1.
Ranking Up
Now that you see how useful it is to use type parameters and forall, can we use this fact at the meta-level even within our code itself?
Ensuring structural preservation
Let’s say we want to map an IO function over every item in our UserF, and return a new one. We know that whatever IO function we use must leave the actual “result” type unchanged. So that means we must take a forall a. f a -> h (f a).
traverseUser
:: Applicative h
=> (forall a. f a -> h (g a))
-> UserF f
-> h (UserF g)
traverseUser f u = User <$> f (userName u) <*> f (userAge u)Here again we use the trick above to generalize for all Applicative h instead of concretely IO, so we can know that the final action can’t sneak in stray IO.
Ensuring lexically-confined resources
We can also use this property in phantom types to enforce lexically-confined resources. Let’s say we are simulating local variables in an IntMap:
newtype Var = Var Int
newtype Memory v = Memory { getMemory :: IntMap v }
initVar :: v -> State (Memory v) Var
initVar x = state $ \(Memory mp) ->
case IM.lookupMax mp of
Nothing -> (Var 0, Memory $ IM.insert 0 x mp)
Just (i, _) -> (Var (i + 1), Memory $ IM.insert (i + 1) x mp)
readVar :: Var -> State (Memory v) v
readVar (Var i) = gets ((IM.! i) . getMemory)
writeVar :: Var -> v -> State (Memory v) ()
writeVar (Var i) x = modify (Memory . IM.insert i x . getMemory)
runWithMemory :: State (Memory v) a -> a
runWithMemory = (`evalState` Memory IM.empty)(By the way, what do we gain from having the state be IntMap v parametric on v? What guarantees/invariants do we get, what sort of actions do we forbid the library itself from doing? Is it possible to have a default-initialized variable?)
We can run operations like:
getFib :: Int -> State (Memory Int) Int
getFib n = do
a <- initVar 0
b <- initVar 1
replicateM_ n $ do
newSum <- (+) <$> readVar a <*> readVar b
writeVar a =<< readVar b
writeVar b newSum
readVar bghci> runWithMemory (getFib 10)
55But now our variables are not actually scoped. We could, for instance, run runWithMemory inside itself:
myAction :: State (Memory String) a
myAction = do -- new memory starts out empty
v <- initVar "hello" -- memory is now (0, "hello")
let x = runWithMemory $ do -- new memory starts out empty
readVar v -- runtime error, looking up '0' in empty map!
-- ..
-- ..Now readVar v will fail! Remember that v is Var 0, but that 0 key only has meaning in the outer scope. In the inner scope, 0 refers to a different IntMap, where it is undefined.
We can also do something silly like returning a Var:
ghci> runWithMemory (initVar "hello")
Var 0And now that var exists outside its scope. Its binding is gone, so the name no longer refers to anything meaningful.
We can prevent this by associating every variable with the scope that created it. Then we can ensure that runWithMemory requires the scope phantom to never be a part of the final output:
newtype Var s = Var Int
newtype Memory s v = Memory { getMemory :: IntMap v }
initVar :: v -> State (Memory s v) (Var s)
readVar :: Var s -> State (Memory s v) v
writeVar :: Var s -> v -> State (Memory s v) ()
runWithMemory :: (forall s. State (Memory s v) a) -> a
runWithMemory = (`evalState` Memory IM.empty)Here, a Var s must come from a Memory s v with the same scope s. It is associated with that scope, and no others. The forall here ensures that the action being given cannot unify with any external s: the scope is freshly created by runWithMemory.
Right off the bat, this prevents passing variables into nested calls (the first var’s s is different than the inner scope’s s), but this also prevents variables from leaking. That’s because the result type a must be fully independent of the s, so returning a Var s is illegal, since that would require the a to depend on s, which escapes the scope of the forall. (This is exactly how the ST monad works in GHC standard libraries, actually.)
By requiring the caller to give up control of the s, we ensure lexical confinement both of the library and of the user-given continuation. Now this safety doesn’t come from carefully tracking where variables came from. Instead, it is assured through the universality of the forall and the unconditional properties it enforces.
Habits to Build
Let’s look at what it looks like to recognize this principle in practice, and use it in your code. Let’s imagine we have a function that you can use to deploy a new Config in your environment:
deployConfig :: Config -> IO ()But, deployment is a bit expensive. So we want to deduplicate our deploys: deploying the same Config twice would be a no-op. We can do this by keeping a Config in an IORef:
-- | returns True if changed, otherwise False if already deployed
updateConfig :: IORef Config -> Config -> IO Bool
updateConfig cache newConfig = do
oldConfig <- readIORef cache
if oldConfig == newConfig
then pure False
else do
deployConfig newConfig
writeIORef cache newConfig
pure TrueThis works, but after learning about the principles in this post, that type signature should feel a little bit suspicious to you. Note that our function never actually inspects the Config at all. The logic is independent. Would there be any value in pulling out the caching logic generically?
cachedUpdate :: Eq a => (a -> IO ()) -> IORef a -> a -> IO Bool
cachedUpdate action cache newVal = do
oldVal <- readIORef cache
if oldVal == newVal
then pure False
else do
action newVal
writeIORef cache newVal
pure True
updateConfig :: IORef Config -> Config -> IO Bool
updateConfig = cachedUpdate deployConfigLet’s presume that we never intend to reuse cachedUpdate. So, we just increased our total lines of code…and for what? What does cachedUpdate get us?
Firstly, in the original monomorphic updateConfig, written directly against Config, there is so much that could go wrong. Maybe you could mis-handle the configuration or accidentally modify it. You could set certain fields to fixed values. You might end up deploying a configuration that was never passed in directly.
In our cachedUpdate implementation, we are sure that any Config deployed will only come directly from calls to updateConfig. No other operations are possible.
Secondly, the type signature of cachedUpdate tells us a lot more about what cachedUpdate’s intended logic is and what exactly it can support. Let’s say in the future, a new requirement comes: Deploy a “default” configuration if deployConfig ever fails.
You want something as drastic as this to require you to change your types and your contracts. In fact, if a new requirement comes along and you are able to implement it without changing your types, that should be extremely scary to you, because you previously allowed way too many potentially invalid programs to compile.
If we were to add such a change (“deploy a default Config”), it should have us go back to the type signature of cachedUpdate and see how it must change in order for us to support it. That process of interrogation makes us think about what we actually want to do and how it would fundamentally change our data flow.
If you subscribe to “SOLID” programming, this should all remind you of “Dependency Inversion”.
Basically: treat all monomorphic code with suspicion. It may be a symptom of you trying to hold on to more control, when you should be letting go.
Another example of the same instinct: say you have a function that broadcasts a notification to a list of users:
notifyUsers :: [User] -> Text -> IO ()How can this branch on the users? Really, in any way. It could inspect each user, craft different messages for admins vs. regular users, silently skip certain users, log personal data, vary behavior based on user properties…
Compare that to:
notifyAll :: Foldable t => t recipient -> (recipient -> IO ()) -> IO ()notifyAll is parametric in recipient. It cannot inspect who it is notifying. It cannot skip recipients based on their properties or treat admins differently from regular users. All of that “policy” logic is forced to live in the caller. The broadcasting logic itself must be uniform: it calls send indiscriminately on some fixed subset of the elements. It can pick a subset to send to, but it can’t pick what gets included in that subset based on the properties of the recipient.
Embracing Unconditional Election
What sort of control are you trying to hang on to in life, in a way that puts you in your own prison?
To me, the fact that making code more polymorphic and giving up information is valuable not just for abstraction, but for taking advantage of universal properties, was a surprising one. But ever since I started writing Haskell, it’s a fact that I take advantage of every day. So, next time you see the opportunity, try thinking about what that parametric forall can do for you. Take advantage of the doctrine of Haskell predestination that arrives from properties of logic determined before our universe ever existed.
The Next Step
Embracing Total Depravity and Unconditional Election should redefine your relationship with your code. But not all code lives in the nice pure world where we can cordon off effects. forall a. [a] -> [a] is very different than forall a. [a] -> IO [a], after all.
To extend these boundaries to useful code, we have to deal with that boundary between the world of the pure and the world where things actually happen for real. We’ll explore the nuances of that boundary in the next chapter of Five-Point Haskell, Limited Atonement.
Special Thanks
I am very humbled to be supported by an amazing community, who make it possible for me to devote time to researching and writing these posts. Very special thanks to my supporter at the “Amazing” level on patreon, Josh Vera! :)
This is the “Fast and Loose Reasoning” condition (Danielsson et al.).↩︎
Excluding
unsafePerformIO,unsafeCoerce, etc.↩︎If you disallow
repeat,forall a. a -> [a]is actually isomorphic to the natural numbers!↩︎This is actually the essence of Yoneda lemma I think, whatever that is.↩︎
It’s
forall a. [a] -> Const Int a!↩︎