in Code — Entries

"Five-Point Haskell": Unconditional Election (via Parametricity)

Justin Le — Tue, 4 Aug 2026 18:15:09 UTC

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

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): T

Yet 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-termination ¹ and other escape hatches²)

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

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:

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:

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

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

How about:

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

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

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 a

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

Let’s try another one:

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.

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

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

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

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?

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 of Ints 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 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 . 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?⁵

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 User

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

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

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

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

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 b

ghci> runWithMemory (getFib 10)
55

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

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

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, 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!↩︎

LLMs Will Cheese Your Types: Fighting Back in Haskell

Justin Le — Wed, 22 Jul 2026 16:10:56 UTC

Sooo yes it’s true, I’ve been integrating LLMs and agentic coding tools in my Haskell coding since the beginning of this year for a lot of my projects, both personal and professional. I do all of my programming in Haskell, a language with a very expressive type system that encourages “type-driven development”.

Working with LLMs on writing Haskell is a very unique experience; a lot of similarities and patterns exist with “normal” agentic coding, but I think the hot flame of LLMs meeting the cool stone of Haskell yields a lot of wholly unique optimal paths, workflow quirks, and failure modes.

This post will focus on understanding what I call constraint-evading behavior in LLMs as it relates to writing Haskell effectively with LLM collaboration.

Consider this Part 1 of a series. This post is about how to spot and understand a very common failure mode of LLMs once you actually are writing “type-driven” Haskell.

The Ideal Case: Haskell and LLMs

Now, my personal opinion and wishful hope is that Haskell should be to agentic software engineering what Lean is in agentic research mathematics: a framework for LLMs to self-construct the scaffolding they need to guide themselves to their correct goal.

I don’t believe that “correctness at generation-time” is a plausible goal, not today in 2026, and probably not any time soon. Motion towards correctness is asymptotic. You might get close enough sometimes, but the long tail of correctness is…long. Even the most full-vibed frontier-model projects have large suites of tests that exist to guide the agent. Agentic coding in five years will not be “spit out the correct program”, it will be “set up the best scaffolding that guides the implementation”.

Remember: the point of types in Haskell isn’t to catch bad code. It’s to direct how you write and structure your code, guide you down the most productive paths, help you concretely iterate on what design you want, and make the actual code-writing time a smooth flow process.

Each part of this is antithetical to how LLMs are trained to use types and write code.

To this end, I try to structure my codebases with the correct scaffolding to help augment the intuition of path exploration: AI has to search which paths are the “most promising”, so I structure my code-base to quickly kill off paths that are most likely to be dead-ends or lead to unmaintainable code, and to channel AI exploration along more promising paths. The greatest tools are types, compilers, warnings, hints.

A lot of these are the same things we teach to human coders, and are not very different than what I write about regularly:

Parse, Don’t Validate: set up your types to make invalid states unrepresentable. AI will, by nature, NOT do this, even the latest frontier models. They usually slip into defensive programming (adding isNull checks everywhere, boolean checks for constructors like isNothing / isObject / isArray instead of just pattern matching, filtering lists for duplicates instead of using Data.Set, adding precondition assertions, etc.), and it’s usually up to the human driver to stop and consciously create data types that model the domain correctly, structurally prevent invalid states, enforce pre- and post-conditions via structurally verified types and not boolean checks, avoid boolean blindness, etc.

Either that, or dedicate an entire session or planning step to clarifying these domain requirements in their types.
Use warnings and linters enthusiastically: -Werror=incomplete-patterns of course, and the default -Werror usually covers a lot of AI failure modes (leaving in dead code, leaving in arguments in functions for no reason and killing opportunities for abstraction).
Add robust test suites for things that cannot be tested within the types, but also explicitly laying out integration tests: something which LLMs seem pretty allergic to without proper prompting.

From my own empirical observations, all of these things are against the nature of how even frontier LLM models operate, embedded deeply from being trained on terabytes of untyped Python and React slop.

So, I’ve been gathering a list of what I call constraint-evading behavior: when the requirements and constraints are explicitly and unambiguously stated, but LLM nature desperately tries to circumvent them because they cannot keep up a sustained fight against their deepest base impulses.

Decisions that require scrutiny

There is a class of failure modes where AI makes a risky decision that a human might reasonably make in the rare case that it is justified. But, usually, it will be making this decision because it’s the “simplest approach”. It cannot separate questionable decisions based on reasoned justification and questionable decisions based on flawed heuristics like “simplicity” or effort.

We have the general failure modes like this that people mention for all programming languages:

“This test doesn’t pass, so let’s disable it”
“Let’s feed this test junk data so it will pass.”
“Let’s have this function detect if it’s in a test environment and behave differently if it is.”

But here are some that I feel are specific to working with LLMs in Haskell.

Disabling Warnings for Escape Hatches

A lot of the “type safety” of Haskell can be bypassed trivially by disabling warnings, and a lot of the “escape hatches” within the language are disabled via linting rules (Prelude.error, unsafeCoerce, etc.)

LLMs will often add warning suppressors that straight-up disable warning or lint checks.

“Let me add -Wno-incomplete-patterns to this file so that it can compile, because this pattern is inaccessible anyway in normal operation”
“Let me add HLINT ignore to this build so that I can bypass the hlint rule forbidding Prelude.error”

It’s pretty straightforward to add post-edit hooks to forbid edits of this pattern…but I think this is a good platonic example of what I mean by “constraint-evading behavior”.

Maybe sometimes you should be disabling warnings in your files. Maybe sometimes you should be using Prelude.error. A human might look at the situation at hand and think, “this is one of those rare cases where Prelude.error is correct”, or “this is one of those rare cases where that warning is incorrect.”

But should you trust an LLM to make that judgment call? Fuck no. 99% of the time, it is only doing this as the easy way out. Yes, every once in a while it will discover a legitimate reason, but has not properly weighted P(legitimate | attempted). Most of the attempts will be as hacks, and it will be more than happy to follow through with an attempt if it truly is the “simplest way”.

Understanding something as constraint-evading behavior doesn’t mean “ban this behavior”. It is meant to help highlight situations where 99% of the time, it’s the LLM taking the easy or fast way out instead of the correct one. In these cases, it’s imperative that a human is what is adding the warning silencing or hlint ignore.

“The simplest approach is…” is the worst thing you ever want to see in a thought trace, because it’s a sure guaranteed sign that they are about to spew the most ridiculous and awful code you’ve ever seen.

Breaking down the matrix:

P(not legitimate && not attempted): Correct avoidance of problematic behavior
P(legitimate && not attempted): The noble struggle. The rare case that you are really justified in this normally risky behavior, but out of misguided principle you do not. This is a bias and failure mode more likely to be hit by humans. Or at least one human (that’s me).
P(not legitimate && attempted): The failure mode where an LLM will choose this out of a flawed heuristic like simplicity or effort.
P(legitimate && attempted): The rare case that you are justified in normally risky behavior, and the LLM was correct in attempting it.

As this matrix moves towards more favorable marginals, my stance here will slowly change. But for now, the numbers I roughly see encourage continued vigilance.

Ignoring types in planned code

Let’s say you plan your perfect types that match your domain exactly, forbidding all invalid states, perfectly monotonic parsers. Then you go to execute that plan. Unfortunately, LLMs will not hesitate to throw away your carefully designed types.

“The plan says to use NonEmpty Int as an argument, but that would require changing too much. The simplest approach is to just have it take [Int] and check for empty lists”
“We planned to use this existing enum, but it doesn’t have a branch we need. Instead of adding a branch, we’ll have it take String instead.”
“Instead of a structured data type, let’s just use stringly encoded lists or records with separators we can parse out.”
“We have to call fooFunc, which returns an Int, so let’s have our function return an Int instead of a Natural like our original plan”.
“The plan requires adding a field to this record, but to keep things simple, let’s just take a Data.Aeson.Object instead so we can return whatever fields we want.”
“The plan was to have this function be Binary a =>, but this type we defined doesn’t have a Binary instance yet, so we’ll just use Show a => instead. It’s the simplest approach.”

This is especially frustrating because often these plans and types were chosen to enforce some domain invariant or guide the proper and correct development, but LLMs will almost never hesitate before throwing away all of the planned type safety.

These are all reasonable things that a human might reconsider during the process of following out a plan. Maybe we originally wanted to use NonEmpty Int, but upon closer examination, we realized it does have to be an [Int]. This is the natural process of iterating on a design, as you discover more truths about the domain.

But, that call should be a discussed one, not an implicit one…it took thought to make the original plan, so it should take thought to change the plan. Most of the time AI makes these decisions, it isn’t out of discovered truths about the domain, but rather because of needless heuristics to minimize effort, or a misunderstanding of the intent and design of the original plan (especially if after a compaction). Things that should be discussed explicitly, not done implicitly. Outside of planning mode, LLMs aren’t seeking out the truth of the domain, they’re seeking out the path of least resistance.

Note that this is different than weakening types in existing functions. That’s a failure mode I rarely see in practice. Instead, when running into a wall with the type of existing code, there’s another failure mode that’s much more common…

Structural Type Abuse

Sometimes AI will optimize preserving existing types (especially across package boundaries) instead of changing them.

String Stuffing

I like to call this “string stuffing”. We like to make nice semantic types that match our domain and only allow the creation of meaningful values…but LLMs absolutely love to find ways to twist these to save time. Strings, in particular, are vulnerable because most Haskell types have Show instances.

Consider a type for structured errors:

data ErrorEvent = UnknownUser String
                | DatabaseErrorCode Int
                | InvalidJSON A.Value
                | NetworkError SomeException
                | Canceled (Maybe CancelationReason)
                | ...

And you have a function:

handleRequest :: Request -> IO (Either ErrorEvent Response)

And we have to add a new handler for a new request type. Maybe this new handler has a new type of error. Instead of adding a new structural error, LLMs will find great joy in cleverly abusing the structure to invalidate the domain.

handleAddGroup :: AddGroupRequest -> IO (Either ErrorEvent Response)
handleAddGroup req
    | validGroup group = -- ..
    | otherwise = pure $ Left (UnknownUser $ "Invalid group: " <> group)
  where
    group = getGroup req

“Invalid groups are not a valid ErrorEvent. The simplest solution is to put the error in UnknownUser, which can take a group name.”

And yes, this depravity knows no bounds. You would be surprised by the creative ways AI will discover to stuff your strings. These are all things I have personally witnessed in frontier models.

handleAddGroup :: AddGroupRequest -> IO (Either ErrorEvent Response)
handleAddGroup req
    -- ...
    | otherwise = pure $ Left (DatabaseErrorCode (-1))

handleAddGroup :: AddGroupRequest -> IO (Either ErrorEvent Response)
handleAddGroup req
    -- ...
    | otherwise = pure $ Left $ InvalidJSON $
        A.object ["errorType" .= "Invalid group", "group" .= group]
  where
    group = getGroup req

handleAddGroup :: AddGroupRequest -> IO (Either ErrorEvent Response)
handleAddGroup req
    -- ...
    | otherwise = pure $ Left $ NetworkError $
        toException (userError $ "Invalid group: " <> show group)
  where
    group = getGroup req

handleAddGroup :: AddGroupRequest -> IO (Either ErrorEvent Response)
handleAddGroup req
    -- ...
    | otherwise = pure $ Left (Canceled Nothing)

This type of failure mode is probably more egregious than the others in that it is very rare that this is ever the intended behavior. The entire reason we picked an ADT to describe our type is so that we can structurally match on them later, treat them semantically, etc., and string stuffing to abuse our structure has pretty much zero legitimate use-cases other than quickly hacking a printf debug session. However, it truly is often “the simplest solution”.

The main way I deal with this is to be very very careful of putting abusable fields like String, A.Value, Int, SomeException in my data types…just a single field or branch that has an abusable field, AI will find it, and you will feel very stupid for missing it. But hey, the whole point of using properly structured values was to avoid stuffing things into String too, right? The fix for this is a fix that helps human coders, too.

data ErrorEvent = UnknownUser UserName
                | DatabaseErrorCode ErrorCode
                | InvalidJSON ParseError
                | NetworkError NetworkException
                | Canceled CancelationReason
                | ...

Field Abuse

This isn’t just limited to sum types. AI will often stuff data into record value fields that are strings or lists.

data Report = Report
    { reportName :: String
    , reportAuthors :: [String]
    , reportDate :: Day
    , ...
    }

“I need to specify the affiliations of the authors in this report. The simplest solution is to add this to the list of reportAuthors after the authors.”

AI will also stuff sentinel values everywhere: instead of changing the type to take Maybe Day, it might add ModifiedJulianDay 0 for missing days.

There’s also the dual, where the AI will be happy to use existing record fields in overloaded ways instead of adding a new field.

data Targets = Targets
    { fooTarget :: String
    , barTarget :: String
    , -- ...
    }

Let’s say you need to add a new feature or code path that requires a new target for a baz service.

“I need to get a new target…instead of adding a new field to Targets, let’s re-use barTarget. That’s the cleanest approach.”

It will optimize keeping existing types instead of extending them to match your domain as your domain expands, especially if those existing types cross a library boundary.

I believe there are three heuristics at play that drive this behavior.

The heuristic to avoid extra risk in modifying upstream types across library boundaries with heavy dependencies. This might be very risky behavior in an untyped language like Python, where each type change might introduce new regressions that are not immediately obvious. So, avoiding upstream type changes avoids potential regression.
The heuristic to avoid extra work in modifying upstream types across library boundaries and compilation units. In Haskell, however, upstream type changes force you to address each possible regression point downstream. So changing an upstream type will require you to address every place it is used, which can be time-consuming and avoided by LLMs, especially if compilation is expensive, or multiple new typeclass instances might need to be added.

I have literally seen LLMs say “Adding this field would require adding typeclass instances on several other types, which would be a huge change. The simplest approach would be…”

However, updates require work by design: API changes should require lots of thought, and the compiler enforcing that is the whole point.

The big irony here is that these updates and changes are largely mechanical in nature, and are exactly the boilerplatey task that LLMs are optimally good for. These are the reasonable one-shots. So it’s kind of funny when you let an agentic coder take on a “self-directed” mode, it refuses to use “itself” in the way that a real human would for these smaller tasks.
The heuristic to avoid extra risk in touching data types that might already be used in prod code or databases. Config files that might have to be updated to new schemas, inter-op with existing services that might not be easily deployed in sync, working with data at rest…all of these are real risks you have to manage when changing data types. In practice, a lot of our type changes will not be relevant to any of these concerns, but it is understandable that the LLM would develop an instinct to blanket-avoid them.

These are also the types of failure modes that are most difficult to catch during code review. Diff views will analyze that code has changed, so code that didn’t change is especially difficult for human monkey brains to spot, with no green or red bright highlighting. You must be especially vigilant to catch code that did not change but should have.

Resisting New Types

Sometimes AI does modify existing sum types, but doesn’t quite adapt existing code correctly.

For example, if your domain has a specific meaningful universe:

data State = Alaska | Arkansas | Arizona | ...

processState :: State -> IO ()

We might want to start supporting countries alongside US states. An LLM might recognize that the domain needs to be expanded, but it might expand it flatly:

data Region = Canada | Mexico | Alaska | Arkansas | Arizona

processRegion :: Region -> IO ()
processRegion = \case
    Canada -> ...
    Mexico -> ...
    st -> processState st

processState :: Region -> IO ()
processState = \case
    Canada -> pure ()
    Mexico -> pure ()
    Alaska -> ... -- actual logic

The real solution would be to have all your pattern matches strictly reduce the space of what they cover (and be monotonically decreasing), and to be suspicious of “ignored case matches” that have dummy values like pure ():

data Region = Canada | Mexico | USState State
data State = Alaska | Arkansas | Arizona | ...

processRegion :: Region -> IO ()
processRegion = \case
    Canada -> ...
    Mexico -> ...
    USState st -> processState st

processState :: State -> IO ()
processState = \case
    Alaska -> ... -- actual logic

All things that are code smells in normal human code (not necessarily wrong, but invite further scrutiny), but are maybe amplified in the age of LLMs because of a mis-tuned heuristic on not defining new types and instead trying to re-use or abuse existing types.

So, if there is some pressure against modifying types, there might be an even greater pressure against adding types.

Meditations

None of these behaviors are blanket-wrong, but they usually signal that the LLM is under stress or duress and attempting to find ways to take the easy or “low-effort” path over the correct one. All of them are worth human intervention and guidance as soon as possible, at least until the day where P(legitimate | attempted) approaches 1.

Will there be a day when LLMs can generate the correct types to match the domain, and resist their tendency to “defensive-program” their way into correctness? Maybe. But I have rarely ever had Opus 4.8 crank out a sufficient domain model for any non-trivial product. And, when I do reach a plan I find sufficient, a few compactions later and all of the original motivations seem to get washed out.

There might be a way to uber-prompt all of these issues away, but I feel that effectively using LLMs isn’t necessarily something you can address from the prompt level: it’s something that demands constant vigilance and care. I’ve found automated hooks (like forbidding warning-disabling, detecting hlint bypassing…ask claude for help writing these lol) also help me flag areas that need attention immediately.

Who knows, maybe all of these things will be solved within a year. But I still think of software development as something that’s worth scrutinizing for anything of importance. As failure modes like these become less common…the long tail of correctness, I predict, will remain long.

Anyway, that’s it for this topic, but if I find the time I’ll continue on with some other topics I’ve been thinking about during my Haskell and LLM adventures:

Effective ways to plan out Haskell code and approaches, ways to encourage the best possible types
Structuring your libraries mechanically for the best build-and-test rapid development cycle
Starting and maintaining full “vibe-coded” Haskell projects (when correctness is not critical) and the advantages over untyped vibes.

Let me know if there are any you’d like to see first, or if there are other aspects of Haskell LLM usage you might like me to address!

And hey, since we’re here, why not train your agentic friend to take these ideas to heart?

<https://blog.jle.im/entry/llms-and-haskell-1-constraint-evading-behavior.html>

Read this post and make me a Claude Code skill that reviews a Haskell diff for
the constraint-evading compromises it describes: suppressed warnings, string
and field stuffing, and weakened types that differ from any recorded plans.
Some of these hide in code that did not change but should have, so the skill
should start from the functions that changed and evaluate how they use or abuse
the types involved, but also spot type changes that look suspicious.

Extreme Haskell: Typed Expression EDSLs (Part 1)

Justin Le — Tue, 7 Jul 2026 17:11:34 UTC

I always say, inside every Haskeller there are two wolves, living on opposite ends of the Haskell Fancy Code Spectrum. Are you going to write “simple Haskell”, using basic GHC 2010 tools and writing universal Haskell that every introductory course offers, trying to keep the code as immediately understandable and accessible? Or are you going to pile in all of the Haskell type system and evaluation tricks you can find and turn on all the extensions, and go full fancy?

In my Seven Levels of Type Safety post, I described different extremes of type safety and fancy code. I talked about how writing effective code was finding the correct compromise for the level of communication and safety you need.

But this is not that kind of blog post. This is the kind of blog post where we celebrate terrifying type-safety, facetious fanciness, and masochistic meta-analysis. This series is about what happens when we dare to go full fancy. Let’s write code that is so inscrutable, so painful and torturous to write, yet so undeniably useful that you can’t help but try to throw it into every single thing you write and will feel a gnawing emptiness in your soul until you do.

As our example, let’s write a type-safe method to specify your program as a series of states, with triggered transitions between them: a type-safe state machine graph using a type-safe lambda calculus. We want to specify this in a way that we can write once and then:

be interpretable in a type-safe way within Haskell.
be inspectable with visualizable control flow.
be compilable to multiple actual back-ends, letting you run the same function under multiple implementations.

This exact thing is something I’ve needed and used multiple times now in projects. I want to specify one program graph within Haskell, but in a way that can compile both in C and javascript while also being visualizable and interactively explorable.

Once you go down this road, everything you ever write will feel woefully unsafe and limited. And everything you want to write will be hopelessly inscrutable by normal humans and borderline unusable. But such is the curse we all bear. Turn around now, you have been warned.

This post will build up the embedded typed expression language. Part 2 will use that expression language to define typed state machines with embedded predicates and visualize them, and Part 3 will compile those machines to different languages and verify they execute identically, with some live demos.

All of the code here is available online, and if you check out the repo and run nix develop you should be able to load it all in ghci:

$ cd code-samples/typed-sm-lc
$ nix develop
$ ghci
ghci> :load ExprStage1.hs

The Lambda Calculus

Let’s derive a way to express an algorithm or expression in Haskell that can be reified and analyzed within Haskell, and eventually be a form we can compile to different backends, interpret in Haskell, or generate Graphviz visualizations for.

A First Pass

One basic thing we can do is start with:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage1.hs#L18-L34

data Prim = PInt Int | PBool Bool | PString String
  deriving (Eq, Show)

data Op = OPlus | OTimes | OLte | OAnd
  deriving (Eq, Show)

data Expr
  = EPrim Prim
  | EVar String
  | ELambda String Expr
  | EApply Expr Expr
  | EOp Op Expr Expr
  | ERecord (Map String Expr)
  | EAccess Expr String
  | EChoice String Expr
  | ECase Expr (Map String (String, Expr))
  deriving (Eq, Show)

And you can write (\x -> x * 3) 5 as:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage1.hs#L36-L37

fifteen :: Expr
fifteen = ELambda "x" (EOp OTimes (EVar "x") (EPrim (PInt 3))) `EApply` EPrim (PInt 5)

The strings in ELambda introduce variables, and EVar refers to the bound variable. As you can see, this is…pretty untyped. We could easily write something that is meaningless:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage1.hs#L67-L69

badTypeExample :: Expr
badTypeExample =
  EOp OAnd (EPrim (PInt 1)) (EPrim (PInt 2))

Of course, GHC can typecheck our code if we literally write \x -> x + 3 and reject 1 && 2. But we aren’t trying to build opaque Haskell code here, we’re trying to represent our expression as an ADT that we can analyze within the language.

If we want a record projection and one labeled choice with a case analysis over it:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage1.hs#L39-L62

recordExample :: Expr
recordExample =
  EOp
    OPlus
    ( EAccess
        ( ERecord $
            M.fromList
              [ ("value", EPrim (PInt 7)),
                ("label", EPrim (PString "found"))
              ]
        )
        "value"
    )
    (EPrim (PInt 1))

sumExample :: Expr
sumExample =
  ECase
    (EChoice "Found" (EPrim (PInt 7)))
    ( M.fromList
        [ ("Found", ("value", EOp OPlus (EVar "value") (EPrim (PInt 1)))),
          ("Missing", ("message", EPrim (PInt 0)))
        ]
    )

Now, for the entire point of Expr, we can write a function to pretty-print it, using the prettyprinter library:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage1.hs#L253-L299

ppPrim :: Prim -> PP.Doc ann
ppPrim = \case
  PInt n -> PP.pretty n
  PBool True -> "true"
  PBool False -> "false"
  PString s -> PP.pretty (show s)

ppOp :: Op -> PP.Doc ann
ppOp = \case
  OPlus -> "+"
  OTimes -> "*"
  OLte -> "<="
  OAnd -> "&&"

ppExpr :: Bool -> Expr -> PP.Doc ann
ppExpr paren = \case
  EPrim p -> ppPrim p
  EVar v -> PP.pretty v
  ELambda n body ->
    wrap $ "\\" <> PP.pretty n <+> "->" <+> ppExpr False body
  EApply f x ->
    wrap $ ppExpr True f <+> ppExpr True x
  EOp o x y ->
    wrap $ ppExpr True x <+> ppOp o <+> ppExpr True y
  ERecord xs ->
    PP.encloseSep "{ " " }" ", " $
      [PP.pretty k <+> "=" <+> ppExpr False v | (k, v) <- M.toList xs]
  EAccess e k ->
    ppExpr True e <> "." <> PP.pretty k
  EChoice tag x ->
    wrap $ PP.pretty tag <+> ppExpr True x
  ECase x hs ->
    wrap $
      PP.sep
        [ "case" <+> ppExpr False x <+> "of"
        , PP.encloseSep "{ " " }" "; " $
            [ PP.pretty tag <+> PP.pretty n <+> "->" <+> ppExpr False body
            | (tag, (n, body)) <- M.toList hs
            ]
        ]
  where
    wrap
      | paren = PP.parens
      | otherwise = id

prettyExpr :: Expr -> PP.Doc ann
prettyExpr = ppExpr False

ghci> prettyExpr fifteen
(\x -> x * 3) 5
ghci> prettyExpr badTypeExample
1 && 2
ghci> prettyExpr recordExample
{ label = "found", value = 7 }.value + 1
ghci> prettyExpr sumExample
case Found 7 of { Found value -> value + 1; Missing message -> 0 }

Now, we can write a quick typechecker for this using a greedy type-checking algorithm (written out here), which is a fun exercise, but it’s beyond the point of this post. For our purposes, we’re going to write the in-Haskell evaluator, which is one sure-fire evidential/constructive way to prove an expression was valid after-the-fact.

So…how can you “evaluate” this to 15, within Haskell? What would the type even be? The best we can do at this point is make the entire thing monadic by returning Maybe or Either, and split out the expressions we write from the values we can actually evaluate to:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage1.hs#L228-L330

data EValue
  = EVInt Int
  | EVBool Bool
  | EVString String
  | EVFun (EValue -> Maybe EValue)
  | EVRecord (Map String EValue)
  | EVChoice String EValue

eval :: Map String EValue -> Expr -> Maybe EValue
eval env = \case
  EPrim p -> evalPrim p
  EVar v -> M.lookup v env
  ELambda n body -> pure (EVFun (\x -> eval (M.insert n x env) body))
  EApply f x -> eval env f >>= \case
    EVFun f' -> eval env x >>= f'
    _ -> Nothing
  EOp o x y -> do
    u <- eval env x
    v <- eval env y
    case (u, v) of
      (EVInt a, EVInt b) -> case o of
        OPlus -> pure (EVInt (a + b))
        OTimes -> pure (EVInt (a * b))
        OLte -> pure (EVBool (a <= b))
        OAnd -> Nothing
      (EVBool a, EVBool b) -> case o of
        OAnd -> pure (EVBool (a && b))
        _ -> Nothing
      _ -> Nothing
  ERecord xs -> EVRecord <$> traverse (eval env) xs
  EAccess e k -> do
    EVRecord xs <- eval env e
    M.lookup k xs
  EChoice tag x -> EVChoice tag <$> eval env x
  ECase x hs -> do
    EVChoice tag payload <- eval env x
    (n, body) <- M.lookup tag hs
    eval (M.insert n payload env) body

This would properly evaluate:

ghci> eval M.empty fifteen
Just (EVInt 15)

We can also produce closures as values:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage1.hs#L64-L65

plusThree :: Expr
plusThree = ELambda "x" (EOp OPlus (EVar "x") (EPrim (PInt 3)))

ghci> for_ (eval M.empty plusThree) \case
    EVFun f -> print (f (EVInt 4))
    _ -> putStrLn "not a function"
Just (EVInt 7)

This kind of works if you remember to thread everything through Maybe (or Either) or what have you. But this is not ideal. You should be able to know, at compile-time, that your Expr is valid. After all, you want to be able to create one “valid” Expr, and run it at every context. It’s useless to you if every single time you used an Expr, you had to manually handle the Nothing case. Your diagram generator, your Haskell runner, your code generator, will always be in Either even though you know your Expr is valid, via tests or something. We want GHC to reject badly typed expressions, so we never need to unwrap or handle a Nothing or Left!

No, no, this is not okay and not acceptable. We should be able to verify in the types if an Expr is valid.

Type-Indexed Expressions

Just Add the Index

The next step you’ll see in posts online is to add a phantom index type to Expr:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L19-L49

type data Ty
  = TInt
  | TBool
  | TString
  | Ty :-> Ty

data Prim :: Ty -> Type where
  PInt :: Int -> Prim TInt
  PBool :: Bool -> Prim TBool
  PString :: String -> Prim TString

data Op :: Ty -> Ty -> Ty -> Type where
  OPlus :: Op TInt TInt TInt
  OTimes :: Op TInt TInt TInt
  OLte :: Op TInt TInt TBool
  OAnd :: Op TBool TBool TBool

data Expr :: Ty -> Type where
  EPrim :: Prim t -> Expr t
  EVar :: STy t -> String -> Expr t
  ELambda :: STy a -> String -> Expr b -> Expr (a :-> b)
  EApply :: Expr (a :-> b) -> Expr a -> Expr b
  EOp :: Op a b c -> Expr a -> Expr b -> Expr c

(We’ll explain each part of this declaration eventually)

A phantom type is a type parameter that doesn’t represent any actual value “contained” inside the data type, but just serves to “tag” or distinguish values for the compiler to reject or unify things in useful ways.

This introduces several new language features, so bear with me as I break them down.

First, we use -XTypeData to define a data kind: Ty is a kind with types TInt :: Ty, TBool :: Ty, etc. And in Expr t, we have an expression tagged with t, which describes the result type. (In fact, all data types are automatically promoted to the type level with -XDataKinds. You might see the 'Nothing quote prefix syntax in cases where it’s ambiguous if you’re talking about the data constructor or the type constructor, like '[] and '(,))

For example, because we have EPrim :: Prim t -> Expr t, and PInt 3 :: Prim TInt, we have EPrim (PInt 3) :: Expr TInt: a primitive 3 is an expression describing an integer.

And because EOp :: Op a b c -> Expr a -> Expr b -> Expr c, and OLte :: Op TInt TInt TBool, we have

EOp OLte :: Expr TInt -> Expr TInt -> Expr TBool

So we can write an operation on two Exprs that typecheck how we’d expect:

ghci> :t EOp OLte (EPrim (PInt 3)) (EPrim (PInt 4))
Expr TBool

We also have EOp OAnd :: Expr TBool -> Expr TBool -> Expr TBool, which means the compiler will reject our previous 1 && 2 example:

ghci> :t EOp OAnd (EPrim (PInt 1)) (EPrim (PInt 2))
<interactive> error:
    • Couldn't match type ‘TInt’ with ‘TBool’
      Expected: Prim TBool
        Actual: Prim TInt

We can write lambdas in this system too:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L51-L55

fifteen :: Expr TInt
fifteen =
  EApply
    (ELambda STInt "x" (EOp OTimes (EVar STInt "x") (EPrim (PInt 3))))
    (EPrim (PInt 5))

Because of Ty, we can also make a new indexed data type with phantoms of “fully resolved” values:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L115-L119

data EValue :: Ty -> Type where
  EVInt :: Int -> EValue TInt
  EVBool :: Bool -> EValue TBool
  EVString :: String -> EValue TString
  EVFun :: (EValue a -> Maybe (EValue b)) -> EValue (a :-> b)

This is what we want to eventually eval into, as we can guarantee ourselves to get a value of the correct type based on the Ty:

eValueToInt :: EValue TInt -> Int
eValueToInt = \case
    EVInt x -> x

And GHC will verify this as a total pattern match because EVInt is the only possible way to create an EValue TInt.

Singletons and Existentials

We’ll keep our bound variables stored as an ambient map of variable names to their evaluated values for now. But, to do this, we need to turn the heterogeneous EValue t into the homogeneous Map String SomeValue by wrapping the type variable as an existential type.

You might notice we have a singleton for our Ty type, STy, that pops up in multiple situations.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L27-L31

data STy :: Ty -> Type where
  STInt :: STy TInt
  STBool :: STy TBool
  STString :: STy TString
  STFun :: STy a -> STy b -> STy (a :-> b)

Firstly, it might help to recognize the general pattern where STy (the singleton) appears. It usually pops up whenever we have existentially scoped variables, like in data SomeValue = forall t. SomeValue (STy t) (EValue t). In this case, the t is completely lost to the outside world, and STy t is used to allow us to recover a runtime witness to what t was, after pattern matching on STy. This is the dependent sum pattern, and is similar to how Typeable is used in Data.Dynamic.

In our case, because variables are still stored ambiently in the environment and validated at runtime, we do need singletons to implement eval . The type Expr t only specifies the type of the result, but the type information of the ambient variables is not available. So, you can write EVar STInt "myVar" :: Expr TInt, but:

myVar might not be a variable in scope at all, so eval will fail at runtime
myVar might be in scope, but might be a TString and not a TInt

The first case is easy enough to deal with (M.lookup returns Nothing), but the second one is a little more subtle. Let’s say we do have a SomeValue under our key myVar…how do we make sure it has the correct type?

Runtime Type Equality

We can do ad-hoc pattern matching on EValue, but that won’t get us too far. Mostly because some of the EValue constructors actually don’t have enough information for us to validate their actual type (try it! EVFun will give you a lot of trouble). So, what we can do is write a function that takes two STy at runtime and unifies them conditionally if they are the same. We’ll write a function sameTy :: STy a -> STy b -> Maybe (a :~: b), where

data (:~:) :: k -> k -> Type where
    Refl :: a :~: a

pattern matching on a value of type a :~: b will reveal that a and b are the same type variable, because the only way to construct it is with Refl :: a :~: a.

With that, we can write sameTy:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L133-L143

sameTy :: STy a -> STy b -> Maybe (a :~: b)
sameTy = \case
  STInt -> \case STInt -> Just Refl; _ -> Nothing
  STBool -> \case STBool -> Just Refl; _ -> Nothing
  STString -> \case STString -> Just Refl; _ -> Nothing
  STFun a b -> \case
    STFun c d -> do
      Refl <- sameTy a c
      Refl <- sameTy b d
      Just Refl
    _ -> Nothing

There’s a typeclass in base (or rather, a “kindclass”), TestEquality, that encapsulates this pattern:

class TestEquality f where
    testEquality :: f a -> f b -> Maybe (a :~: b)

In fact, we can write our sameTy as an instance:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L130-L131

instance TestEquality STy where
  testEquality = sameTy

We’re now at a higher fanciness level than before. But you might see the problem here: EVar STInt "x". x might not be defined, and it also might not have the correct type. Soooo yes, we still have issues here.

But now at least we can write eval:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L145-L176

eval :: Map String SomeValue -> Expr t -> Maybe (EValue t)
eval env = \case
  EPrim (PInt n) -> pure (EVInt n)
  EPrim (PBool b) -> pure (EVBool b)
  EPrim (PString s) -> pure (EVString s)
  EVar t v -> do
    SomeValue t' v' <- M.lookup v env
    Refl <- sameTy t t'
    pure v'
  ELambda ta n body ->
    pure $ EVFun $ \x -> eval (M.insert n (SomeValue ta x) env) body
  EApply f x -> do
    EVFun g <- eval env f
    x' <- eval env x
    g x'
  EOp o x y -> case o of
    OPlus -> do
      EVInt a <- eval env x
      EVInt b <- eval env y
      pure (EVInt (a + b))
    OTimes -> do
      EVInt a <- eval env x
      EVInt b <- eval env y
      pure (EVInt (a * b))
    OLte -> do
      EVInt a <- eval env x
      EVInt b <- eval env y
      pure (EVBool (a <= b))
    OAnd -> do
      EVBool a <- eval env x
      EVBool b <- eval env y
      pure (EVBool (a && b))

This does seem to work:

ghci> for_ (eval M.empty fifteen) \case
    EVInt x -> print x
15

Our system also allows us to produce closures and functions as values:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L63-L64

plusThree :: Expr (TInt :-> TInt)
plusThree = ELambda STInt "x" (EOp OPlus (EVar STInt "x") (EPrim (PInt 3)))

ghci> for_ (eval M.empty plusThree) \case
    EVFun f -> for_ (f (EVInt 4)) \case
      EVInt x -> print x    -- compiler-verified to always be EVInt
7

We have a type-safe eval now that will create a value of the type we want. But we still have the same errors when looking at variables: variables can still not be defined, or be defined as the wrong type.

Pretty-Printing

One nice consequence of this type-index method is that if you choose to consume them into an untyped target, you can do it more or less in the same way as the non-indexed untyped data.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L87-L113

ppPrim :: Prim t -> PP.Doc ann
ppPrim = \case
  PInt n -> PP.pretty n
  PBool b -> if b then "true" else "false"
  PString s -> PP.pretty (show s)

ppOp :: Op a b c -> PP.Doc ann
ppOp = \case
  OPlus -> "+"
  OTimes -> "*"
  OLte -> "<="
  OAnd -> "&&"

ppExpr :: Bool -> Expr t -> PP.Doc ann
ppExpr paren = \case
  EPrim p -> ppPrim p
  EVar _ v -> PP.pretty v
  ELambda _ n body -> wrap $ "\\" <> PP.pretty n <+> "->" <+> ppExpr False body
  EApply f x -> wrap $ ppExpr True f <+> ppExpr True x
  EOp o x y -> wrap $ ppExpr True x <+> ppOp o <+> ppExpr True y
  where
    wrap
      | paren = PP.parens
      | otherwise = id

prettyExpr :: Expr t -> PP.Doc ann
prettyExpr = ppExpr False

And they render the same way:

ghci> prettyExpr fifteen
(\x -> x * 3) 5
ghci> prettyExpr plusThree
\x -> x + 3
ghci> prettyExpr badVariable
(\x -> x + 3) true

Still Not Fully Verified

Implicit in the previous section was the admission of failure: this system lets us use indexed types to help propagate unification (the result types of OLte, OAnd, OPlus, etc.), but it can’t prevent all ill-defined programs from compiling.

The issue is EVar: its type EVar :: STy t -> String -> Expr t lets us bind any variable name as any type, and it’ll still typecheck. Even with the help of everything we have, we can just straight-up declare a reference to an unbound variable

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L71-L72

unboundVariable :: Expr TInt
unboundVariable = EVar STInt "missing"

This typechecks in GHC even though it’s meaningless in the domain. We can also reference the variable under any type:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage2.hs#L57-L61

badVariable :: Expr TInt
badVariable =
  EApply
    (ELambda STBool "x" (EOp OPlus (EVar STInt "x") (EPrim (PInt 3))))
    (EPrim (PBool True))

That’s because EVar can freely take any STy without any restriction, and no association with the binder name, so there’s no way for GHC to stop us.

So, again, we cannot create a fully type-checked Expr. We still have to deal with most of the same errors. This is noble, but clearly not good enough. We have to go deeper.

Typed Records and Sums

A quick detour: you might have noticed that this past implementation dropped records and sums. Before we move on, let’s go ahead and add those. Introducing records and sums at the same time as type-indexed Expr is a bit too much of a jump to fit into a single section.

Let’s add sums and records, which can use pretty similar mechanisms (via duality) for implementation.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L31-L79

type data Ty
  = TInt
  | TBool
  | TString
  | TRecord [(Symbol, Ty)]
  | TSum [(Symbol, Ty)]
  | Ty :-> Ty

data STy :: Ty -> Type where
  STInt :: STy TInt
  STBool :: STy TBool
  STString :: STy TString
  STRecord :: Rec STyField as -> STy (TRecord as)
  STSum :: Rec STyField as -> STy (TSum as)
  STFun :: STy a -> STy b -> STy (a :-> b)

Ty now includes TRecord [(Symbol, Ty)] and TSum [(Symbol, Ty)], which represent the field names and constructor payloads (Symbol being a type-level string). So, for example, TRecord ["value" ::: TInt, "label" ::: TString] would be the type of a record with ordered fields value and label of integers and strings, respectively. TSum ["Found" ::: TInt, "Missing" ::: TString] would be the type of a sum between Found containing an integer and Missing containing a string. Note we take a page out of vinyl by defining the type alias (:::) = '(,) to make things syntactically nicer.

Record Access

We need the fields and types at the type level because we have to answer what the Expr phantom type of field access is. If we had an x :: Expr (TRecord ["value" ::: TInt, "label" ::: TString]), we want the type of x.value to be Expr TInt.

To do this, we need to have a value in our Expr for field access that can “point” at a specific field in the type. One way to do that is to take a field of type Index:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L47-L49

data Index :: [k] -> k -> Type where
  IZ :: Index (x : xs) x
  IS :: Index xs x -> Index (y : xs) x

You can read this as: “IZ is an index to the head of the type-level list, and IS n is an index to the n-th item of the tail”. So, IS IZ is an index into the second element, IS (IS IZ) is an index into the third, etc.

If we have ["value" ::: TInt, "label" ::: TString], then we have values:

IZ    :: Index ["value" ::: TInt, "label" ::: TString] ("value" ::: TInt)
IS IZ :: Index ["value" ::: TInt, "label" ::: TString] ("label" ::: TString)

Note that the way this is constructed, it’s impossible for IS (IS IZ) :: Index ["value" ::: TInt, "label" ::: TString] _ to typecheck as anything!

In this way, we have a well-typed field accessor syntax, which takes an Expr of a record of fields and indexes it to get an Expr of the type at that index:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L105-L105

  EAccess :: KnownSymbol l => Expr (TRecord as) -> Index as (l ::: a) -> Expr a

Which is typed as:

(`EAccess` IZ)    :: Expr (TRecord ["value" ::: TInt, "label" ::: TString]) -> Expr TInt
(`EAccess` IS IZ) :: Expr (TRecord ["value" ::: TInt, "label" ::: TString]) -> Expr TString

To create an Expr of a record, we can use Rec from vinyl or NP from sop-core: a heterogeneous list indexed by a type-level list.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L43-L45

data Rec :: (k -> Type) -> [k] -> Type where
  RNil :: Rec f '[]
  (:&) :: f x -> Rec f xs -> Rec f (x : xs)

If you haven’t seen Rec before, basically Rec f [a,b,c] is a tuple of f a, f b, and f c. For example:

ghci> :t Identity 3 :& Identity True :& Identity "hello" :& RNil
Rec Identity [Int, Bool, String]
ghci> :t Const "x" :& Const "y" :& RNil
Rec (Const String) [x1, x2]

Keeping Rec f as instead of a direct heterogeneous list of as lets us store more interesting things than just Type-kinded things. For example, since our lists here are lists of (Symbol, Ty), we can create a container to hold fields:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L109-L110

data ExprField :: (Symbol, Ty) -> Type where
  EField :: KnownSymbol l => Expr a -> ExprField (l ::: a)

The field constructor keeps a KnownSymbol l constraint, so the type-level label is still available later when we need to render it:

ghci> :t EField @"value" (EPrim (PInt 7))
            :& EField @"label" (EPrim (PString "found"))
            :& RNil
Rec ExprField ["value" ::: TInt, "label" ::: TString]

So, we can create Expr (TRecord ["value" ::: TInt, "label" ::: TString]) by taking a Rec:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L104-L104

  ERecord :: Rec ExprField as -> Expr (TRecord as)

We can make this a little more ergonomic by using -XRequiredTypeArguments (as of GHC 9.10) to get rid of the -XTypeApplication ugliness:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L115-L150

eField :: forall l -> KnownSymbol l => Expr a -> ExprField (l ::: a)
eField l = EField @l

makeRecordExample :: Expr (TRecord ["value" ::: TInt, "label" ::: TString])
makeRecordExample =
  ERecord
    ( eField "value" (EPrim (PInt 7))
        :& eField "label" (EPrim (PString "found"))
        :& RNil
    )

recordExample :: Expr TInt
recordExample = EOp OPlus (EAccess @"value" makeRecordExample IZ) (EPrim (PInt 1))

Sum Injection and Case Analysis

We also need a type-level list witness for sum types, because we need to be able to implement the correct continuations for pattern matches: How do we know what thing to handle in each pattern match, unless the sum type has that information in its type?

Luckily due to the magic of duality, we can use the same tools, for the most part! We can inject into a sum with an Index, let’s say for a Expr (TSum ["Found" ::: TInt, "Missing" ::: TString]): sum type with Found containing an integer and Missing containing a string:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L106-L106

  EChoice :: KnownSymbol l => Index as (l ::: a) -> Expr a -> Expr (TSum as)

EChoice @"Found" IZ        :: Expr TInt -> Expr (TSum ["Found" ::: TInt, "Missing" ::: TString])
EChoice @"Missing" (IS IZ) :: Expr TString -> Expr (TSum ["Found" ::: TInt, "Missing" ::: TString])

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L181-L182

makeSumExample :: Expr (TSum ["Found" ::: TInt, "Missing" ::: TString])
makeSumExample = EChoice @"Found" IZ (EPrim (PInt 7))

And we can re-use Rec to define a type that can handle a ["Found" ::: TInt, "Missing" ::: TString] sum:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L112-L133

data ExprHandler :: Ty -> (Symbol, Ty) -> Type where
  EHandler :: KnownSymbol l => STy a -> String -> Expr b -> ExprHandler b (l ::: a)

eHandler :: forall l -> KnownSymbol l => STy a -> String -> Expr b -> ExprHandler b (l ::: a)
eHandler l = EHandler @l

ghci> :t eHandler "Found" STInt "value" (EOp OPlus (EVar STInt "value") (EPrim (PInt 1)))
ExprHandler TInt ("Found" ::: TInt)
         -- ^ result           ^ payload

And we can put these into a Rec to handle each option in the list:

ghci> :t eHandler "Found" STInt "value" (EOp OPlus (EVar STInt "value") (EPrim (PInt 1)))
           :& eHandler "Missing" STString "message" (EPrim (PInt 0))
           :& RNil
Rec (ExprHandler TInt) ["Found" ::: TInt, "Missing" ::: TString]

And that’s exactly what a case statement is:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L107-L107

  ECase :: Expr (TSum as) -> Rec (ExprHandler b) as -> Expr b

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L184-L191

sumExample :: Expr TInt
sumExample =
  ECase
    makeSumExample
    ( eHandler "Found" STInt "value" (EOp OPlus (EVar STInt "value") (EPrim (PInt 1)))
        :& eHandler "Missing" STString "message" (EPrim (PInt 0))
        :& RNil
    )

Note that we’re still using string binders, so there’s still an element of unsafety here… we say that the variable name is "value" and that it is a TInt, but when we later refer to the variable with EVar STInt "value", it isn’t type-checked that later references use the same type. The compiler would be just as happy with EVar STString "value".

Here’s an example demonstrating both failure modes: the first handler references a variable that doesn’t exist, and the second handler references a variable that does exist as an incorrect type! How unfortunate.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L202-L209

badCaseBranchExample :: Expr TInt
badCaseBranchExample =
  ECase
    (EChoice @"Found" IZ (EPrim (PInt 7)))
    ( eHandler "Found" STInt "value" (EOp OPlus (EVar STInt "missing") (EPrim (PInt 1)))
        :& eHandler "Missing" STString "message" (EOp OPlus (EVar STInt "message") (EPrim (PInt 1)))
        :& RNil
    )

Runtime Equality for Records and Sums

One complication is that we need to update the TestEquality instance for STy. The record and sum labels are type-level Symbols, so we compare those with the sameSymbol (kind of like testEquality for any KnownSymbol instance) and then compare the payload types recursively.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L284-L324

instance TestEquality STy where
    testEquality = sameTy

instance TestEquality STyField where
    testEquality = sameField

sameTy :: STy a -> STy b -> Maybe (a :~: b)
sameTy = \case
  STInt -> \case STInt -> Just Refl; _ -> Nothing
  STBool -> \case STBool -> Just Refl; _ -> Nothing
  STString -> \case STString -> Just Refl; _ -> Nothing
  STRecord as -> \case
    STRecord bs -> do
      Refl <- sameFields as bs
      Just Refl
    _ -> Nothing
  STSum as -> \case
    STSum bs -> do
      Refl <- sameFields as bs
      Just Refl
    _ -> Nothing
  STFun a b -> \case
    STFun c d -> do
      Refl <- sameTy a c
      Refl <- sameTy b d
      Just Refl
    _ -> Nothing

sameFields :: Rec STyField xs -> Rec STyField ys -> Maybe (xs :~: ys)
sameFields RNil RNil = Just Refl
sameFields (x :& xs) (y :& ys) = do
  Refl <- sameField x y
  Refl <- sameFields xs ys
  Just Refl
sameFields _ _ = Nothing

sameField :: STyField x -> STyField y -> Maybe (x :~: y)
sameField (STyField @l tx) (STyField @m ty) = do
    Refl <- sameSymbol (Proxy @l) (Proxy @m)
    Refl <- sameTy tx ty
    Just Refl

The Full Eval

Before we write the final eval, let’s practice using Index and Rec together. If we have an index Index as a that picks out a value a in as, then we can pick out the f a from a Rec f as:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L60-L63

indexRec :: Index xs x -> Rec f xs -> f x
indexRec = \case
  IZ -> \(x :& _) -> x
  IS i -> \(_ :& xs) -> indexRec i xs

We also can recursively iterate a function over each item, assuming the function forall x. f x -> g x: that is, we can turn a Rec f as into a Rec g as assuming our function is polymorphic over each x, and only depends on the shape of f.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L65-L67

traverseRec :: Applicative m => (forall x. f x -> m (g x)) -> Rec f xs -> m (Rec g xs)
traverseRec _ RNil = pure RNil
traverseRec f (x :& xs) = (:&) <$> f x <*> traverseRec f xs

With that, we can write our full eval.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L326-L369

eval :: Map String SomeValue -> Expr t -> Maybe (EValue t)
eval env = \case
  EPrim (PInt n) -> pure (EVInt n)
  EPrim (PBool b) -> pure (EVBool b)
  EPrim (PString s) -> pure (EVString s)
  EVar t v -> do
    SomeValue t' v' <- M.lookup v env
    Refl <- sameTy t t'
    pure v'
  ELambda ta n body ->
    pure $ EVFun $ \x -> eval (M.insert n (SomeValue ta x) env) body
  EApply f x -> do
    EVFun g <- eval env f
    x' <- eval env x
    g x'
  EOp o x y -> case o of
    OPlus -> do
      EVInt a <- eval env x
      EVInt b <- eval env y
      pure (EVInt (a + b))
    OTimes -> do
      EVInt a <- eval env x
      EVInt b <- eval env y
      pure (EVInt (a * b))
    OLte -> do
      EVInt a <- eval env x
      EVInt b <- eval env y
      pure (EVBool (a <= b))
    OAnd -> do
      EVBool a <- eval env x
      EVBool b <- eval env y
      pure (EVBool (a && b))
  ERecord xs ->
    EVRecord <$> traverseRec (evalField env) xs
  EAccess e i -> do
    EVRecord xs <- eval env e
    case indexRec i xs of
      EVField v -> pure v
  EChoice i x ->
    EVSum i <$> eval env x
  ECase x hs -> do
    EVSum i v <- eval env x
    case indexRec i hs of
      EHandler t n body -> eval (M.insert n (SomeValue t v) env) body

Ergonomics of Records and Sums

Note that we could also choose to implement records and sums using row types indexed by the name of the field itself, instead of an ordered list of tuples. This would have the advantage of making, for example, { value :: Int, label :: String } the same type as { label :: String, value :: Int }. However, I personally prefer the style of building things inductively (:&/RNil and IS/IZ), it makes the type errors and constructions a lot easier to work with and reason with.

However, we can get a little bit of the best of both worlds by using typeclasses to auto-insert the Index witnesses into a list.

First, we can write a typeclass that searches a type-level list of fields and produces the right Index:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L51-L58

class ListIx (l :: Symbol) (xs :: [(Symbol, Ty)]) (a :: Ty) | l xs -> a where
  listIx :: Index xs (l ::: a)

instance ListIx l (l ::: a : xs) a where
  listIx = IZ

instance {-# OVERLAPPABLE #-} ListIx l xs a => ListIx l (m ::: b : xs) a where
  listIx = IS (listIx @l)

The FunDep l xs -> a lets us use this like a function: for a label l and a list xs, we should be able to uniquely determine the a type it singles out, if it exists. So we have an instance of ListIx "value" ["value" ::: TInt, "label" ::: TString] TInt, where the label "value" and the list uniquely determines the result type TInt.

We can now have a helper function that we can call like eAccess "value" using GHC 9.10’s RequiredTypeArguments:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L118-L123

eAccess ::
  forall (l :: Symbol) ->
  (KnownSymbol l, ListIx l as a) =>
  Expr (TRecord as) ->
  Expr a
eAccess l e = EAccess @l e (listIx @l)

That lets us write the field name directly, and the compiler will generate the Index automatically for us:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L167-L176

namedAccessExample :: Expr TString
namedAccessExample =
  eAccess
    "label"
    ( ERecord
        ( eField "value" (EPrim (PInt 7))
            :& eField "label" (EPrim (PString "found"))
            :& RNil
        )
    )

Here, eAccess "value" :: Expr (TRecord ["value" ::: TInt, "label" ::: TString]) -> Expr TInt, its result type uniquely determined by the types in the record fields.

The same trick works for sum injections, so we can write the constructor name directly:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L125-L179

eChoice ::
  forall (l :: Symbol) ->
  (KnownSymbol l, ListIx l as a) =>
  Expr a ->
  Expr (TSum as)
eChoice l e = EChoice @l (listIx @l) e

namedChoiceExample :: Expr (TSum ["Found" ::: TInt, "Missing" ::: TString])
namedChoiceExample = eChoice "Missing" (EPrim (PString "not here"))

Here, eChoice "Missing" :: Expr TString -> Expr (TSum ["Found" ::: TInt, "Missing" ::: TString]), because the constructor name "Missing" uniquely determines the payload type inside that sum.

Pretty-Printing Records and Sums

To pretty-print, we finally use that KnownSymbol constraint we’ve been tracking this entire time. We can use symbolVal :: KnownSymbol s => p s -> String to get the string value from the type-level string.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage3.hs#L237-L282

ppPrim :: Prim t -> PP.Doc ann
ppPrim = \case
  PInt n -> PP.pretty n
  PBool b -> if b then "true" else "false"
  PString s -> PP.pretty (show s)

ppOp :: Op a b c -> PP.Doc ann
ppOp = \case
  OPlus -> "+"
  OTimes -> "*"
  OLte -> "<="
  OAnd -> "&&"

ppFields :: Rec ExprField xs -> [PP.Doc ann]
ppFields RNil = []
ppFields (EField @l x :& xs) =
  (PP.pretty (symbolVal (Proxy @l)) <+> "=" <+> ppExpr False x) : ppFields xs

ppHandlers :: Rec (ExprHandler b) xs -> [PP.Doc ann]
ppHandlers RNil = []
ppHandlers (EHandler @l _ n body :& xs) =
  (PP.pretty (symbolVal (Proxy @l)) <+> PP.pretty n <+> "->" <+> ppExpr False body) : ppHandlers xs

ppExpr :: Bool -> Expr t -> PP.Doc ann
ppExpr paren = \case
  EPrim p -> ppPrim p
  EVar _ v -> PP.pretty v
  ELambda _ n body -> wrap $ "\\" <> PP.pretty n <+> "->" <+> ppExpr False body
  EApply f x -> wrap $ ppExpr True f <+> ppExpr True x
  EOp o x y -> wrap $ ppExpr True x <+> ppOp o <+> ppExpr True y
  ERecord xs -> PP.encloseSep "{ " " }" ", " (ppFields xs)
  EAccess @l e _ -> ppExpr True e <> "." <> PP.pretty (symbolVal (Proxy @l))
  EChoice @l _ x -> wrap $ PP.pretty (symbolVal (Proxy @l)) <+> ppExpr True x
  ECase x hs ->
    wrap $
      PP.sep
        [ "case" <+> ppExpr False x <+> "of"
        , PP.encloseSep "{ " " }" "; " (ppHandlers hs)
        ]
  where
    wrap
      | paren = PP.parens
      | otherwise = id

prettyExpr :: Expr t -> PP.Doc ann
prettyExpr = ppExpr False

Capturing Variables

In order to have EVar be type-safe, the environment itself needs to be a part of the Expr type, and you should only be able to use EVar if the Expr enforces it. ELambda would, therefore, introduce the new variable to the environment.

We’ll have:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L80-L80

data Expr :: [(Symbol, Ty)] -> Ty -> Type where

So a value of type Expr ["x" ::: TInt, "y" ::: TBool] t is an expression with free variables x of type Int and y of type Bool.

Surprise! That small detour to add records and sums to our language actually ended up being a smooth precursor to all of the techniques we will be using to solve for variable binders.

ELambda would therefore take an Expr with a free variable and turn it into an Expr of a function type. We also keep a KnownSymbol constraint for the name so that we can recover the name when we render the expression.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L83-L83

  ELambda :: KnownSymbol n => Expr (n ::: a ': vs) b -> Expr vs (a :-> b)

EVar then becomes exactly like EAccess! We “index” into the environment of the Expr vs a using Index:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L82-L82

  EVar :: Index vs (n ::: t) -> Expr vs t

So it is legal to have EVar IZ :: Expr ["x" ::: TInt, "y" ::: TBool] TInt, and also it is automatically inferred to be a TInt. But we could not write EVar IZ :: Expr [] TInt.

And finally, our whole Expr:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L80-L89

data Expr :: [(Symbol, Ty)] -> Ty -> Type where
  EPrim :: Prim t -> Expr vs t
  EVar :: Index vs (n ::: t) -> Expr vs t
  ELambda :: KnownSymbol n => Expr (n ::: a ': vs) b -> Expr vs (a :-> b)
  EApply :: Expr vs (a :-> b) -> Expr vs a -> Expr vs b
  EOp :: Op a b c -> Expr vs a -> Expr vs b -> Expr vs c
  ERecord :: Rec (ExprField vs) as -> Expr vs (TRecord as)
  EAccess :: KnownSymbol l => Expr vs (TRecord as) -> Index as (l ::: a) -> Expr vs a
  EChoice :: KnownSymbol l => Index as (l ::: a) -> Expr vs a -> Expr vs (TSum as)
  ECase :: Expr vs (TSum as) -> Rec (ExprHandler vs b) as -> Expr vs b

Just like with record access, we can use the ListIx class to write a named helper:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L47-L120

class ListIx (l :: Symbol) (xs :: [(Symbol, Ty)]) (a :: Ty) | l xs -> a where
  listIx :: Index xs (l ::: a)

instance ListIx l (l ::: a ': xs) a where
  listIx = IZ

instance {-# OVERLAPPABLE #-} ListIx l xs a => ListIx l (m ::: b ': xs) a where
  listIx = IS (listIx @l)

eVar :: forall n -> ListIx n vs a => Expr vs a
eVar n = EVar (listIx @n)

Adding in our other -XRequiredTypeArguments helpers:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L91-L117

eLambda :: forall n -> KnownSymbol n => Expr (n ::: a ': vs) b -> Expr vs (a :-> b)
eLambda n = ELambda @n

eField :: forall l -> KnownSymbol l => Expr vs a -> ExprField vs (l ::: a)
eField l = EField @l

eAccess ::
  forall l ->
  (KnownSymbol l, ListIx l as a) =>
  Expr vs (TRecord as) ->
  Expr vs a
eAccess l e = EAccess @l e (listIx @l)

eChoice ::
  forall l ->
  (KnownSymbol l, ListIx l as a) =>
  Expr vs a ->
  Expr vs (TSum as)
eChoice l e = EChoice @l (listIx @l) e

eHandler ::
  forall n ->
  forall l ->
  (KnownSymbol n, KnownSymbol l) =>
  Expr (n ::: a ': vs) b ->
  ExprHandler vs b (l ::: a)
eHandler n l = EHandler @n @l

And we get something that is truly type-safe: all expressions are well-typed, and all variables are ensured to be bound!

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L139-L171

fifteen :: Expr '[] TInt
fifteen =
  EApply
    (eLambda "x" (EOp OTimes (eVar "x") (EPrim (PInt 3))))
    (EPrim (PInt 5))

recordExample :: Expr '[] TInt
recordExample =
  EOp
    OPlus
    ( eAccess
        "value"
        ( ERecord
            ( eField "value" (EPrim (PInt 7))
                :& eField "label" (EPrim (PString "found"))
                :& RNil
            )
        )
    )
    (EPrim (PInt 1))

sumExample :: Expr '[] TInt
sumExample =
  ECase
    (eChoice "Found" (EPrim (PInt 7)))
    ( eHandler "value" "Found" (EOp OPlus (eVar "value") (EPrim (PInt 1)))
        :& eHandler "message" "Missing" (EPrim (PInt 0))
        :& RNil
    )

What we gained

Now all of the previous “bad” examples we gave are finally compiler-verified:

ghci> :t (EVar IZ :: Expr '[] TInt)
<interactive> error:
    • Couldn't match type: (n0 ::: TInt) : xs0
                     with: '[]
      Expected: Index '[] (n0 ::: TInt)
        Actual: Index ((n0 ::: TInt) : xs0) (n0 ::: TInt)

ghci> :t (EVar IZ :: Expr '["x" ::: TString] TInt)
<interactive> error:
    • Couldn't match type ‘TString’ with ‘TInt’
      Expected: Index '["x" ::: TString] ("x" ::: TInt)
        Actual: Index '["x" ::: TString] ("x" ::: TString)

ghci> :t ECase
      (EChoice @"Found" IZ (EPrim (PInt 7)) :: Expr '[] (TSum '["Found" ::: TInt, "Missing" ::: TString]))
      ( EHandler @"value" @"Found" (EOp OPlus (EVar (IS IZ)) (EPrim (PInt 1)))
          :& EHandler @"message" @"Missing" (EOp OPlus (EVar IZ) (EPrim (PInt 1)))
          :& RNil
      )
<interactive> error:
    • Couldn't match type: (n0 ::: TInt) : xs0
                     with: '[]
<interactive> error:
    • Couldn't match type ‘TString’ with ‘TInt’

And using the ListIx helpers, those same failures show up as failed index searches:

ghci> :t (eVar "missing" :: Expr '[] TInt)
<interactive> error:
    • No instance for ‘ListIx "missing" '[] TInt’

ghci> :t (eVar "x" :: Expr '["x" ::: TString] TInt)
<interactive> error:
    • No instance for ‘ListIx "x" '[] TInt’

ghci> :t ECase
      (eChoice "Found" (EPrim (PInt 7)) :: Expr '[] (TSum '["Found" ::: TInt, "Missing" ::: TString]))
      ( eHandler "value" "Found" (EOp OPlus (eVar "missing") (EPrim (PInt 1)))
          :& eHandler "message" "Missing" (EOp OPlus (eVar "message") (EPrim (PInt 1)))
          :& RNil
      )
<interactive> error:
    • No instance for ‘ListIx "missing" '[] TInt’
<interactive> error:
    • No instance for ‘ListIx "message" '[] TInt’

Expressions that are not well-typed in our domain language are now rejected by GHC!¹

(As an exercise, can understand why those errors are what they are? Why they all contain ListIx _ '[]? For more ergonomics there is stuff we can do with TypeError machinery to make the messages a little prettier; the vinyl library does a lot to make error messages a bit better, like in HasField instance)

Note that this is sometimes done using straight De Bruijn indices: Expr :: [Ty] -> Type, so we don’t use any names but just the direct index, but the point of this exercise is to be borderline unbearable to write, and not to be actually unbearable to write.

Eval with a typed environment

To actually write eval now, we need to have a type-safe environment to store these variables. In order to eval an Expr vs, we need EValues for each v in vs. So for Expr ["x" ::: TInt, "y" ::: TBool], we need to store a TInt and a TBool. We can once again re-purpose Rec:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L130-L131

data EValueField :: (Symbol, Ty) -> Type where
  EVField :: EValue a -> EValueField '(l, a)

ghci> :t (EVField (EVInt 3) :& EVField (EVBool True) :& RNil :: Rec EValueField ["x" ::: TInt, "y" ::: TBool])
Rec EValueField ["x" ::: TInt, "y" ::: TBool]

And so we can finally write:

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L122-L271

data EValue :: Ty -> Type where
  EVInt :: Int -> EValue TInt
  EVBool :: Bool -> EValue TBool
  EVString :: String -> EValue TString
  EVRecord :: Rec EValueField as -> EValue (TRecord as)
  EVSum :: Index as (l ::: a) -> EValue a -> EValue (TSum as)
  EVFun :: (EValue a -> EValue b) -> EValue (a :-> b)

eval :: Rec EValueField vs -> Expr vs t -> EValue t
eval env = \case
  EPrim (PInt n) -> EVInt n
  EPrim (PBool b) -> EVBool b
  EPrim (PString s) -> EVString s
  EVar i -> case indexRec i env of
    EVField v -> v
  ELambda body ->
    EVFun $ \x -> eval (EVField x :& env) body
  EApply f x -> case eval env f of
    EVFun g -> g (eval env x)
  EOp o x y -> case (o, eval env x, eval env y) of
    (OPlus, EVInt a, EVInt b) -> EVInt (a + b)
    (OTimes, EVInt a, EVInt b) -> EVInt (a * b)
    (OLte, EVInt a, EVInt b) -> EVBool (a <= b)
    (OAnd, EVBool a, EVBool b) -> EVBool (a && b)
  ERecord xs ->
    EVRecord $ mapRec (\(EField x) -> EVField (eval env x)) xs
  EAccess e i -> case eval env e of
    EVRecord xs -> case indexRec i xs of
      EVField v -> v
  EChoice i x -> EVSum i (eval env x)
  ECase x hs -> case eval env x of
    EVSum i y -> case indexRec i hs of
      EHandler h -> eval (EVField y :& env) h

At least, we are here. A type-safe EDSL where only AST’s that can be validly evaluated are legal to represent in Haskell. At least, we can embrace the freedom of not having to carefully construct your terms. You can relax now. The compiler and the types have your back.

Even EVFun :: (EValue a -> EValue b) -> EValue (a :-> b) has a total EValue a -> EValue b, making the closure evaluation also fully total.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L145-L147

plusThree :: Expr '[] (TInt :-> TInt)
plusThree =
  eLambda "x" (EOp OPlus (eVar "x") (EPrim (PInt 3)))

ghci> case eval RNil plusThree of
    EVFun f -> case f (EVInt 4) of
      EVInt x -> print x
7

Pretty-Printing Scoped Expressions

Now to get to the entire utility of this abstraction: inspecting and consuming the structure. For our new structure, we took out the string name from EVar in lieu of an index. This is intentional, so that we keep the “responsibility” of storing the string name at the ELambda constructor and not have EVar redundantly store it.

However, this means that for pretty-printing, we will need to track the variable names in the environment as we descend into lambdas. This is done very similar to how it was done in eval, but instead of tracking and indexing out the evaluated EValues, we track and index out the string names of each variable instead.

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L182-L183

data NameField :: (Symbol, Ty) -> Type where
  NameField :: KnownSymbol l => NameField (l ::: a)

ghci> :t NameField @"hello" :& NameField @"world" :& RNil
Rec NameField ["hello" ::: a, "world" ::: b]

-- source: https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage4.hs#L185-L245

ppPrim :: Prim t -> PP.Doc ann
ppPrim = \case
  PInt n -> PP.pretty n
  PBool b -> if b then "true" else "false"
  PString s -> PP.pretty (show s)

ppOp :: Op a b c -> PP.Doc ann
ppOp = \case
  OPlus -> "+"
  OTimes -> "*"
  OLte -> "<="
  OAnd -> "&&"

ppFields :: Rec NameField vs -> Rec (ExprField vs) xs -> [PP.Doc ann]
ppFields _ RNil = []
ppFields names (EField @l x :& xs) =
  (PP.pretty (symbolVal (Proxy @l)) <+> "=" <+> ppExpr names False x) : ppFields names xs

ppHandlers :: Rec NameField vs -> Rec (ExprHandler vs b) xs -> [PP.Doc ann]
ppHandlers _ RNil = []
ppHandlers names (EHandler @n @l body :& xs) =
  ( PP.pretty (symbolVal (Proxy @l))
      <+> PP.pretty (symbolVal (Proxy @n))
      <+> "->"
      <+> ppExpr (NameField @n :& names) False body
  )
    : ppHandlers names xs

ppExpr :: Rec NameField vs -> Bool -> Expr vs t -> PP.Doc ann
ppExpr names paren = \case
  EPrim p -> ppPrim p
  EVar i -> case indexRec i names of
    NameField @n -> PP.pretty (symbolVal (Proxy @n))
  ELambda @n body ->
    wrap $
      "\\" <> PP.pretty (symbolVal (Proxy @n))
        <+> "->"
        <+> ppExpr (NameField @n :& names) False body
  EApply f x ->
    wrap $ ppExpr names True f <+> ppExpr names True x
  EOp o x y ->
    wrap $ ppExpr names True x <+> ppOp o <+> ppExpr names True y
  ERecord xs ->
    PP.encloseSep "{ " " }" ", " (ppFields names xs)
  EAccess @l e _ ->
    ppExpr names True e <> "." <> PP.pretty (symbolVal (Proxy @l))
  EChoice @l _ x ->
    wrap $ PP.pretty (symbolVal (Proxy @l)) <+> ppExpr names True x
  ECase x hs ->
    wrap $
      PP.sep
        [ "case" <+> ppExpr names False x <+> "of"
        , PP.encloseSep "{ " " }" "; " (ppHandlers names hs)
        ]
  where
    wrap
      | paren = PP.parens
      | otherwise = id

prettyExpr :: Expr '[] t -> PP.Doc ann
prettyExpr = ppExpr RNil False

ghci> prettyExpr fifteen
(\x -> x * 3) 5

The Next Step

Well, we set out with a simple goal: an expression language that lives within Haskell that we can inspect and interrogate within the language, but where it was impossible to construct (in Haskell) a term that did not type-check (in the domain language).

But, honestly, why does it matter that our expression language has to reject invalid domain-level terms at the Haskell level? Why couldn’t we go the way of other expression DSLs in Haskell, where we settle with “untyped” terms being expressible in Haskell, and validated using a separate typeCheck function to validate terms at runtime?

I don’t know. But really, maybe this is another way of taking the old Parse, Don’t Validate adage to the extreme. Why allow yourself to construct invalid terms of your domain inside Haskell? Why use a “validate” function (isValid) when you can just make invalid terms impossible to construct?

But…no. There is no other choice. We CANNOT allow invalid domain terms to be constructible. If we have the ability to do better, we MUST. With great power comes great responsibility. And if we compromise here, how can we trust ourselves not to compromise when it really matters?

One must imagine the stubborn typer happy.

In Part 2, we’ll use our new EDSL to specify visualizable state machines and programs within Haskell that are type-checked to be correct, and what it looks like to actually use these within Haskell. And in Part 3, we’ll start “compiling” them to different language targets and different backends, with the assurance that our generated programs are all synchronized and self-consistent.

A Note on AI Coding

I guess I’m going to have to start mentioning this in every post. But, I really do feel like this “extreme type safety” approach is more critical than ever, in the age of agentic coding and LLM. I’ve been using LLMs in my daily coding for many months now at this point, and one common pattern I’ve noticed: when I start with a design with very clear, very strict types, LLMs excel. They make much fewer errors, and the type system provides more immediate feedback on their progress, without needing hundreds of defensive x != null-style guard pollution.

Once I can express what I want in the language of extreme “invalid states unrepresentable” types, LLM agents no longer feel like agents of chaotic spaghetti extruding unmaintainable code. Instead, it feels like…seeding a crystal and watching it grow into a beautiful, shimmering lattice. It feels like the language they yearn to speak. And the more expressive your types, the more beautiful the crystalline structure in the end.

Honestly, humans might have problems writing and using this code, but LLMs definitely don’t, if properly scaffolded! Since early 2026, at least, for me. We’ll explore a bit more about this once we have more to work with in Part 2.

Special Thanks

Excluding _|_ in Haskell-land (recursion or undefined), unfortunately.↩︎

"Five-Point Haskell": Total Depravity (and Defensive Typing)

Justin Le — Mon, 2 Feb 2026 15:06:46 UTC

I have thought about distilling the principles by which I program Haskell, and how I’ve been able to steer long-lived projects over years of growth, refactorings, and changes in demands. I find myself coming back to a few distinct and helpful “points” (“doctrines”, if you may allow me to say) that have yet to lead me astray.

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 the mindset we use to define “good” coding principles.

In this series, Five-Point Haskell, I’ll set out to establish a five-point framework for typed functional programming (and Haskell-derived) design that aims to produce code that is maintainable, correct, long-lasting, extensible, and beautiful to write and work with. We’ll reference real-world case studies with actual examples when we can, and also attempt to dispel thought-leader sound bites that have become all too popular on Twitter (“heresies”, so to speak).

Let’s jump right into point 1: the doctrine of Total Depravity, and why Haskell is perfectly primed to make living with it as frictionless as possible.

Total Depravity: If your code’s correctness depends on keeping complicated interconnected structure in your head, a devastating incident is not a matter of if but when.

Therefore, delegate these concerns to tooling and a sufficiently powerful compiler, use types to guard against errors, and free yourself to only mentally track the actual important things.

Mix-ups Are Inevitable

Think about the stereotype of a “brilliant programmer” that an inexperienced programmer has in their mind — someone who can hold every detail of a complex system in their head, every intricate connection and relationship between each component. There’s the classic Monkey User Comic that valorizes this ideal.

The 10x developer is one who can carry the state and interconnectedness of an entire system in their brain, and the bigger the state they can carry, the more 10x they are.

This is the myth of the hero programmer. Did you have a bug? Well, you just need to upgrade your mental awareness and your context window. You just need to be better and better at keeping more in your mind.

Actually addressing these issues in most languages requires a lot of overhead and clunkiness. But luckily we’re in Haskell.

Explicit Tags

The 2022 Atlassian Outage, in part, was the result of passing the wrong type of ID. The operators were intended to pass App IDs, but instead passed Site IDs, and the errors cascaded from there. It goes without saying that if you have a bunch of “naked” IDs, then mixing them up is eventually going to backfire on you.

newtype Id = Id String

type SiteId = Id
type AppId = Id

getApps :: SiteId -> IO [AppId]
deleteSite :: SiteId -> IO ()
deleteApp :: AppId -> IO ()

This is convenient because you get functions for all IDs without any extra work. Let’s say you want to serialize/print or deserialize/read these IDs — it can be helpful to give them all the same type so that you can write this logic in one place.

instance ToJSON Id where
  toJSON (Id x) = object [ "id" .= x ]

instance FromJSON Id where
  parseJSON = withObject "Id" $ \v ->
    Id <$> (v .: "id")

Convenient and effective, as long as you never accidentally use a SiteId as an AppId or vice versa. And this is a very easy delusion to fall into, if you don’t believe in total depravity. However, sooner or later (maybe in a week, maybe in a year, maybe after you onboard that new team member)…someone is going to accidentally pass a site ID where an app ID is expected.

main :: IO ()
main = do
    let targetSites = [Id "abc", Id "def"]
    mapM_ deleteApp targetSites

And at that point it’s all over.

Knowing this can happen, we can add a simple newtype wrapper so that accidentally using the wrong ID is a compile error:

newtype SiteId = SiteId String
newtype AppId = AppId String

And now such a mis-call will never compile! Congratulations!

We do have a downside now: we can no longer write code polymorphic over IDs when we want to. In the untagged situation, we could only write polymorphic code, and in the new situation we can only write code for one ID type.

instance FromJSON SiteId where
  parseJSON = withObject "Id" $ \v -> do
    tag <- v .: "type"
    unless (tag == "Site") $
      fail "Parsed wrong type of ID!"
    SiteId <$> (v .: "id")

instance ToJSON SiteId where
  toJSON (SiteId x) = object [ "type" .= "Site", "id" .= x ]

instance FromJSON AppId where
  parseJSON = withObject "Id" $ \v -> do
    tag <- v .: "type"
    unless (tag == "App") $
      fail "Parsed wrong type of ID!"
    AppId <$> (v .: "id")

instance ToJSON AppId where
  toJSON (AppId x) = object [ "type" .= "App", "id" .= x ]

However, luckily, because we’re in Haskell, it’s easy to get the best of both worlds with phantom types (that don’t refer to anything inside the actual data representation):

data Id a = Id { getId :: String }

data Site
data App

type SiteId = Id Site
type AppId = Id App

-- using Typeable for demonstration purposes
instance Typeable a => ToJSON (Id a) where
  toJSON (Id x) = object
    [ "type" .= show (typeRep @a)
    , "id" .= x
    ]

instance Typeable a => FromJSON (Id a) where
  parseJSON = withObject "Id" $ \v -> do
    tag <- v .: "type"
    unless (tag == show (typeRep @a)) $
      fail "Parsed wrong type of ID!"
    Id <$> (v .: "id")

Type safety doesn’t necessarily mean inflexibility!

Phantom Powers

Phantom types give us a lot of low-hanging fruit for preventing inadvertent misuse.

The 2017 DigitalOcean outage, for example, was partially about the wrong environment credentials being used.

We could imagine a test harness that clears a test database using postgresql-simple:

-- | Warning: do NOT call this outside of test environment!
clearTestEnv :: Connection -> IO ()
clearTestEnv conn = do
  putStrLn "Are you sure you read the warning on this function? Well, too late now!"
  _ <- execute_ conn "DROP TABLE IF EXISTS users CASCADE"
  putStrLn "Test data wiped."

However, somewhere down the line, someone is going to call clearTestEnv deep inside a function inside a function inside a function, which itself is called against the prod database. I guarantee it.

To ensure this never happens, we can use closed phantom types using DataKinds (made nicer with TypeData post-GHC 9.6):

-- type data = declare a closed kind and two type constructors at the type level using -XTypeData
type data Env = Prod | Test

newtype DbConnection (a :: Env) = DbConnection Connection

runQuery :: DbConnection a -> Query -> IO Int64
runQuery (DbConnection c) q = execute_ c q

-- | Warning: Did you remember to charge your chromebook? Oh and this function
-- is safe by the way.
clearTestEnv :: DbConnection Test -> IO ()
clearTestEnv conn = do
  _ <- runQuery conn "DROP TABLE IF EXISTS users CASCADE"
  putStrLn "Test data wiped."

connectProd :: IO (DbConnection Prod)
connectProd = DbConnection <$> connectPostgreSQL "host=prod..."

Now, if you create a connection using connectProd, you can use runQuery on it (because it can run any DbConnection a)…but if any sub-function of a sub-function calls clearTestEnv, it will have to unify with DbConnection Test, which is impossible for a prod connection.

This is somewhat similar to using “mocking-only” subclasses for dependency injection, but with a closed universe. I discuss patterns like this in my Introduction to Singletons series.

Correct Representations

Semantic Phantoms

And sometimes, phantom types can do the work for you, not only preventing mix-ups but also encoding business logic in their manipulation.

Take, for instance, the Mars Climate Orbiter failure, where the software module provided by Lockheed Martin expected US Customary Units, and another one developed by NASA expected SI units.

If I had a function like:

-- | In Newton-seconds
myMomentum :: Double
myMomentum = 20

-- | In Pounds-second
myImpulse :: Double
myImpulse = 4

-- | Make sure these are both the same units!
applyImpulse :: Double -> Double -> Double
applyImpulse currentMomentum impulse = currentMomentum + impulse

This is just asking for someone to come along and provide newtons alongside pounds. It isn’t even clear from the types what is expected!

We can instead use the dimensional library:

import qualified Numeric.Units.Dimensional.Prelude as U
import Numeric.Units.Dimensional ((*~))
import Numeric.Units.Dimensional.SIUnits
import Numeric.Units.Dimensional.NonSI

myMomentum :: Momentum
myMomentum = 20 *~ (newton U.* seconds)

myImpulse :: Impulse
myImpulse = 4 *~ (poundForce U.* seconds)

-- Verify at compile-time that we can use '+' with Momentum and Impulse
applyImpulse :: Momentum -> Impulse -> Momentum
applyImpulse currentMomentum impulse = currentMomentum + impulse

Now as long as momentum and impulse are provided in the correct types at API boundaries, no mix-up will happen. No need to send 300 million dollars down the drain! Libraries will just need to provide a unified Momentum or Impulse type, and everything will work out.

The Billion-Dollar Mistake

Speaking of costly errors, there is one extremely egregious pattern that is so pervasive, so alluring, and yet so inevitably devastating, it has been dubbed the “Billion Dollar Mistake”. It’s the idea of a sentinel value, or in-band signaling.

There are examples:

String.indexOf(), str.find(), etc. in many languages return -1 if the substring is not found
C’s fgetc(), getchar(), return -1 for EOF. And if you cast to char, you basically can’t distinguish EOF from 0xff (ÿ).
malloc() returning the pointer 0 means not enough memory
Some languages have a special NULL pointer value as well — or even a value null that can be passed in for any expected type or object or value.
JavaScript’s parseInt returns not null, but rather NaN for a bad parse — giving two distinct sentinel values
A lot of Unix scripting uses the empty string "" for non-presence
Sensor firmware often reports values like -999 for a bad reading…but sometimes -999 might actually be a valid value!

It should be evident that these are just accidents and ticking time bombs waiting to happen. Some caller just needs to forget to handle the sentinel value, or to falsely assume that the sentinel value is impossible to occur in any situation.

It’s called the billion dollar mistake, but it’s definitely arguable that the cumulative damage has been much higher. High-profile incidents include sock_sendpage and the 2025 GCP outage, but if you’re reading this and you are honest with yourself, it’s probably happened to you multiple times and has been the source of many frustrating bug hunts.

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.

Why do we do this to ourselves? Because it is convenient. In the case of EVP_VerifyInit, we can define an enum instead…

data VerifyResult = Success | Failure | Error

However, it’s not easy to make an “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:

unsafeIndexOf :: String -> String -> Int

-- vs.

-- takes a success continuation and a failure continuation
indexOf :: String -> String -> (Int -> r) -> (() -> r) -> r

All of this just to fake having actual sum types.

We don’t really have an excuse in Haskell, since we can just return Maybe:

-- from Data.Vector
elemIndex :: Eq a => a -> Vector a -> Maybe Int

Returning Maybe or Option forces the caller to handle:

case elemIndex 3 myVec of
  Just i -> -- ..
  Nothing -> -- ..

and this handling is compiler-enforced. Provided, of course, you don’t intentionally throw away your type-safety and compiler checks for no reason. You can even return Either with an enum for richer responses, and very easily chain erroring operations using Functor and Monad. In fact, with cheap ADTs, you can define your own rich result type, like in unix’s ProcessStatus:

data ProcessStatus
   = Exited ExitCode
   | Terminated Signal Bool
   | Stopped Signal

Imagine trying to cram all of that information into an int!

Unmarked Assumptions

Assumptions kill, and a lot of times we arrive at implicit assumptions in our code. Unfortunately, even if we add these assumptions in our documentation, it only takes a minor refactor or lapse in memory for these to cause catastrophic incidents.

There are the simple cases — consider a mean function:

-- | Warning: do not give an empty list!
mean :: [Double] -> Double
mean xs = sum xs / fromIntegral (length xs)

But are you really going to remember to check if your list is empty every time you give it to mean? No, of course not. Instead, make it a compiler-enforced constraint.

mean :: NonEmpty Double -> Double
mean xs = sum xs / fromIntegral (length xs)

Now mean takes a NonEmpty list, which can only be created safely using nonEmpty :: [a] -> Maybe (NonEmpty a) (where the caller has to explicitly handle the empty list case, so they’ll never forget) or from functions that already return NonEmpty by default (like some :: f a -> f (NonEmpty a) or group :: Eq a => [a] -> [NonEmpty a]), allowing you to beautifully chain post-conditions directly into pre-conditions.

Accessing containers is, in general, very fraught…even things like indexing lists can send us into a graveyard spiral. Sometimes the issue is more subtle. This is our reminder to never let these implicit assumptions go unnoticed.

Separate Processed Data

“Shotgun parsing” involves mixing validated and unvalidated data at different levels in your program. Oftentimes it is considered “fine” because you just need to remember which inputs are validated and which aren’t…right? In truth, all it takes is a simple temporary lapse of mental model, a time delay between working on code, or uncoordinated contributions before things fall apart.

Consider a situation where we validate usernames only on write to the database.

validUsername :: String -> Bool
validUsername s = all isAlphaNum s && all isLower s

-- | Returns 'Nothing' if username is invalid or insertion failed
saveUser :: Connection -> String -> IO (Maybe UUID)
saveUser conn s
  | validUsername s = do
      newId <- query conn "INSERT INTO users (username) VALUES (?) returning user_id" (Only s)
      pure $ case newId of
        [] -> Nothing
        Only i : _ -> Just i
  | otherwise = pure Nothing

getUser :: Connection -> UUID -> IO (Maybe String)
getUser conn uid = do
  unames <- query conn "SELECT username FROM users where user_id = ?" (Only uid)
  pure $ case unames of
    [] -> Nothing
    Only s : _ -> Just s

It should be fine as long as you only ever use saveUser and getUser…and nobody else has access to the database. But, if someone hooks up a custom connector, or does some manual modifications, then the users table will now have an invalid username, bypassing Haskell. And because of that, getUser can return an invalid string!

Don’t assume that these inconsequential slip-ups won’t happen; assume that it’s only a matter of time.

Instead, we can bake the state of a validated string into the type itself:

newtype Username = UnsafeUsername String
  deriving (Show, Eq)

-- | Our "Smart Constructor"
mkUsername :: String -> Maybe Username
mkUsername s
  | validUsername s = Just (UnsafeUsername s)
  | otherwise       = Nothing

-- | Access the raw string if needed
unUsername :: Username -> String
unUsername (UnsafeUsername s) = s

Username and String themselves are not structurally different — instead, Username is a compiler-enforced tag specifying it went through a specific required validation function within Haskell, not just externally verified.

Now saveUser and getUser are safe at the boundaries:

saveUser :: Connection -> Username -> IO (Maybe UUID)
saveUser conn s = do
  newId <- query conn "INSERT INTO users (username) VALUES (?) returning user_id" (Only (unUsername s))
  pure $ case newId of
    [] -> Nothing
    Only i : _ -> Just i

getUser :: Connection -> UUID -> IO (Maybe Username)
getUser conn uid = do
  unames <- query conn "SELECT username FROM users where user_id = ?" (Only uid)
  pure $ case unames of
    [] -> Nothing
    Only s : _ -> mkUsername s

(In real code, of course, we would use a more usable indication of failure than Maybe)

We can even hook this into Haskell’s typeclass system to make this even more rigorous: Username could have its own FromField and ToField instances that push the validation to the driver level.

instance FromField Username where
  fromField f mdata = do
    s :: String <- fromField f mdata
    case mkUsername s of
      Just u  -> pure u
      Nothing -> returnError ConversionFailed f ("Invalid username format: " ++ s)

instance ToField Username where
  toField = toField . unUsername

saveUser :: Connection -> Username -> IO (Maybe UUID)
saveUser conn s = do
  newId <- query conn "INSERT INTO users (username) VALUES (?) returning user_id" (Only s)
  pure $ case newId of
    [] -> Nothing
    Only i : _ -> Just i

getUser :: Connection -> UUID -> IO (Maybe Username)
getUser conn uid = do
  unames <- query conn "SELECT username FROM users where user_id = ?" (Only uid)
  pure $ case unames of
    [] -> Nothing
    Only s : _ -> Just s

Pushing it to the driver level will also unify everything with the driver’s error-handling system.

These ideas are elaborated further in one of the best Haskell posts of all time, Parse, Don’t Validate.

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 as to what it means. You can sort of interpret the 1999 Mars Polar Lander crash this way. Its functions took a boolean based on the state of the legs:

deployThrusters :: Bool -> IO ()

and True and False were misinterpreted. Instead, they could have considered semantically meaningful types: (simplified)

data LegState = Extended | Retracted

deployThrusters :: LegState -> IO ()

Note that Maybe itself is not immune from “semantic blindness” — if you find yourself using a lot of anonymous combinators like Maybe and Either to get around boolean blindness, be aware of falling into algebraic blindness!

Resource Cleanup

Clean-up of finite system resources is another area that is very easy to assume you have a handle on before it gets out of hand and sneaks up on you.

process :: Handle -> IO ()

doTheThing :: FilePath -> IO ()
doTheThing path = do
  h <- openFile path ReadMode
  process h
  hClose h

A bunch of things could go wrong —

You might forget to always hClose a file handle, and if your files come at you dynamically, you’re going to run out of file descriptors, or hold on to locks longer than you should
If process throws an exception, we never get to hClose, and the same issues happen
If another thread throws an asynchronous exception (like a thread cancellation), you have to make sure the close still happens!

The typical solution that other languages (like Python, modern Java) take is to put everything inside a “block” where quitting the block guarantees the closure. In Haskell we have the bracket pattern:

-- strongly discourage using `openFile` and `hClose` directly
withFile :: FilePath -> (Handle -> IO r) -> IO r
withFile path = bracket (openFile path ReadMode) hClose

doTheThing :: FilePath -> IO ()
doTheThing path = withFile path $ \h -> do
  process h

If you never use openFile directly, and always use withFile, all file usage is safe!

But, admittedly, continuations can be annoying to work with. For example, what if you wanted to safely open a list of files?

processAll :: [Handle] -> IO ()

doTheThings :: [FilePath] -> IO ()
doTheThings paths = -- uh...

All of a sudden, not so fun. And what if you had, for example, a Map of files, like Map Username FilePath?

processAll :: Map Username Handle -> IO ()

doTheThings :: Map Username FilePath -> IO ()
doTheThings paths = -- uh...

In another language, at this point, we might just give up and resort to manual opening and closing of files.

But this is Haskell. We have a better solution: cleanup-tracking monads!

This is a classic usage of ContT to let you chain bracket-like continuations:

processTwo :: Handle -> Handle -> IO ()

doTwoThings :: FilePath -> FilePath -> IO ()
doTwoThings path1 path2 = evalContT $ do
    h1 <- ContT $ withFile path1
    h2 <- ContT $ withFile path2
    liftIO $ processTwo h1 h2

processAll :: Map Username Handle -> IO ()

doTheThings :: Map Username FilePath -> IO ()
doTheThings paths = evalContT $ do
    handles <- traverse (ContT . withFile) paths
    liftIO $ processAll handles

However, using ContT doesn’t allow you to do things like early cleanups or canceling cleanup events. It forces us into a last-in, first-out sort of cleanup pattern. If you want to deviate, this might cause you to, for convenience, go for manual resource management. However, we have tools for more fine-grained control, we have things like resourcet ResourceT, which lets you manually control the order of clean-up events, with the guarantee that all of them eventually happen.

import qualified Data.Map as M

-- | Returns set of usernames to close
processAll :: Map Username Handle -> IO (Set Username)

allocateFile :: FilePath -> ResourceT IO (ReleaseKey, Handle)
allocateFile fp = allocate (openFile fp ReadMode) hClose

-- Guarantees that all handles will eventually close, even if `go` crashes
doTheThings :: Map Username FilePath -> IO ()
doTheThings paths = runResourceT $ do
    releasersAndHandlers <- traverse allocateFile paths
    go releasersAndHandlers
  where
    -- normal operation: slowly releases handlers as we drop them
    go :: Map Username (ReleaseKey, Handle) -> ResourceT IO ()
    go currOpen = do
      toClose <- liftIO $ processAll (snd <$> currOpen)
      traverse_ (release . fst) (currOpen `M.restrictKeys` toClose)
      let newOpen = currOpen `M.withoutKeys` toClose
      unless (M.null newOpen) $
        go newOpen

Here we get the best of both worlds: the ability to manually close handlers when they are no longer needed, but also the guarantee that they will eventually be closed.

Embracing Total Depravity

Hopefully these examples, and similar situations, should feel relatable. We’ve all experienced the biting pain of too much self-trust. Or, too much trust in our ability to communicate with team members. Or, too much trust in ourselves 6 months from now. The traumas described here should resonate with you if you have programmed in any capacity for more than a couple of scripts.

The doctrine of total depravity does not mean that we don’t recognize the ability to write sloppy code that works, or that flow states can enable some great feats. After all, we all program with a certain sense of imago machinae. Instead, it means that all such states are fundamentally unstable in their nature and will always fail at some point. The “total” doesn’t mean we are totally cooked, it means this eventual reckoning applies to all such shortcuts.

The problem won’t be solved by “get good”. The problem is solved by utilizing the tooling we are given, especially since Haskell makes them so accessible and easy to pull in.

There’s another layer here that comes as a result of embracing this mindset: you’ll find that you have more mental space to dedicate to things that actually matter! Instead of worrying about inconsequential minutiae and details of your flawed abstractions, you can actually think about your business logic, the flow of your program, and architecting that castle of beauty I know you are capable of.

In the Age of Agentic Coding

Before we end, let’s address the elephant in the room. We’re writing this in 2026, in the middle of one of the biggest revolutions in software engineering in the history of the field. A lot of people have claimed that types and safety are now no longer important in the age of LLMs and agentic coding.

However, these claims seem to miss the fact that the fundamental issue being addressed here exists both in LLMs and humans: the limited “context window” and attention. Humans might be barely able to keep a dozen things in our heads, LLMs might be able to keep a dozen dozen things, but it will still be ultimately finite. So, the more we can move concerns out of our context window (be it biological or mechanical), the less crowded our context windows will be, and the more productive we will be.

Agentic coding is progressing quickly, and over the past few months I have been exploring this a lot, using models hands-on. One conclusion I have found (and, this agrees with everyone else I’ve asked who has been trying the same thing) is that Haskell’s types, in many ways, are the killer productivity secret of agentic coding.

Many of my Haskell coding tasks for an LLM agent often involve:

How will the types change, or what should the types be?
Ralph Wiggum loop to death until the program typechecks, using ghci and cabal.

And, this isn’t 100% effective, but from personal experience it is much more effective than the similar situation without typed guardrails for fast feedback, and without instant compiler feedback. The feedback loop is tighter, the objectives clearer, the constraints more resilient, the tooling more utilized.

I have noticed, also, that my LLM agents often check the types of the APIs using ghci :type, and rarely the documentation of the functions using ghci :docs. So, any “documentation-based contracts” are definitely much more likely to explode in your face in this new world than type-based contracts.

I’m not sure how quickly LLM-based agentic coding will progress, but I am sure that the accidental “dropping” of concerns will continue to be a bottleneck. All of the traits described in this post for humans will continue to be traits of limited context windows for LLMs.

If anything, limited “brain space” might be the bottleneck, for both humans and LLMs. If provide LLMs with properly “depravity-aware” typed code (and encourage them to write it by giving them the right iterative tooling), I truly believe that we have the key to unlocking the full potential of agentic coding.

And…not whatever this tweet is.

The Next Step

Total depravity is all about using types to prevent errors. However, you can only go so far with defensive programming and carefully picking the structure of your types. Sometimes, it feels like you are expending a lot of energy and human effort just picking the perfectly designed data type, only for things out of your hand to ruin your typed castle.

In the next chapter, we’ll see how a little-discussed aspect of Haskell’s type system gives you a powerful tool for opening your mind to new avenues of design that were impossible before. At the same time, we’ll see how we can leverage universal properties of mathematics itself to help us analyze our code in unexpected ways.

Let’s explore this further in the next principle of Five-Point Haskell, Unconditional Election!

Special Thanks

Also thanks to jackdk’s comment for highlighting extra resources and context that I believe are very useful and relevant!

Advent of Code 2025: Haskell Solution Reflections for all 12 Days

Justin Le — Wed, 24 Dec 2025 20:44:05 UTC

Merry Christmas all! This is my annual Advent of Code post! Advent of Code is a series of (this year) 12 daily Christmas-themed programming puzzles that are meant to be fun diversions from your daily life, help you find a bit of whimsy in your world, give you a chance to explore new ideas and program together with your friends. I always enjoy discussing creative ways to solve these puzzles every day, and it’s become a bit of an annual highlight for me and a lot of others. My favorite part about these puzzles is that they are open ended enough that there are usually many different interesting ways to solve them — it’s not like a stressful interview question where you have to recite the obscure incantation to pass the test. In the past I’ve leveraged group theory, galilean transformations and linear algebra, and more group theory.

Haskell is especially fun for these because if you set up your abstractions in just the right way, the puzzles seem to solve themselves. It’s a good opportunity every year to get exposed to different parts of the Haskell ecosystem! Last year, I moved almost all of my Haskell code to an Advent of Code Megarepo, and I also write up my favorite ways to solve each one in the megarepo wiki.

All of this year’s 12 puzzles are here, but I’ve also included links to each individual one in this post. I’m also considering expanding some of these into full on blog posts, so be on the look out, or let me know if there are any that you might want fully expanded! And if you haven’t, why not try these out yourself? Be sure to drop by the libera-chat ##advent-of-code channel to discuss any fun ways you solve them, or any questions! Thanks again to Eric for a great new fresh take on the event this year!

Day 1 - Secret Entrance — The classic Day 1 scanl
Day 2 - Gift Shop — The super efficient IntSet
Day 3 - Lobby — StateT + [] = backtracking search monad
Day 4 - Printing Department — 2D cellular automata
Day 5 - Cafeteria — The power of the data-interval library
Day 6 - Trash Compactor — Data.List manipulations
Day 7 - Laboratories — Tying the knot
Day 8 - Playground — Iterative Clustering
Day 9 - Movie Theater — IntervalSet and IntervalMap
Day 10 - Factory — Guassian Elimation, Type-safe Mutable Vectors
Day 11 - Reactor — More Knot Tying and DP!
Day 12 - Christmas Tree Farm — Counting