https://feeds.feedburner.com/incodeblog

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:

1. How will the types change, or what should the types be?
2. 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

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

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

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

Everybody Loves My Baby is a Jazz Standard from 1924 with the famous lyric:

Everybody loves my baby, but my baby don’t love nobody but me.

Which is often formalized as:

\[ \begin{align} \text{Axiom}_1 . & \forall x. \text{Loves}(x, \text{Baby}) \\ \text{Axiom}_2 . \forall x. & \text{Loves}(\text{Baby}, x) \implies x = me \end{align} \]

Let’s prove in Haskell (in one line) that these two statements, taken together, imply that I am my own baby.

The normal proof

The normal proof using propositional logic goes as follows:

1. If everyone loves Baby, Baby must love baby. (instantiate axiom 1 with \(x = \text{Baby}\)).
2. If baby loves someone, that someone must be me. (axiom 2)
3. Therefore, because baby loves baby, baby must be me. (instantiate axiom 2 with axiom 1 with \(x = \text{Baby}\))

Haskell as a Theorem Prover

First, some background: when using Haskell as a theorem prover, you represent the theorem as a type, and proving it involves constructing a value of that type — you create an inhabitant of that type.

Using the Curry-Howard correspondence (often also called the Curry-Howard isomorphism), we can pair some simple logical connectives with types:

1. Logical “and” corresponds to tupling (or records of values). If (a, b) is inhabited, it means that both a and b are inhabited.
2. Logical “or” corresponds to sums, Either a b being inhabited implies that either a or b are inhabited. They might both the inhabited, but Either a b requires the “proof” of only one.
3. Constructivist logical implication is a function: If a -> b is inhabited, it means that an inhabitant of a can be used to create an inhabitant of b.
4. Any type with a constructor is “true”: (), Bool, String, etc.; any type with no constructor (data Void) is “false” because it has no inhabitants.
5. Introducing type variables (forall a.) corresponds to…well, for all. If forall a. Either a () means that Either a () is “true” (inhabited) for all possible a. This one represented logically as \(\forall x. x \lor \text{True}\).

You can see that, by chaining together those primitives, you can translate a lot of simple proofs. For example, the proof of “If x and y together imply z, then x implies that y implies z”:

\[ \forall x y z. ((x \wedge y) \implies z) \implies (x \implies (y \implies z)) \]

can be expressed as:

curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
curry f x y = f (x, y)

Or maybe, “If either x or y imply z, then x implies z and y implies z, independently:”

\[ \forall x y z. ((x \lor y) \implies z) \implies ((x \implies z) \land (y \implies z))) \]

In haskell:

unEither :: (Either a b -> c) -> (a -> c, b -> c)
unEither f = (f . Left, f . Right)

And, we have a version of negation: if a -> Void is inhabited, then a must be uninhabited (the principle of explosion). Let’s prove that “‘x or y’ being false implies both x and y are false”: \(\forall x y. \neg(x \lor y) \implies (\neg x \wedge \neg y)\)

deMorgan :: (Either a b -> Void) -> (a -> Void, b -> Void)
deMorgan f = (f . Left, f . Right)

(Maybe surprisingly, that’s the same proof as unEither!)

We can also think of “type functions” (type constructors that take arguments) as “parameterized propositions”:

data Maybe a = Nothing | Maybe a

Maybe a (like \(\text{Maybe}(x)\)) is the proposition that \(\text{True} \lor x\): Maybe a is always inhabited, because “True or X” is always True. Even Maybe Void is inhabited, as Nothing :: Maybe Void.

The sky is the limit if we use GADTs. We can create arbitrary propositions by restricting what types constructors can be called with. For example, we can create a proposition that x is an element of a list:

data Elem :: k -> [k] -> Type where
    Here :: Elem x (x : xs)
    There :: !(Elem x ys) -> Elem x (y : ys)

Read this as “Elem x xs is true (inhabited) if either x is the first item, or if x is an elem of the tail of the list”. So for example, Elem 5 [1,5,6] is inhabited but Elem 7 [1,5,6] is not:1

itsTrue :: Elem 5 [1,5,6]
itsTrue = There Here

itsNotTrue :: Elem 7 [1,5,6] -> Void
itsNotTrue = \case {}     -- GHC is smart enough to know both cases are invalid

We can create a two-argument proposition that two types are equal, a :~: b:

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

The proposition a :~: b is only inhabited if a is equal to b, since Refl is its only constructor.

Of course, this whole correspondence assumes we aren’t ever touching bottom (things like undefined for let x = x in x). For this exercise, we are working in a total subset of Haskell.

The Baby Paradox

Now we have enough. Let’s parameterize it over a proposition loves, where loves a b being inhabited means that a loves b.

We can express our axiom as a record of propositions in terms of the atoms loves, me, and baby:

data BabyAxioms loves me baby = BabyAxioms
    { everybodyLovesMyBaby :: forall x. loves x baby
    , myBabyOnlyLovesMe :: forall x. loves baby x -> x :~: me
    }

The first axiom everybodyLovesMyBaby means that for any x, loves x baby must be “true” (inhabited). The second axiom myBabyOnlyLovesMe means that if we have a loves baby x (if my baby loves someone), then it must be that x ~ me: we must be able to derive that person the baby loves is indeed me.

The expression of the baby paradox then relies on writing the function

babyParadox :: BabyAxioms loves me baby -> me :~: baby

And indeed if we play around with GHC enough, we’ll get this typechecking implementation:

babyParadox :: BabyAxioms loves me baby -> me :~: baby
babyParadox BabyAxioms{everybodyLovesMyBaby, myBabyOnlyLovesMe} =
    myBabyOnlyLovesMe everybodyLovesMyBaby

Using x & f = f x from Data.Function, this becomes a bit smoother to read:

babyParadox :: BabyAxioms loves me baby -> me :~: baby
babyParadox BabyAxioms{everybodyLovesMyBaby, myBabyOnlyLovesMe} =
    everybodyLovesMyBaby & myBabyOnlyLovesMe

And we have just proved it! It ended up being a one-liner. So, given the BabyAxioms loves me baby, it is possible to prove that me must be equal to baby. That is, it is impossible to create any BabyAxioms without me and baby being the same type.

The actual structure of the proof goes like this:

1. First, we instantiated everybodyLovesBaby with x ~ baby, to get loves baby baby.
2. Then, we used myBabyOnlyLovesMe, which normally takes loves baby x and returns x :~: me. Because we give it loves baby baby, we get a baby :~: me!

And that’s exactly the same structure of the original symbolic proof.

What is Love?

We made BabyAxioms parametric over loves, me, and baby, which means that these apply in any universe where love, me, and baby follow the rules of the song lyrics.

Essentially this means that for any binary relationship Loves x y, if that relationship follows these axioms, it must be true that me is baby. No matter what that relationship actually is, concretely.

That being said, it might be fun to play around with what this might look like in concrete realizations of love, me, and my baby.

First, we could imagine that Love is completely mundane, and can be created between any two operands without any extra required data or constraints — essentially, a proxy between two phantoms:

data Love a b = Love

In this case, it’s impossible to create a BabyAxioms where me and baby are different:

data Love a b = Love

-- | me ~ baby is a cosntraint required by GHC
proxyLove :: (me ~ baby) => BabyAxioms Love me baby
proxyLove = BabyAxioms
    { everybodyLovesMyBaby = Love
    , myBabyOnlyLovesMe = \_ -> Refl
    }

The me ~ baby constraint being required by GHC is actually an interesting manifestation of the paradox itself, without an explicit proof required on our part. Alternatively, and more traditionally, we can write proxyLove :: BabyAxioms Love baby baby or proxyLove :: BabyAxioms Love me me to mean the same thing.

We can imagine another concrete universe where it is only possible to love my baby, and my baby is the singular recipient of love in this entire universe:

data LoveOnly :: k -> k -> k -> Type where
    LoveMyBaby :: LoveOnly baby x baby

onlyBaby :: BabyAxioms (LoveOnly baby) me baby
onlyBaby = BabyAxioms
    { everybodyLovesMyBaby = LoveMyBaby
    , myBabyOnlyLovesMe = \case LoveMyBaby -> Refl
    }

Now we get both axioms fulfilled for free! Basically if we ever have a LoveOnly baby x me, the only possible constructor is is LoveMyBaby :: LoveOnly baby x baby, so me must be baby!

Finally, we could imagine that love has no possible construction, with no way to construct or realize. In this case, love is the uninhabited Void:

data Love a b

In this universe, we can finally fulfil myBabyOnlyLovesMe without me being baby, because “my baby don’t love nobody but me” is vacuously true if there is no possible love. However, we cannot fulfil everybodyLovesMyBaby because no love is possible, except in the case that the universe of people (k) is also empty. But GHC doesn’t have any way to encode empty kinds, I believe (I would love to hear of any techniques if you knew of any), so we cannot realize these axioms even if forall (x :: k) is truly empty.

Note that we cannot fully encode the axioms purely as a GADT in Haskell — our LoveOnly was close, but it is too restrictive: in a fully general interpretation of the song, we want to be able to allow other recipients of love besides baby. Basically, Haskell GADTs cannot express the eliminators necessary to encode myBabyOnlyLovesMe purely structurally, as far as I am aware. But I could be wrong.

Why

Nobody who listens to this song seriously believes that the speaker is intending to convey that they are their own baby, or attempting to tantalize the listener with an unintuitive tautology. However, this is indeed a common homework assignment in predicate logic classes, and I wasn’t able to find anyone covering this yet in Haskell, so I thought might as well be the first.

Sorry, teachers of courses that teach logic through Haskell.

I’ve also been using paradox as one of my go-to LLM stumpers, and it’s actually only recently (with GPT 5) that it’s been able to get this right. Yay the future? Before this, it would get stuck on trying to define a Loves GADT, which is a dead end as previously discussed.

---

1. I’m pretty sure nobody has ever used it for anything useful, but I wrote the entire decidable library around manipulating propositions like this.↩︎

Haskell is the world’s best programming language1, but let’s face the harsh reality that a lot of times in life you’ll have to write in other programming languages. But alas you have been fully Haskell-brained and lost all ability to program unless it is type-directed, you don’t even know how to start writing a program without imagining its shape as a type first.

Well, fear not. The foundational theory behind Algebraic Data Types and Generalized Algebraic Data Types (ADTs and GADTs) are so fundamental that they’ll fit (somewhat) seamlessly into whatever language you’re forced to write. After all, if they can fit profunctor optics in Microsoft’s Java code, the sky’s the limit!

This is an “April Fools” joke in the tradition of my previous one in some of these ways that we are going to twist these other languages might seem unconventional or possibly ill-advised… but also the title is definitely a lie: these languages definitely should have them! :D

Normal ADTs

As a reminder, algebraic Data Types (ADTs) are products and sums; that’s why they’re algebraic, after all!

Product Types

Products are just immutable structs, which pretty much every language supports — as long as you’re able to make sure they are never mutated.

Structs in c, for example, look like:

#include <stdint.h>

typedef struct {
    uint32_t timestamp;
    double amount;
} Transaction;

But you’ll need proper immutable API for it:

Transaction createTransaction(uint32_t timestamp, double amount) {
    return (Transaction){ timestamp, amount};
}

uint32_t getTimestamp(const Transaction* t) {
    return t->timestamp;
}

double getAmount(const Transaction* t) {
    return t->amount;
}

Transaction setTimestamp(const Transaction* t, uint32_t timestamp) {
    return (Transaction){timestamp, t->amount};
}

Transaction setAmount(const Transaction* t, double amount) {
    return (Transaction){t->timestamp, amount};
}

This is much simpler in languages where you can associate functions with data, like OOP and classes. For example, this is the common “value object” pattern in java (roughly related to the java bean2):

public class Transaction {
    private final long timestamp;
    private final double amount;

    public Transaction(long timestamp, double amount) {
        this.timestamp = timestamp;
        this.amount = amount;
    }

    public long getTimestamp() { return timestamp; }
    public double getAmount() { return amount; }

    public Transaction setTimestamp(long newTimestamp) {
        return new Transaction(newTimestamp, this.amount);
    }

    public Transaction setAmount(double newAmount) {
        return new Transaction(this.timestamp, newAmount);
    }
}

And there you go. Nothing too surprising there!

In this case, not only are these ADTs (algebraic data types), they’re also ADTs (abstract data types): you are meant to work with them based on a pre-defined abstract interface based on type algebra, instead of their internal representations.

Sum Types

If your language doesn’t support sum types, usually the way to go is with the visitor pattern: the underlying implementation is hidden, and the only way to process a sum type value is by providing handlers for every branch — a pattern match as a function, essentially. Your sum values then basically determine which handler is called.

For example, we can implement it for a network address type that can either be IPv4 or IPv6. Here we are using C++ just for generics and lambdas with closures, for simplicity, but we’ll discuss how this might look in C later.

#include <iostream>
#include <format>
#include <cstdint>

struct IPAddress {
    bool isIPv4;
    union {
        uint32_t ipv4;
        uint8_t ipv6[16];
    };
};

template <typename R>
struct IPAddressVisitor {
    R (*visitIPv4)(uint32_t);
    R (*visitIPv6)(const uint8_t (&)[16]);
};

template <typename R>
R acceptIPAddress(const IPAddress& ip, IPAddressVisitor<R> visitor) {
    return ip.isIPv4 ? visitor.visitIPv4(ip.ipv4)
                     : visitor.visitIPv6(ip.ipv6);
}

You can create the values using:

IPAddress mkIPv4(uint32_t value) {
    return { true, { value } };
}

IPAddress mkIPv6(const uint8_t (&value)[16]) {
    IPAddress out = { false };
    std::copy(std::begin(value), std::end(value), out.ipv6);
    return out;
}

And we can show an address:

std::string showIPAddress(const IPAddress& ip) {
    IPAddressVisitor<std::string> visitor = {
        [](uint32_t v) {
            return std::format("{}.{}.{}.{}",
                               (v >> 24) & 0xFF, (v >> 16) & 0xFF,
                               (v >> 8) & 0xFF, v & 0xFF);
        },
        [](const uint8_t (&v)[16]) {
            return std::format("{:02X}{:02X}:{:02X}{:02X}:{:02X}{:02X}:{:02X}{:02X}:"
                               "{:02X}{:02X}:{:02X}{:02X}:{:02X}{:02X}:{:02X}{:02X}",
                               v[0], v[1], v[2], v[3], v[4], v[5], v[6], v[7],
                               v[8], v[9], v[10], v[11], v[12], v[13], v[14], v[15]);
        }
    };
    return acceptIPAddress(ip, visitor);
}

Note that in this way, the compiler enforces that we handle every branch. And, if we ever add a new branch, everything that ever consumes IPAddress with an IPAddressVisitor will have to add a new handler.

In a language without generics or powerful enough polymorphism, it’s difficult to enforce the “pure” visitor pattern because you can’t ensure that all branches return the same type.

One common pattern is to have an “effectful” visitor pattern, where the point isn’t to return something, but to execute something on the payload of the present branch. This is pretty effective for languages like C, javascript, python, etc. where types aren’t really a rigid thing.

For example, this might be how you treat an “implicit nullable”:

export const visitMaybe = (visitNothing, visitJust, val) =>
  (val == null) ? visitNothing() : visitJust(val);

This is basically for_ from Haskell: You can do something like conditionally launch some action if the value is present.

visitMaybe(
  () => console.log("Nothing to request"),
  (reqPayload) => makeRequest("google.com", reqPayload),
  maybeRequest
);

On a simpler note, if your language as subtyping built in (maybe with classes and subclasses) or some other form of dynamic dispatch, you can implement it in terms of that, which is nice in python, java, C++, etc.

interface ExprVisitor<R> {
    R visitLit(int value);
    R visitNegate(Expr unary);
    R visitAdd(Expr left, Expr right);
    R visitMul(Expr left, Expr right);
}

abstract class Expr {
    public abstract <R> R accept(ExprVisitor<R> visitor);
}

Alternatively, you’re in a language where lambdas are easy, instead of tupling up the visitor, you could just have accept itself take a number of arguments corresponding to each constructor:

// Alternative definition without an explicit Visitor class
abstract class Expr {
    public abstract <R> R accept(
        Function<int,R> visitLit,
        Function<Expr,R> visitNegate,
        BiFunction<Expr,Expr,R> visitAdd,
        BiFunction<Expr,Expr,R> visitMul
    );
}

(Note that C++ doesn’t allow template virtual methods — not because it’s not possible within the language semantics and syntax, but rather because the maintainers are too lazy to add it — so doing this faithfully requires a bit more creativity)

Now, if your language has dynamic dispatch or subclass polymorphism, you can actually do a different encoding, instead of the tagged union. This will work in languages that don’t allow or fully support naked union types, too. In this method, each constructor becomes a class, but it’s important to only allow access using accept to properly enforce the sum type pattern.

class Lit extends Expr {
    private final int value;

    public Lit(int value) {
        this.value = value;
    }

    @Override
    public <R> R accept(ExprVisitor<R> visitor) {
        return visitor.visitLit(value);
    }
}

class Negate extends Expr {
    private final Expr unary;

    public Negate(Expr unary) { this.unary = unary; }

    @Override
    public <R> R accept(ExprVisitor<R> visitor) {
        return visitor.visitNegate(unary);
    }
}

class Add extends Expr {
    private final Expr left;
    private final Expr right;

    public Add(Expr left, Expr right) {
        this.left = left;
        this.right = right;
    }

    @Override
    public <R> R accept(ExprVisitor<R> visitor) {
        return visitor.visitAdd(left, right);
    }
}

class Mul extends Expr {
    private final Expr left;
    private final Expr right;

    public Mul(Expr left, Expr right) {
        this.left = left;
        this.right = right;
    }

    @Override
    public <R> R accept(ExprVisitor<R> visitor) {
        return visitor.visitMul(left, right);
    }
}

(But, just wanted to note that if you actually are working in java, you can actually do something with sealed classes, which allows exhaustiveness checking for its native switch/case statements.)

Alternatively you could make all of the subclasses anonymous and expose them as factory methods, if your language allows it:

abstract class Expr {
    public abstract <R> R accept(ExprVisitor<R> visitor);

    public static Expr lit(int value) {
        return new Expr() {
            @Override
            public <R> R accept(ExprVisitor<R> visitor) {
                return visitor.visitLit(value);
            }
        };
    }

    public static Expr negate(Expr unary) {
        return new Expr() {
            @Override
            public <R> R accept(ExprVisitor<R> visitor) {
                return visitor.visitNegate(unary);
            }
        };
    }

    public static Expr add(Expr left, Expr right) {
        return new Expr() {
            @Override
            public <R> R accept(ExprVisitor<R> visitor) {
                return visitor.visitAdd(left, right);
            }
        };
    }

    // ... etc
}

You’d then call using:

public class Main {
    public static void main(String[] args) {
        Expr expr = new Mul(new Negate(new Add(new Lit(4), new Lit(5))), new Lit(8));
        // or
        // Expr expr = Eval.mul(Eval.negate(Eval.add(Eval.lit(4), Eval.lit(5))), Eval.lit(8));

        ExprVisitor<Integer> eval = new ExprVisitor<>() {
            @Override public Integer visitLit(int value) {
                return value;
            }
            @Override public Integer visitNegate(Expr unary) {
                return -unary.accept(this);
            }
            @Override public Integer visitAdd(Expr left, Expr right) {
                return left.accept(this) + right.accept(this);
            }
            @Override public Integer visitMul(Expr left, Expr right) {
                return left.accept(this) * right.accept(this);
            }
        };

        System.out.println("Result: " + expr.accept(eval));
    }
}

Passing around function references like this is actually pretty close to the scott encoding of our data type — and for non-recursive types, it’s essentially the church encoding.

Recursive Types

Speaking of recursive types…what if your language doesn’t allow recursive data types? What if it doesn’t allow recursion at all, or what if recursively generated values are just annoying to deal with? Just imagine writing that Expr type in a language with explicit memory management, for example. Or, what if you wanted a way to express your recursive types in a more elegant and runtime-safe manner?

One thing you can instead do is have your visitor be in its “catamorphism”, or church encoding. Instead of having the “visitor” take the recursive sub-values, instead have it return the result of recursively applying itself.

Let’s do this in dhall, one of the most famous non-recursive languages. Dhall does have native sum types, so we won’t worry about manually writing a visitor pattern. But it does not have recursive data types.

Let’s define a type like:

data Expr = Lit Natural
          | Add Expr Expr
          | Mul Expr Expr

But we can’t define data types in dhall that refer to themselves. So instead, we can define them in their “church encoding”: give what you would do with an Expr to consume it, where the consumption function is given as if it were recursively applied.

let ExprF : Type -> Type
      = \(r : Type) ->
        { lit : Natural -> r
        , add    : r -> r -> r
        , mul    : r -> r -> r
        }

let Expr : Type
      = forall (r : Type) -> ExprF r -> r

Note that ExprF r is essentially ExprVisitor<R>, except instead of add being Expr -> Expr -> r, it’s r -> r -> r: the input values aren’t the expression, but rather the results of recursively folding on the expression. In fact, our original non-recursive ExprVisitor<R> (to be more precise, the R accept(ExprVisitor<R>)) is often called the “scott encoding”, as opposed to the recursive “church encoding” fold.

For value creation, you take the visitor and recursively apply:

let lit : Natural -> Expr
      = \(x : Natural) ->
        \(r : Type) ->
        \(handlers : ExprF r) ->
            handlers.lit x

let add : Expr -> Expr -> Expr
      = \(left : Expr) ->
        \(right : Expr) ->
        \(r : Type) ->
        \(handlers : ExprF r) ->
            handlers.add (left r handlers) (right r handlers)

let mul : Expr -> Expr -> Expr
      = \(left : Expr) ->
        \(right : Expr) ->
        \(r : Type) ->
        \(handlers : ExprF r) ->
            handlers.mul (left r handlers) (right r handlers)

And finally, using the data type involves providing the handler to fold up from the bottom to top. Note that add : \(left : Natural) -> \(right : Natural) -> left + right already assumes that the handler has been applied to the sub-expressions, so you get Naturals on both sides instead of Expr.

let eval : Expr -> Natural
      = \(e : Expr) ->
          e Natural
            { lit = \(x : Natural) -> x
            , add = \(left : Natural) -> \(right : Natural) -> left + right
            , mul = \(left : Natural) -> \(right : Natural) -> left * right
            }

let testVal : Expr
      = mul (add (lit 4) (lit 5)) (lit 8)

in  assert : eval testVal === 72

This pattern is useful even in languages with good datatype recursion, like Haskell — it’s actually the recursion-schemes refactoring of a recursive data type, and it can be useful to have it live alongside your normal recursive types. I’ve written this blog post talking about how useful this pattern is to have alongside your normal recursive types.

This pattern is pretty portable to other languages too, as long as you can scrounge together something like Rank-N types:

interface ExprFold<R> {
    R foldLit(int value);
    R foldNegate(R unary);
    R foldAdd(R left, R right);
    R foldMul(R left, R right);
}

interface Expr {
    public abstract <R> R accept(ExprFold<R> fold);

    public static Expr lit(int value) {
        return new Expr() {
            @Override
            public <R> R accept(ExprFold<R> fold) {
                return fold.foldLit(value);
            }
        };
    }

    public static Expr negate(Expr unary) {
        return new Expr() {
            @Override
            public <R> R accept(ExprFold<R> fold) {
                return fold.foldNegate(unary.accept(fold));
            }
        };
    }

    // etc.
}

By “Rank-N types” here, I mean that your objects can generate polymorphic functions: given an Expr, you could generate an <R> R accept(ExprFold <R> fold) for any R, and not something pre-determined or pre-chosen by your choice of representation of Expr.

Generalized Algebraic Data Types

You’ve implemented ADTs in your language of choice, or you are currently in a language with native ADTs. Life is good, right? Until that sneaky voice starts whispering in your hear: “we need more type safety.” You resist that urge, maybe even get a lot done without it, but eventually you are compelled to give in and embrace the warm yet harsh embrace of ultimate type safety. Now what?

Singletons and Witnesses

In Haskell, singletons are essentially enums used to associate a value with a reifiable type. “Reifiable” here means that you can take the runtime value of a singleton and use it to bring evidence to the type-level. I ran into a real-world usage of this while writing https://coronavirus.jle.im/, a web-based data visualizer of COVID-19 data (source here) in purescript. I needed a singleton to represent scales for scatter plots and linking them to the data that can be plotted. And, not only did it need to be type-safe in purescript (which has ADTs but not GADTs), it had to be type-safe in the javascript ffi as well.

Here’s how it might look in Haskell:

-- | Numeric types
data NType :: Type -> Type where
    NInt :: NType Int
    NDouble :: NType Double
    NPercent :: NType Percent

-- | Define a scale
data Scale :: Type -> Type where
    ScaleDate :: Scale Date
    ScaleLinear :: Bool -> NType a -> Scale a   -- ^ whether to include zero in the axis or not
    ScaleLog :: NType a -> Scale a

You’d then run it like this:

plot :: Scale a -> Scale b -> [(a, b)] -> Canvas

So, we have the type of the input tuples being determined by the values you pass to plot:

ghci> :t plot ScaleDate (ScaleLinear True (LNumeric NInt))
[(Date, Int)] -> Canvas

But let’s say we only had ADTs. And then we’re passing them down to a javascript FFI which only has structs and functions. We could drop the type-safety and instead error on runtime, but…no. Type unsafety is not acceptable.

The fundamental ability we want to gain is that if we pattern match on ScaleDate, then we know a has to be Date. If we match on NInt, we know that a has to be Int.

For the sake of this example, we’re going to be implementing a simpler function in purescript and in javascript: a function that takes a scale type and a list of points prints the bounds. In Haskell, this looks like:

data AxisBounds a = AB
    { minValue :: a
    , minLabel :: String
    , maxValue :: a
    , maxLabel :: String
    }

displayAxis :: Scale a -> [a] -> AxisBounds a
displayAxis = \case
    ScaleDate -> \xs ->
      let xMin = minimum xs
          xMax = maximum xs
       in AB xMin (showDate xMin) xMax (showDate xMax)
    ScaleLinear hasZero nt -> \xs ->
      displayNumericAxis (if hasZero then 0:xs else xs)
    ScaleLog nt ->
      displayNumericAxis nt xs

displayNumericAxis :: NType a -> [a] -> AxisBounds a
displayNumericAxis = \case
    NInt -> \xs ->
      let xMin = minimum xs
          xMax = maximum xs
       in AB xMin (printf "%d" xMin) xMax (printf "%d" xMax)
    NDouble -> \xs ->
      let xMin = minimum xs
          xMax = maximum xs
       in AB xMin (printf "%.4f" xMin) xMax (printf "%.4f" xMax)
    NPercent -> \xs ->
      let xMin = minimum xs
          xMax = maximum xs
       in AB xMin (printf "%.1f%%" (xMin*100)) xMax (printf "%.1f%%" (xMax*100))

(Pretend the Percent type is just a newtype-wrapped Float or something)

There are at least two main approaches to do this. We’ll be discussing runtime equality witnesses and Higher-Kinded Eliminators.

Runtime Witnesses and Coyoneda Embedding

The Yoneda Lemma is one of the most powerful tools that Category Theory has yielded as a branch of math, but its sibling coyoneda is one of the most useful Haskell abstractions.

This doesn’t give you GADTs, but it’s a very lightweight way to “downgrade” your GADTs into normal GADTs which is appropriate if you don’t need the full power.

The trick is this: if you have MyGADT a, and you know you are going to be using it to produce as, you can do a covariant coyoneda transform.

For example, if you have this type representing potential data sources:

data Source :: Type -> Type where
    ByteSource :: Handle -> Source Word
    StringSource :: FilePath -> Source String

readByte :: Handle -> IO Word
readString :: FilePath -> IO String

readSource :: Source a -> IO a
readSource = \case
    ByteSource h -> readByte h
    StringSource fp -> readString fp

You could instead turn Source into a non-GADT by making it a normal parameterized ADT and adding a X -> a field, which is a type of CPS transformation:

data Source a =
    ByteSource Handle (Word -> a)
  | StringSource FilePath (String -> a)

byteSource :: Handle -> Source Word
byteSource h = ByteSource h id

stringSource :: FilePath -> Source String
stringSource fp = StringSource fp id

readSource :: Source a -> IO a
readSource = \case
    ByteSource h out -> out <$> readByte h
    StringSource fp out -> out <$> readString fp

A nice benefit of this method is that Source can now have a Functor instance, which the original GADT could not.

And, if MyGADT a is going to be consuming as, you can do the contravariant coyoneda transform:

data Sink a =
    ByteSink Handle (a -> Word)
  | StringSink FilePath (a -> String)

This gives it a free Contravariant instance too!

And, if you are going to be both consuming and producing as, you can do the invariant coyoneda transform

data Interface a =
    ByteInterface Handle (Word -> a) (a -> Word)
  | StringInterface FilePath (String -> a) (Word -> a)

However, in practice, true equality involves being able to lift under injective type constructors, and carrying every single continuation is unwieldy. We can package them up together with a runtime equality witness.

This is something we can put “inside” NInt such that, when we pattern match on a NType a, the type system can be assured that a is an Int.

You need some sort of data of type IsEq a b with functions:

• refl :: IsEq a a
• to :: IsEq a b -> a -> b
• sym :: IsEq a b -> IsEq b a
• trans :: IsEq a b -> IsEq b c -> IsEq a c
• inj :: IsEq (f a) (f b) -> IsEq a b

If you have to and sym you also get from :: IsEq a b -> b -> a.

From all of this, we can recover our original IsEq a Word -> Word -> a and IsEq a Word -> a -> Word functions, saving us from having to put two functions.

Your language of choice might already have this IsEq. But one of the more interesting ways to me is Leibniz equality (discussed a lot in this Ryan Scott post), which works in languages with higher-kinded polymorphism. Leibniz quality in languages with higher-kinded polymorphism means that a and b are equal if forall p. p a -> p b: any property of a is also true of b.

In Haskell, we write this like:

newtype Leibniz a b = Leibniz (forall p. p a -> p b)

refl :: Leibniz a a
refl = Leibniz id

The only possible way to construct a ‘Leibniz’ is with both type parameters being the same: You can only ever create a value of type Leibniz a a, never a value of Leibniz a b where b is not a.

You can prove that this is actually equality by writing functions Leibniz a b -> Leibniz b a and Leibniz a b -> Leibniz b c -> Leibniz a c (this Ryan Scott post goes over it well), but in practice we realize this equality by safely coercing a and b back and forth:

newtype Identity a = Identity { runIdentity :: a }

to :: Leibniz a b -> a -> b
to (Leibniz f) = runIdentity . f . Identity

newtype Op a b = Op { getOp :: b -> a }

from :: Leibniz a b -> b -> a
from (Leibniz f) = getOp (f (Op id))

So, if your language supports higher-kinded Rank-2 types, you have a solution!

There are other solutions in other languages, but they will usually all be language-dependent.

Let’s write everything in purescript. The key difference is we use map (to isNumber) :: Array a -> Array Number, etc., to get our Array as something we know it has the type of.

import Text.Printf

newtype Leibniz a b = Leibniz (forall p. p a -> p b)

to :: Leibniz a b -> a -> b
from :: Leibniz a b -> b -> a

data NType a =
    NInt (Leibniz a Int)
  | NNumber (Leibniz a Number)
  | NPercent (Leibniz a Percent)

type AxisBounds a =
    { minValue :: a
    , minLabel :: String
    , maxValue :: a
    , maxLabel :: String
    }

displayNumericAxis :: NType a -> Array a -> AxisBounds a
displayNumericAxis = \case
    NInt isInt -> \xs ->
      let xMin = minimum $ map (to isInt) xs
          xMax = maximum $ map (to isInt) xs
          showInt = show
       in { minValue: xMin
          , minLabel: showInt xMin
          , maxValue: xMax
          , maxLabel: showInt xMax
          }
    NNumber isNumber -> \xs ->
      let xMin = minimum $ map (to isNumber) xs
          xMax = maximum $ map (to isNumber) xs
          showFloat = printf (Proxy :: Proxy "%.4f")   -- it works a little differently
       in { minValue: xMin
          , minLabel: showFloat xMin
          , maxValue: xMax
          , maxLabel: showFloat xMax
          }
    NPercent isPercent -> \xs ->
      let xMin = minimum $ map (to isPercent) xs
          xMax = maximum $ map (to isPercent) xs
          showPercent = printf (Proxy :: Proxy "%.1f%%") <<< (_ * 100.0)
       in { minValue: xMin
          , minLabel: showPercent xMin
          , maxValue: xMax
          , maxLabel: showPercent xMax
          }

To work with our [a] as if it were [Int], we have to map the coercion function over it that our Leibniz a Int gave us. Admittedly, this naive way adds a runtime cost of copying the array. But we could be more creative with finding the minimum and maximum in this way in constant space and no extra allocations.

And, if we wanted to outsource this to the javascript FFI, remember that javascript doesn’t quite have sum types, so we can create a quick visitor:

type NVisitor a r =
    { nvInt :: Leibniz a Int -> r
    , nvNumber :: Leibniz a Number -> r
    , nvPercent :: Leibniz a Percent -> r
    }

type NAccept a = forall r. NVisitor a r -> r

toAccept :: NType a -> NAccept a
toAccept = case _ of
    NInt isInt -> \nv -> nv.nvInt isInt
    NNumber isNumber -> \nv -> nv.nvNumber isNumber
    NPercent isPercent -> \nv -> nv.nvPercent isPercent

foreign import _formatNumeric :: forall a. Fn2 (NAccept a) a String

formatNumeric :: NType a -> a -> String
formatNumeric nt = runFn2 _formatNumeric (toAccept nt)

The FFI binding looks like: (taken from my actual source code)

import * as d3 from "d3-format";

export const _formatNumeric = (naccept, xs) =>
  naccept(
    { nvInt: (isInt) => d3.format("~s")
    , nvNumber: (isNumber) => d3.format(".3~s")
    , nvPercent: (isPercent) => d3.format("+.3~p")
    }
  );

Admittedly in the javascript we are throwing away the “GADT type safety” because we throw away the equality. But we take what we can — we at least retain the visitor pattern for sum-type type safety and exhaustiveness checking. I haven’t done this in typescript yet so there might be a way to formalize Leibniz equality to do this in typescript and keep the whole chain type-safe from top to bottom.

Higher-Kinded Eliminators

This is essentially the higher-kinded version of the visitor pattern, except in dependent type theory these visitors are more often called “eliminators” or destructors, which is definitely a cooler name.

In the normal visitor you’d have:

data User = TheAdmin | Member Int

data UserHandler r = UH
    { uhTheAdmin :: r
    , uhMember :: Int -> r
    }

But note that if you have the right set of continuations, you have something that is essentially equal to User without having to actually use User:

type User' = forall r. UserHandler r -> r

fromUser :: User -> User'
fromUser = \case
    TheAdmin -> \UH{..} -> uhTheAdmin
    Member userId -> \UH{..} -> uhMember userId

toUser :: User' -> Foo
toUser f = f $ UH { fhTheAdmin = TheAdmin, fhMember = Member }

This means that User is actually equivalent to forall r. UserHandler r -> r: they’re the same type, so if your language doesn’t have sum types, you could encode it as forall r. UserHandler r -> r instead. Visitors, baby.

But, then, what actually does the r type variable represent here, semantically? Well, in a UserHandler r, r is the “target” that we interpret into. But there’s a deeper relationship between r and User: A UserHandler r essentially “embeds” a User into an r. And, a UserHandler r -> r is the application of that embedding to an actual User.

If we pick r ~ (), then UserHandler () embeds User into (). If we pick r ~ String, then UserHandler () embeds User into String (like, “showing” it). And if we pick r ~ User, a UserHandler User embeds a User into…itself?

So here, r is essentially the projection that we view the user through. And by making sure we are forall r. UserHandler r -> r for all r, we ensure that we do not lose any information: the embedding is completely 1-to-1. It lets you “create” the User faithfully in a “polymorphic” way.

In fact, to hammer this home, some people like to use the name of the type as the type variable: UserHandler user:

-- | The same thing as before but with things renamed to prove a point
data MakeUser user = MakeUser
    { uhTheAdmin :: user
    , uhMember :: Int -> user
    }

type User' = forall user. MakeUser user -> user

The forall user. lets us faithfully “create” a User within the system we have, without actually having a User data type. Essentially we can imagine the r in the forall r as “standing in” for User, even if that type doesn’t actually exist.

Now, here’s the breakthrough: If we can use forall (r :: Type) to substitute for User :: Type, how about we use a forall (p :: Type -> Type) to substitute for a Scale :: Type -> Type?

data Scale :: Type -> Type where
    ScaleDate :: Scale Date
    ScaleLinear :: Bool -> LType a -> Scale a
    ScaleLog :: NType a -> Scale a

data ScaleHandler p a = SH
    { shDate :: p Date
    , shLinear :: Bool -> NType a -> p a
    , shLog :: NType a -> p a
    }

type Scale' a = forall p. ScaleHandler p a -> p a

fromScale :: Scale a -> Scale' a
fromScale = \case
    ScaleDate -> \SH{..} -> shDate
    ScaleLinear hasZero lt -> \SH{..} -> shLinear hasZero lt
    ScaleLog nt -> \SH{..} -> shLog nt

toScale :: Scale' a -> Scale a
toScale f = f $ SH { shDate = ScaleDate, shLinear = ScaleLinear, shLog = ScaleLog }

So in our new system, forall p. ScaleHandler p a -> p a is identical to Scale: we can use p a to substitute in Scale in our language even if our language itself cannot support GADTs.

So let’s write formatNType in purescript. We no longer have an actual Scale sum type, but its higher-kinded church encoding:

type NType a = forall p.
    { int :: p Int
    , number :: p Number
    , percent :: p Percent
    } -> p a

type Scale a = forall p.
    { date :: p Date
    , linear :: Bool -> NType a -> p a
    , log :: NType a -> p a
    } -> p a

ntInt :: NType Int
ntInt nth = nth.int

ntNumber :: NType Number
ntNumber nth = nth.number

ntPercent :: NType Percent
ntPercent nth = nth.percent

formatNType :: NType a -> a -> String
formatNType nt = f
  where
    Op f = nt
      { int: Op show
      , number: Op $ printf (Proxy "%.4f")
      , percent: Op $ printf (Proxy "%.1f%%") <<< (_ * 100.0)
      }

Here we are using

newtype Op b a = Op (a -> b)

as our “target”: turning an NType a into an Op String a. And an Op String a is an a -> String, which is what we wanted! The int field is Op String Int, the number field is Op String Number, etc.

In many languages, using this technique effectively requires having a newtype wrapper on-hand, so it might be unwieldy in non-trivial situations. For example, if we wanted to write our previous axis function which is NType a -> [a] -> String, we’d have to have a newtype wrapper for [a] -> String that has a as its argument:

newtype OpList b a = Op ([a] -> b)

or you could re-use Compose:

newtype Compose f g a = Compose (f (g a))

and your p projection type would be Compose Op []. So, you don’t necessarily have to write a bespoke newtype wrapper, but you do have to devote some brain cycles to think it through (unless you’re in a language that doesn’t need newtype wrappers to have this work, like we’ll discuss later).

By the way, this method generalizes well to multiple arguments: if you have a type like MyGADT a b c, you just need to project into a forall (p :: k1 -> k2 -> k3 -> Type).

I believe I have read somewhere that the two methods discussed here (runtime equality witness vs. higher-kinded eliminator) are not actually fully identical in their power, and there are GADTs where one would work and not the other … but I can’t remember where I read this and I’m also not big-brained enough to figure out what those situations are. But if you, reader, have any idea, please let me know!

Existential Types

Let’s take a quick break to talk about something that’s not technically related to GADTs but is often used alongside them.

What if we wanted to store a value with its NType and hide the type variable? In Haskell we’d write this like:

data NType :: Type -> Type where
    NInt :: NType Int
    NDouble :: NType Double
    NPercent :: NType Percent

data SomeNType = forall a. SomeNType (NType a) a

formatNType :: NType a -> a -> String
formatNType nt x = ...

formatSomeNType :: SomeNType -> String
formatSomeNType (SomeNType nt x) = formatNType nt x

myFavoriteNumbers :: [SomeNType]
myFavoriteNumbers = [SomeNType NInt 3, SomeNType NDouble pi]

But what if our language doesn’t have existentials? Remember, this is basically a value SomeNType that isn’t a Generic, but contains both a NType a and an a of the same variable.

One strategy we have available is to CPS-transform our existentials into their CPS form (continuation-passing style form). Basically, we write exactly what we want to do with our contents if we pattern matched on them. It’s essentially a Rank-N visitor pattern with only a single constructor:

type SomeNType = forall r. (forall a. NType a -> a -> r) -> r

someNType :: NType a -> a -> SomeNType
someNType nt x = \f -> f nt x

formatSomeNumeric :: SomeNType -> String
formatSomeNumeric snt = snt
    \nt x -> formatNumeric nt x

You can imagine, syntactically, that snt acts as its “own” pattern match, except instead of matching on SomeNType nt x -> .., you “match” on \nt x -> ..

This general pattern works for languages with traditional generics like Java too:

interface SomeNTypeVisitor<R> {
    <A> R visit(NType<A> nt, A val);
}

interface SomeNType {
    public abstract <R> R accept(SomeNTypeVisitor<R> visitor);

    // One option: the factory method
    public static <A> SomeNType someNType(NType<A> nt, A val) {
        return new SomeNType() {
            @Override
            public <R> R accept(SomeNTypeVisitor<R> visitor) {
                return visitor.visit(nt, val);
            }
        };
    }
}

// Second option: the subtype hiding a type variable, which you have to always
// make sure to upcast into `SomeNType` after creating
class SomeNTypeImpl<A> extends SomeNType {
    private NType<A> nt;
    private A val;

    public SomeNTypeImpl(NType<A> nt, A val) {
        this.nt = nt;
        this.val = val;
    }

    @Override
    public <R> R accept(SomeNTypeVisitor<R> visitor) {
        return visitor.visit(nt, val);
    }
}

Does…anyone write java like this? I tried committing this once while at Google and I got automatically flagged to be put on a PIP.

Recursive GADTs

The climax of this discussion: what if your language does not support GADTs or recursive data types?

We’re going to be using dhall as an example again, but note that the lessons applied here are potentially useful even when you do have recursive types: we’re going to be talking about a higher-kinded church encoding, which can be a useful form of your data types that live alongside your normal recursive ones.

Let’s imagine Expr as a GADT, where Expr a represents an Expr that evaluates to an a:

data Expr :: Type -> Type where
    NatLit :: Natural -> Expr Natural
    BoolLit :: Bool -> Expr Bool
    Add :: Expr Natural -> Expr Natural -> Expr Natural
    LTE :: Expr Natural -> Expr Natural -> Expr Bool
    Ternary :: Expr Bool -> Expr a -> Expr a -> Expr a

eval :: Expr a -> a
eval = \case
    NatLit n -> n
    BoolLit b -> b
    Add x y -> eval x + eval y
    LTE a b -> eval a <= eval b
    Ternary b x y -> if eval b then eval x else eval y

Adding this type variable ensures that our Expr is type-safe: it’s impossible to Add an Expr Bool, and the two branches of a Ternary must have the same result type, etc. And, we can write eval :: Expr a -> a and know exactly what type will be returned.

Now, let’s combine the two concepts: First, the church encoding, where our handlers take the “final result” of our fold r instead of the recursive value Expr. Second, the higher-kinded eliminator pattern where we embed Expr :: Type -> Type into forall (p :: Type -> Type).

And finally, we get:3

let ExprF =
      \(p : Type -> Type) ->
        { natLit : Natural -> p Natural
        , boolLit : Bool -> p Bool
        , add : p Natural -> p Natural -> p Natural
        , ternary : forall (a : Type) -> p Bool -> p a -> p a -> p a
        }

let Expr
    : Type -> Type
    = \(a : Type) -> forall (p : Type -> Type) -> ExprF p -> p a

let eval
    : forall (a : Type) -> Expr a -> a
    = \(a : Type) ->
      \(e : Expr a) ->
        e
          (\(q : Type) -> q)
          { natLit = \(x : Natural) -> x
          , boolLit = \(x : Bool) -> x
          , add = \(x : Natural) -> \(y : Natural) -> x + y
          , ternary =
              \(a : Type) ->
              \(b : Bool) ->
              \(x : a) ->
              \(y : a) ->
                if b then x else y
          }

Again, now instead of add taking Expr, it takes p Natural: the “Natural result of the fold”. p not only stands in for what we embed Expr into, it stands in for the result of the recursive fold. That’s why in eval, the first arguments of add are the Natural results of the sub-evaluation.

These values can be created in the same way as before, merging the two techniques, sending the handlers downstream:

let natLit
    : Natural -> Expr Natural
    = \(n : Natural) ->
      \(p : Type -> Type) ->
      \(handlers : ExprF p) ->
        handlers.natLit n

let boolLit
    : Bool -> Expr Bool
    = \(n : Bool) ->
      \(p : Type -> Type) ->
      \(handlers : ExprF p) ->
        handlers.boolLit n

let add
    : Expr Natural -> Expr Natural -> Expr Natural
    = \(x : Expr Natural) ->
      \(y : Expr Natural) ->
      \(p : Type -> Type) ->
      \(handlers : ExprF p) ->
        handlers.add (x p handlers) (y p handlers)

let ternary
    : forall (a : Type) -> Expr Bool -> Expr a -> Expr a -> Expr a
    = \(a : Type) ->
      \(b : Expr Bool) ->
      \(x : Expr a) ->
      \(y : Expr a) ->
      \(p : Type -> Type) ->
      \(handlers : ExprF p) ->
        handlers.ternary (b p handlers) (x p handlers) (y p handlers)

let testVal
    : Expr Natural
    = add (natLit 5) (add (natLit 6) (natLit 7))

in  assert : eval testVal === 18

If all of this is difficult to parse, try reviewing both the recursive ADT section and the higher-kinded eliminator section and making sure you understand both well before tackling this, which combines them together!

Admittedly in Haskell (and purescript) this is a lot simpler because we don’t have to explicitly pass in type variables:

data ExprF p = ExprF
    { natLit :: Natural -> p Natural
    , boolLit :: Bool -> p Bool
    , add :: p Natural -> p Natural -> p Natural
    , ternary :: forall a.  p Bool -> p a -> p a -> p a
    }

type Expr a = forall p. ExprF p a -> p a

eval :: Expr a -> a
eval e = runIdentity $
  e
    { natLit = Identity
    , boolLit = Identity
    , add = \(Identity x) -> \(Identity y) -> Identity (x + y)
    , ternary = \(Identity b) -> \(Identity x) -> \(Identity y) -> if b then x else y
    }

ternary :: Expr Bool -> Expr a -> Expr a -> Expr a
ternary b x y handlers = handlers.ternary (b handlers) (x handlers) (y handlers)

But one nice thing about the dhall version that’s incidental to dhall is that it doesn’t require any extra newtype wrappers like the Haskell one does. That’s because type inference tends to choke on things like this, but dhall doesn’t really have any type inference: all of the types are passed explicitly. It’s one of the facts about dhall that make it nice for things like this.

Congratulations

In any case, if you’ve made it this far, congratulations! You are a master of ADTs and GADTs. Admittedly every language is different, and some of these solutions have to be tweaked for the language in question. And, if your program gets very complicated, there is a good chance that things will become ergonomically unfeasible.

But I hope, at least, that this inspires your imagination to try to bring your haskell principles, techniques, standards, practices, and brainrot into the language of your choice (or language you are forced to work with).

And, if you ever find interesting ways to bring these things into a language not discussed here (or a new interesting technique or pattern), I would absolutely love to hear about it!

Until next time, happy “Haskelling”!

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

---

1. I bet you thought there was going be some sort of caveat in this footnote, didn’t you?↩︎

2. I didn’t think I’d ever write “java bean” non-ironically on my blog, but there’s a first time for everything.↩︎

3. Be aware that this implementation is not necessarily appropriately lazy or short-circuiting in Ternary: it might evaluate both sides returning the chosen branch.↩︎

There’s yet again been a bit of functional programming-adjacent twitter drama recently, but it’s actually sort of touched into some subtleties about sum types that I am asked about (and think about) a lot nowadays. So, I’d like to take this opportunity to talk a bit about the “why” and nature of sum types and how to use them effectively, and how they contrast with other related concepts in programming and software development and when even cases where sum types aren’t the best option.

Sum Types at their Best

The quintessential sum type that you just can’t live without is Maybe, now adopted in a lot of languages as Optional:

data Maybe a = Nothing | Just a

If you have a value of type Maybe Int, it means that its valid values are Nothing, Just 0, Just 1, etc.

This is also a good illustration to why we call it a “sum” type: if a has n possible values, then Maybe a has 1 + n: we add the single new value Nothing to it.

The “benefit” of the sum type is illustrated pretty clearly here too: every time you use a value of type Maybe Int, you are forced to consider the fact that it could be Nothing:

showMaybeInt :: Maybe Int -> String
showMaybeInt = \case
  Nothing -> "There's nothing here"
  Just i -> "Something is here: " <> show i

That’s because usually in sum type implementations, they are implemented in a way that forces you to handle each case exhaustively. Otherwise, sum types are much less useful.

At the most fundamental level, this behaves like a compiler-enforced null check, but built within the language in user-space instead being compiler magic, ad-hoc syntax1, or static analysis — and the fact that it can live in user-space is why it’s been adopted so widely. At a higher level, functional abstractions like Functor, Applicative, Monad, Foldable, Traversable allow you to use a Maybe a like just a normal a with the appropriate semantics, but that’s a topic for another time (like 2014).

This power is very special to me on a personal level. I remember many years ago on my first major haskell project changing a type from String to Maybe String, and then GHC telling me every place in the codebase where something needed to change in order for things to work still. Coming from dynamically typed languages in the past, this sublime experience truly altered my brain chemistry and Haskell-pilled me for the rest of my life. I still remember the exact moment, what coffee shop I was at, what my order was, the weather that day … it was truly the first day of the rest of my life.

It should be noted that I don’t consider sum types a “language feature” or a compiler feature as much as I’d consider it a design pattern. Languages that don’t have sum types built-in can usually implement them using typed unions and an abstract visitor pattern interface (more on that later). Of course, having a way to “check” your code before running it (like with a type system or statically verified type annotations) does make a lot of the features much more useful.

Anyway, this basic pattern can be extended to include more error information in your Nothing branch, which is how you get the Either e a type in the Haskell standard library, or the Result<T,E> type in rust.

Along different lines, we have the common use case of defining syntax trees:

data Expr =
    Lit Int
  | Negate Expr
  | Add Expr Expr
  | Sub Expr Expr
  | Mul Expr Expr

eval :: Expr -> Int
eval = \case
    Lit i -> i
    Negate x -> -(eval x)
    Add x y -> eval x + eval y
    Sub x y -> eval x - eval y
    Mul x y -> eval x * eval y

pretty :: Expr -> String
pretty = go 0
  where
    wrap :: Int -> Int -> String -> String
    wrap prio opPrec s
      | prio > opPrec = "(" <> s <> ")"
      | otherwise = s
    go prio = \case
        Lit i -> show i
        Negate x -> wrap prio 2 $ "-" <> go 2 x
        Add x y -> wrap prio 0 $ go 0 x <> " + " <> go 1 y
        Sub x y -> wrap prio 0 $ go 0 x <> " - " <> go 1 y
        Mul x y -> wrap prio 1 $ go 1 x <> " * " <> go 2 y

main :: IO ()
main = do
    putStrLn $ pretty myExpr
    print $ eval myExpr
  where
    myExpr = Mul (Negate (Add (Lit 4) (Lit 5))) (Lit 8)

-(4 + 5) * 8
-72

Now, if we add a new command to the sum type, the compiler enforces us to handle it.

data Expr =
    Lit Int
  | Negate Expr
  | Add Expr Expr
  | Sub Expr Expr
  | Mul Expr Expr
  | Abs Expr

eval :: Expr -> Int
eval = \case
    Lit i -> i
    Negate x -> -(eval x)
    Add x y -> eval x + eval y
    Sub x y -> eval x - eval y
    Mul x y -> eval x * eval y
    Abs x -> abs (eval x)

pretty :: Expr -> String
pretty = go 0
  where
    wrap :: Int -> Int -> String -> String
    wrap prio opPrec s
      | prio > opPrec = "(" <> s <> ")"
      | otherwise = s
    go prio = \case
        Lit i -> show i
        Negate x -> wrap prio 2 $ "-" <> go 2 x
        Add x y -> wrap prio 0 $ go 0 x <> " + " <> go 1 y
        Sub x y -> wrap prio 0 $ go 0 x <> " - " <> go 1 y
        Mul x y -> wrap prio 1 $ go 1 x <> " * " <> go 2 y
        Abs x -> wrap prio 2 $ "|" <> go 0 x <> "|"

Another example where things shine are as clearly-fined APIs between processes. For example, we can imagine a “command” type that sends different types of commands with different payloads. This can be interpreted as perhaps the result of parsing command line arguments or the message in some communication protocol.

For example, you could have a protocol that launches and controls processes:

data Command a =
    Launch String (Int -> a)    -- ^ takes a name, returns a process ID
  | Stop Int (Bool -> a)        -- ^ takes a process ID, returns success/failure

launch :: String -> Command Int
launch nm = Launch nm id

stop :: Int -> Command Bool
stop pid = Stop pid id

This ADT is written in the “interpreter” pattern (used often with things like free monad), where any arguments not involving a are the command payload, any X -> a represent that the command could respond with X.

Let’s write a sample interpreter backing the state in an IntMap in an IORef:

import qualified Data.IntMap as IM
import Data.IntMap (IntMap)

runCommand :: IORef (IntMap String) -> Command a -> IO a
runCommand ref = \case
    Launch newName next -> do
        currMap <- readIORef ref
        let newId = case IM.lookupMax currMap of
              Nothing -> 0
              Just (i, _) -> i + 1
        modifyIORef ref $ IM.insert newId newName
        pure (next newId)
    Stop procId next -> do
        existed <- IM.member procId <$> readIORef ref
        modifyIORef ref $ IM.delete procId
        pure (next existed)

main :: IO ()
main = do
    ref <- newIORef IM.empty
    aliceId <- runCommand ref $ launch "alice"
    putStrLn $ "Launched alice with ID " <> show aliceId
    bobId <- runCommand ref $ launch "bob"
    putStrLn $ "Launched bob with ID " <> show bobId
    success <- runCommand ref $ stop aliceId
    putStrLn $
      if success
        then "alice succesfully stopped"
        else "alice unsuccesfully stopped"
    print =<< readIORef ref

Launched alice with ID 0
Launched bob with ID 1
alice succesfully stopped
fromList [(1, "bob")]

Let’s add a command to “query” a process id for its current status:

data Command a =
    Launch String (Int -> a)    -- ^ takes a name, returns a process ID
  | Stop Int (Bool -> a)        -- ^ takes a process ID, returns success/failure
  | Query Int (String -> a)     -- ^ takes a process ID, returns a status message

query :: Int -> Command String
query pid = Query pid id

runCommand :: IORef (IntMap String) -> Command a -> IO a
runCommand ref = \case
    -- ...
    Query procId next -> do
        procName <- IM.lookup procId <$> readIORef ref
        pure case procName of
          Nothing -> "This process doesn't exist, silly."
          Just n -> "Process " <> n <> " chugging along..."

Relationship with Unions

To clarify a common confusion: sum types can be described as “tagged unions”: you have a tag to indicate which branch you are on (which can be case-matched on), and then the rest of your data is conditionally present.

In many languages this can be implemented under the hood as a struct with a tag and a union of data, along with some abstract visitor pattern interface to ensure exhaustiveness.

Remember, it’s not exactly a union, because, ie, consider a type like:

data Entity = User Int | Post Int

An Entity here could represent a user at a user id, or a post at a post id. If we considered it purely as a union of Int and Int:

union Entity {
    int user_id;
    int post_id;
};

we’d lose the ability to branch on whether or not we have a user or an int. If we have the tagged union, we recover the original tagged union semantics:

struct Entity {
    bool is_user;
    union {
        int user_id;
        int post_id;
    } payload;
};

Of course, you still need an abstract interface like the visitor pattern to actually be able to use this as a sum type with guarantees that you handle every branch, but that’s a story for another day. Alternatively, if your language supports dynamic dispatch nicely, that’s another underlying implementation that would work to back a higher-level visitor pattern interface.

Subtypes Solve a Different Problem

Now, sum types aren’t exactly a part of common programming education curriculum, but subtypes and supertypes definitely were drilled into every CS student’s brain and waking nightmares from their first year.

Informally (a la Liskov), B is a subtype of A (and A is a supertype of B) if anywhere that expects an A, you could also provide a B.

In normal object-oriented programming, this often shows up in early lessons as Cat and Dog being subclasses of an Animal class, or Square and Circle being subclasses of a Shape class.

When people first learn about sum types, there is a tendency to understand them as similar to subtyping. This is unfortunately understandable, since a lot of introductions to sum types often start with something like

-- | Bad Sum Type Example!
data Shape = Circle Double | Rectangle Double Double

While there are situations where this might be a good sum type (ie, for an API specification or a state machine), on face-value this is a bad example on the sum types vs. subtyping distinction.

You might notice the essential “tension” of the sum type: you declare all of your options up-front, the functions that consume your value are open and declared ad-hoc. And, if you add new options, all of the consuming functions must be adjusted.

So, subtypes (and supertypes) are more effective when they lean into the opposite end: the universe of possible options are open and declared ad-hoc, but the consuming functions are closed. And, if you add new functions, all of the members must be adjusted.

In typed languages with a concept of “objects” and “classes”, subtyping is often implemented using inheritance and interfaces.

interface Widget {
    void draw();
    void handleEvent(String event);
    String getName();
}

class Button implements Widget {
    // ..
}

class InputField implements Widget {
    // ..
}

class Box implements Widget {
    // ..
}

So, a function like processWidget(Widget widget) that expects a Widget would be able to be passed a Button or InputField or Box. And, if you had a container like List<Widget>, you could assemble a structure using Button, InputField, and Box. A perfect Liskov storm.

In typical library design, you’re able to add new implementations of Widget as an open universe easily: anyone that imports Widget can, and they can now use it with functions taking Widgets. But, if you ever wanted to add new functionality to the Widget interface, that would be a breaking change to all downstream implementations.

However, this implementation of subtyping, while prevalent, is the most mind-numbly boring realization of the concept, and it pained my soul to even spend time talking about it. So let’s jump into the more interesting way that subtype and supertype relationships manifest in the only language where anything is interesting: Haskell.

Subtyping via Parametric Polymorphism

In Haskell, subtyping is implemented in terms of parametric polymorphism and sometimes typeclasses. This allows for us to work nicely with the concept of functions and APIs as subtypes and supertypes of each other.

For example, let’s look at a function that takes indexers and applies them:

sumAtLocs :: ([Double] -> Int -> Double) -> [Double] -> Double
sumAtLocs ixer xs = ixer xs 1 + ixer xs 2 * ixer xs 3

ghci> sumAtLocs (!!) [1,2,3,4,5]
14

So, what functions could you pass to sumAtLocs? Can you only pass [Double] -> Int -> Double?

Well, not quite. Look at the above where we passed (!!), which has type forall a. [a] -> Int -> a!

In fact, what other types could we pass? Here are some examples:

fun1 :: [a] -> Int -> a
fun1 = (!!)

fun2 :: [a] -> Int -> a
fun2 xs i = reverse xs !! i

fun3 :: (Foldable t, Floating a) => t a -> Int -> a
fun3 xs i = if length xs > i then xs !! i else pi

fun4 :: Num a => [a] -> Int -> a
fun4 xs i = sum (take i xs)

fun5 :: (Integral b, Num c) => a -> b -> c
fun5 xs i = fromIntegral i

fun5 :: (Foldable t, Fractional a, Integral b) => t a -> b -> a
fun5 xs i = sum xs / fromIntegral i

fun5 :: (Foldable t, Integral b, Floating a) => t a -> b -> a
fun5 xs i = logBase (fromIntegral i) (sum xs)

What’s going on here? Well, the function expects a [Double] -> Int -> Double, but there are a lot of other types that could be passed instead.

At first this might seem like meaningless semantics or trickery, but it’s deeper than that: remember that each of the above types actually has a very different meaning and different possible behaviors!

1. forall a. [a] -> Int -> a means that the a must come from the given list. In fact, any function with that type is guaranteed to be partial: if you pass it an empty list, there is no a available to use.
2. forall a. Num a => [a] -> Int -> a means that the result might actually come from outside of the list: the implementation could always return 0 or 1, even if the list is empty. It also guarantees that it will only add, subtract, multiply, or abs: it will never divide.
3. forall a. Fractional a => [a] -> Int -> a means that we could possibly do division on the result, but we can’t do anything “floating” like square rooting or logarithms.
4. forall a. Floating a => [a] -> Int -> a means that we can possibly start square rooting or taking the logarithms of our input numbers
5. [Double] -> Int -> Double gives us the least guarantees about the behavior: the result could come from thin air (and not be a part of the list), and we can even inspect the machine representation of our inputs.

So, we have all of these types with completely different semantics and meanings. And yet, they can all be passed to something expecting a [Double] -> Int -> Double. That means that they are all subtypes of [Double] -> Int -> Double! [Double] -> Int -> Double is a supertype that houses multitudes of possible values, uniting all of the possible values and semantics into one big supertype.

Through the power of parametric polymorphism and typeclasses, you can actually create an extensible hierarchy of supertypes, not just of subtypes.

Consider a common API for json serialization. You could have multiple functions that serialize into JSON:

fooToJson :: Foo -> Value
barToJson :: Bar -> Value
bazToJson :: Baz -> Value

Through typeclasses, you can create:

toJSON :: ToJSON a => a -> Value

The type of toJSON :: forall a. JSON a => a -> Value is a subtype of Foo -> Value, Bar -> Value, and Baz -> Value, because everywhere you would want a Foo -> Value, you could give toJSON instead. Every time you want to serialize a Foo, you could use toJSON.

This usage works well, as it gives you an extensible abstraction to design code around. When you write code polymorphic over Monoid a, it forces you to reason about your values with respect to only the aspects relating to monoidness. If you write code polymorphic over Num a, it forces you to reason about your values only with respect to how they can be added, subtracted, negated, or multiplied, instead of having to worry about things like their machine representation.

The extensibility comes from the fact that you can create even more supertypes of forall a. ToJSON a => a -> Value easily, just by defining a new typeclass instance. So, if you need a MyType -> Value, you could make it a supertype of toJSON :: ToJSON a => a -> Value by defining an instance of the ToJSON typeclass, and now you have something you can use in its place.

Practically this is used by many libraries. For example, ad uses it for automatic differentiation: its diff function looks scary:

diff :: (forall s. AD s ForwardDouble -> AD s ForwardDouble) -> Double -> Double

But it relies on the fact that that (forall s. AD s ForwardDouble -> AD s ForwardDuble) is a superclass of (forall a. Floating a => a -> a), (forall a. Num a => a -> a), etc., so you can give it functions like \x -> x * x (which is a forall a. Num a => a -> a) and it will work as that AD s type:

ghci> diff (\x -> x * x) 10
20      -- 2*x

This “numeric overloading” method is used by libraries for GPU programming, as well, to accept numeric functions to be optimized and compiled to GPU code.

Another huge application is in the lens library, which uses subtyping to unite its hierarchy of optics.

For example, an Iso is a subtype of Traversal which is a subtype of Lens, and Lens is a supertype of Fold and Traversal, etc. In the end the system even allows you to use id from the Prelude as a lens or a traversal, because the type signature of id :: a -> a is actually a subtype of all of those types!

Subtyping using Existential Types

What more closely matches the spirit of subtypes in OOP and other languages is the existential type: a value that can be a value of any type matching some interface.

For example, let’s imagine a value that could be any instance of Num:

data SomeNum = forall a. Num a => SomeNum a

someNums :: [SomeNum]
someNums = [SomeNum (1 :: Int), SomeNum (pi :: Double), SomeNum (0xfe :: Word)]

This is somewhat equivalent to Java’s List<MyInterface> or List<MyClass>, or python’s List[MyClass].

Note that to use this effectively in Haskell with superclasses and subclasses, you need to manually wrap and unwrap:

data SomeFrational = forall a. Fractional a => SumFractional a

castUp :: SomeFractional -> SumNum
castUp (SomeFractional x) = SomeNum x

So, SomeNum is “technically” a supertype of SomeFractional: everywhere a SomeNum is expected, a SomeFractional can be given…but in Haskell it’s a lot less convenient because you have to explicitly cast.

In OOP languages, you can often cast “down” using runtime reflection (SomeNum -> Maybe SomeFractional). However, this is impossible in Haskell the way we have written it!

castDown :: SomeNum -> Maybe SomeFractional
castDown = error "impossible!"

That’s because of type erasure: Haskell does not (by default) couple a value at runtime with all of its associated interface implementations. When you create a value of type SomeNum, you are packing an untyped pointer to that value as well as a “dictionary” of all the functions you could use it with:

data NumDict a = NumDict
    { (+) :: a -> a -> a
    , (*) :: a -> a -> a
    , negate :: a -> a
    , abs :: a -> a
    , fromInteger :: Integer -> a
    }

mkNumDict :: Num a => NumDict a
mkNumDict = NumDict (+) (*) negate abs fromInteger

data FractionalDict a = FractionalDict
    { numDict :: NumDict a
    , (/) :: a -> a -> a
    , fromRational :: Rational -> a
    }

-- | Essentially equivalent to the previous 'SomeNum'
data SomeNum = forall a. SomeNum
    { numDict :: NumDict a
    , value :: a
    }

-- | Essentially equivalent to the previous 'SomeFractional'
data SomeFractional = forall a. SomeFractional
    { fractionalDict :: FractionalDict a
    , value :: a
    }

castUp :: SomeFractional -> SomeNum
castUp (SomeFractional (FractionalDict {numDict}) x) = SomeNum d x

castDown :: SomeNum -> Maybe SomeFractional
castDown (SomeNum nd x) = error "not possible!"

All of these function pointers essentially exist at runtime inside the SomeNum. So, SomeFractional can be “cast up” to SomeNum by simply dropping the FractionalDict. However, you cannot “cast down” from SomeNum because there is no way to materialize the FractionalDict: the association from type to instance is lost at runtime. OOP languages usually get around this by having the value itself hold pointers to all of its interface implementations at runtime. However, in Haskell, we have type erasure by default: there are no tables carried around at runtime.2

In the end, existential subtyping requires explicit wrapping/unwrapping instead of implicit or lightweight casting possible in OOP languages optimized around this sort of behavior.3 Existential-based subtyping is just less common in Haskell because parametric polymorphism offers a solution to most similar problems. For more on this topic, Simon Peyton Jones has a nice lecture on the topic.

The pattern of using existentially qualified data in a container (like [SomeNum]) is often called the “widget pattern” because it’s used in libraries like xmonad to allow extensible “widgets” stored alongside the methods used to manipualte them. It’s more common to explicitly store the handler functions (a “dictionary”) inside the type instead of of existential typeclasses, but sometimes it can be nice to let the compiler handle generating and passing your method tables implicitly for you. Using existential typeclasses instead of explicit dictionaries also allows you to bless certain methods and functions as “canonical” to your type, and the compiler will make sure they are always coherent.

I do mention in a blog post about different types of existential lists, however, that this “container of instances” type is much less useful in Haskell than in other languages for many reasons, including the up/downcasting issues mentioned above. In addition, Haskell gives you a whole wealth of functionality to operate over homogeneous parameters (like [a], where all items have the same type) that jumping to heterogeneous lists gives up so much.

Aside

Let’s briefly take a moment to talk about how typeclass hierarchies give us subtle subtype/supertype relationships.

Let’s look at the classic Num and Fractional:

class Num a

class Num a => Fractional a

Num is a superclass of Fractional, and Fractional is a subclass of Num. Everywhere a Num constraint is required, you can provide a Fractional constraint to do the same thing.

However, in these two types:

Num a => a
Fractional a => a

forall a. Num a => a is actually a subclass of forall a. Fractional a => a! That’s because if you need a forall a. Fractional a => a, you can provide a forall a. Num a => a instead. In fact, let’s look at three levels: Double, forall a. Fractional a => a, and forall a. Num a => a.

-- can be used as `Double`
1.0 :: Double
1.0 :: Fractional a => a
1 :: Num a => a

-- can be used as `forall a. Fractional a => a`
1.0 :: Fractional a => a
1 :: Num a => a

-- can be used as `forall a. Num a => a`
1 :: Num a => a

So, Double is a supertype of Fractional a => a is a supertype of Num a => a.

The general idea here is that the more super- you go, the more you “know” about the actual term you are creating. So, with Num a => a, you know the least (and, you have the most possible actual terms because there are more instances of Num than of Fractional). And, with Double, you know the most: you even know its machine representation!

So, Num is a superclass of Fractional but forall a. Num a => a is a subclass of forall a. Fractional a => a. This actually follows the typical rules of subtyping: if something appears on the “left” of an arrow (=> in this case), it gets flipped from sub- to super-. We often call the left side a “negative” (contravariant) position and the right side a “positive” position, because a negative of a negative (the left side of a left size, like a in (a -> b) -> c) is a positive.

Also note that our “existential wrappers”:

data SomeNum = forall a. Num a => SomeFractional a
data SomeFractional = forall a. Fractional a => SomeFractional a

can be CPS-transformed to their equivalent types:

type SomeNum' = forall r. (forall a. Num a => a -> r) -> r
type SomeFractional' = forall r. (forall a. Fractional a => a -> r) -> r

toSomeNum' :: SomeNum -> SomeNum'
toSomeNum' (SomeNum x) f = f x

toSomeNum :: SomeNum' -> SomeNum
toSomeNum sn = sn SomeNum

And in those cases, Num and Fractional again appear in the covariant (positive) position, since they’re the negative of negative. So, this aligns with our intuition that SomeFractional is a subtype of SomeNum.

The Expression Problem

This tension that I described earlier is closely related to the expression problem, and is a tension that is inherent to a lot of different aspects of language and abstraction design. However, in the context laid out in this post, it serves as a good general guide to decide what pattern to go down:

• If you expect a canonical set of “inhabitants” and an open set of “operations”, sum types can suit that end of the spectrum well.
• If you expect a canonical set of “operations” and an open set of “inhabitants”, consider subtyping and supertyping.

I don’t really think of the expression problem as a “problem” in the sense of “some hindrance to deal with”. Instead, I see it in the “math problem” sort of way: by adjusting how you approach things, you can play with the equation make the most out of what requirements you need in your design.

Looking Forward

A lot of frustration in Haskell (and programming in general) lies in trying to force abstraction and tools to work in a way they weren’t meant to. Hopefully this short run-down can help you avoid going against the point of these design patterns and start making the most of what they can offer. Happy Haskelling!

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

---

1. ?↩︎

2. Must OOP languages also have mechanisms for type erasure, but the default is unerased, which is opposite of Haskell.↩︎

3. Note that there are current GHC proposals that attempt to allow “naked” existentials without newtype wrappers, so we could actually get the same seamless and implicit up-casting as we would get in OOP languages. However, the jury is out on whether or not this is a good idea.↩︎