\documentclass[]{article}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\usepackage{fixltx2e} % provides \textsubscript
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
\else % if luatex or xelatex
  \ifxetex
    \usepackage{mathspec}
    \usepackage{xltxtra,xunicode}
  \else
    \usepackage{fontspec}
  \fi
  \defaultfontfeatures{Mapping=tex-text,Scale=MatchLowercase}
  \newcommand{\euro}{€}
\fi
% use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
% use microtype if available
\IfFileExists{microtype.sty}{\usepackage{microtype}}{}
\usepackage[margin=1in]{geometry}
\ifxetex
  \usepackage[setpagesize=false, % page size defined by xetex
              unicode=false, % unicode breaks when used with xetex
              xetex]{hyperref}
\else
  \usepackage[unicode=true]{hyperref}
\fi
\hypersetup{breaklinks=true,
            bookmarks=true,
            pdfauthor={Justin Le},
            pdftitle={``Five-Point Haskell'': Unconditional Election (via Parametricity)},
            colorlinks=true,
            citecolor=blue,
            urlcolor=blue,
            linkcolor=magenta,
            pdfborder={0 0 0}}
\urlstyle{same}  % don't use monospace font for urls
% Make links footnotes instead of hotlinks:
\renewcommand{\href}[2]{#2\footnote{\url{#1}}}
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
\setlength{\emergencystretch}{3em}  % prevent overfull lines
\setcounter{secnumdepth}{0}

\title{``Five-Point Haskell'': Unconditional Election (via Parametricity)}
\author{Justin Le}
\date{August 4, 2026}

\begin{document}
\maketitle

\emph{Originally posted on
\textbf{\href{https://blog.jle.im/entry/five-point-haskell-part-2-unconditional-election.html}{in
Code}}.}

\documentclass[]{}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\usepackage{fixltx2e} % provides \textsubscript
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
\else % if luatex or xelatex
  \ifxetex
    \usepackage{mathspec}
    \usepackage{xltxtra,xunicode}
  \else
    \usepackage{fontspec}
  \fi
  \defaultfontfeatures{Mapping=tex-text,Scale=MatchLowercase}
  \newcommand{\euro}{€}
\fi
% use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
% use microtype if available
\IfFileExists{microtype.sty}{\usepackage{microtype}}{}
\usepackage[margin=1in]{geometry}
\ifxetex
  \usepackage[setpagesize=false, % page size defined by xetex
              unicode=false, % unicode breaks when used with xetex
              xetex]{hyperref}
\else
  \usepackage[unicode=true]{hyperref}
\fi
\hypersetup{breaklinks=true,
            bookmarks=true,
            pdfauthor={},
            pdftitle={},
            colorlinks=true,
            citecolor=blue,
            urlcolor=blue,
            linkcolor=magenta,
            pdfborder={0 0 0}}
\urlstyle{same}  % don't use monospace font for urls
% Make links footnotes instead of hotlinks:
\renewcommand{\href}[2]{#2\footnote{\url{#1}}}
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
\setlength{\emergencystretch}{3em}  % prevent overfull lines
\setcounter{secnumdepth}{0}


\begin{document}

Welcome back to *[Five-Point
Haskell](https://blog.jle.im/entries/series/+five-point-haskell.html)*! 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](https://blog.jle.im/entry/five-point-haskell-part-1-total-depravity.html),
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 `forall` to 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:

``` java
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:

``` java
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:

``` typescript
function foo<T>(x: T): T
```

Yet again, we have conditional election:

``` typescript
function foo<T>(x: T): T {
  if (typeof x === "number") {
    return (-x) as any as T;
  }
  return x;
}
```

But how about Haskell?

``` haskell
foo :: a -> a
```

(For the rest of this post, let's ignore
[non-termination](https://www.cse.chalmers.se/~nad/publications/danielsson-popl2006-tr.pdf)[^1]
and other escape hatches[^2])

Because Haskell has type erasure and no runtime reflection, the *only* possible
implementation is simply:

``` haskell
foo :: a -> a
foo x = x
```

So, 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:

``` haskell
foo :: forall a. a -> a
```

If 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:

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

``` java
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!

``` haskell
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:

``` haskell
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:

``` haskell
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:

``` haskell
mystery :: a -> b -> a
```

`mystery` *has* to be `\x _ -> x` --- there is no other option.

How about:

``` haskell
turmeric :: ((a, b) -> c) -> a -> b -> c
```

If you think about it, the only option is:

``` haskell
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](https://blog.jle.im/entry/the-baby-paradox-in-haskell.html#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:

``` haskell
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](https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf) 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:

``` haskell
theThing . map f
  == map f . theThing
```

Can 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!

``` haskell
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`:

``` haskell
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:

``` haskell
doIt :: [a] -> Maybe a
```

Think about what this *can't* do. It clearly selects a single item, but:

1.  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
2.  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`!

``` haskell
-- 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 7
```

Let's try another one:

``` haskell
collapse :: [a] -> Int
```

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

``` haskell
-- 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]
10
```

How about something in the opposite direction:

``` haskell
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`

``` haskell
-- 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?

``` haskell
consumeInt :: forall r. (Int -> r) -> r
```

This 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]

``` haskell
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 change
```

What's better than one type variable? How about two?

``` haskell
mapMaybe :: (a -> Maybe b) -> [a] -> [b]
```

Because this has to work for *all* `a` and `b`, we know that the *only* possible
`b`s you can find in your result list are `b`s 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:

``` haskell
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 of `Int`s 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 form `3^k` and must contain `3^(k-1)` copies of `1`, `2`, and `3`, 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 `Int`s, 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](https://en.wikipedia.org/wiki/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:

``` haskell
h . fmap f
    == fmap f . h
```

The 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:

``` haskell
data User = User
    { userId :: Int
    , userName :: String
    , userAge :: Int
    }
```

And we have a function to process the user, like:

``` haskell
processUser :: User -> IO User
```

How can we enforce that the `userId` is not changed?

Maybe if we were in C, we could have a `const` field:

``` c
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:

``` haskell
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:

``` haskell
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?

``` haskell
-- | Invariant: Preserves the ordering of items, and their number.
updateItems :: Checklist -> IO Checklist
```

How 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!

``` haskell
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:

``` haskell
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](https://reasonablypolymorphic.com/blog/higher-kinded-data/) pattern. Maybe
we *do* have data we want to have multiple structural versions of:

``` haskell
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

``` haskell
processUser :: Functor f => UserF f -> UserF f
```

will 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-field `Doc`/documentation
    is never changed or updated.

For an example, we can write:

``` haskell
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](https://blog.jle.im/entry/introduction-to-singletons-1.html)):

``` haskell
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](https://blog.jle.im/entry/fixed-length-vector-types-in-haskell.html),
where the length `n` parameter is the size, what invariant do you think is
preserved in:

``` haskell
something :: Vector n a -> Vector n a
```

We 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:

``` haskell
somethingElse :: Vector n a -> Vector (n - 1) a
```

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

``` haskell
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`:

``` haskell
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:

``` haskell
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 b
```

``` haskell
ghci> runWithMemory (getFib 10)
55
```

But now our variables are not actually scoped. We could, for instance, run
`runWithMemory` *inside* itself:

``` haskell
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`:

``` haskell
ghci> runWithMemory (initVar "hello")
Var 0
```

And 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:

``` haskell
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:

``` haskell
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`:

``` haskell
-- | 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 True
```

This *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?

``` haskell
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 deployConfig
```

Let'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](https://en.wikipedia.org/wiki/SOLID),
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:

``` haskell
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:

``` haskell
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](https://xkcd.com/1312/). We'll explore the nuances of that boundary in the
next chapter of [Five-Point
Haskell](https://blog.jle.im/entries/series/+five-point-haskell.html), **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](https://www.patreon.com/justinle/overview), Josh Vera! :)

# Signoff

Hi, thanks for reading! You can reach me via email at <justin@jle.im>, or at
twitter at [\@mstk](https://twitter.com/mstk)! This post and all others are
published under the [CC-BY-NC-ND
3.0](https://creativecommons.org/licenses/by-nc-nd/3.0/) license. Corrections
and edits via pull request are welcome and encouraged at [the source
repository](https://github.com/mstksg/inCode).

If you feel inclined, or this post was particularly helpful for you, why not
consider [supporting me on Patreon](https://www.patreon.com/justinle/overview),
or a [BTC donation](bitcoin:3D7rmAYgbDnp4gp4rf22THsGt74fNucPDU)? :)

[^1]: This is the "Fast and Loose Reasoning" condition (Danielsson et al.).

[^2]: Excluding `unsafePerformIO`, `unsafeCoerce`, etc.

[^3]: If you disallow `repeat`, `forall a. a -> [a]` is actually isomorphic to
    the natural numbers!

[^4]: This is actually the essence of Yoneda lemma I think, whatever that is.

[^5]: It's `forall a. [a] -> Const Int a`!


\end{document}

\end{document}
