in Code — Entries

Extreme Haskell: Typed Expression EDSLs (Part 1)

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

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

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

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

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

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

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

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

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

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

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

The Lambda Calculus

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

A First Pass

One basic thing we can do is start with:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

This would properly evaluate:

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

We can also produce closures as values:

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

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

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

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

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

Type-Indexed Expressions

Just Add the Index

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

We can write lambdas in this system too:

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

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

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

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

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

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

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

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

Singletons and Existentials

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

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

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

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

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

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

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

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

Runtime Type Equality

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

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

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

With that, we can write sameTy:

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

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

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

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

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

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

instance TestEquality STy where
  testEquality = sameTy

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

But now at least we can write eval:

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

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

This does seem to work:

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

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

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

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

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

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

Pretty-Printing

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

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

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

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

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

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

And they render the same way:

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

Still Not Fully Verified

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

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

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

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

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

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

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

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

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

Typed Records and Sums

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

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

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

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

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

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

Record Access

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

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

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

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

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

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

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

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

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

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

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

Which is typed as:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Sum Injection and Case Analysis

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

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

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

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

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

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

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

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

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

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

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

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

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

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

And that’s exactly what a case statement is:

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

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

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

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

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

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

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

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

Runtime Equality for Records and Sums

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

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

instance TestEquality STy where
    testEquality = sameTy

instance TestEquality STyField where
    testEquality = sameField

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

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

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

The Full Eval

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

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

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

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

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

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

With that, we can write our full eval.

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

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

Ergonomics of Records and Sums

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Pretty-Printing Records and Sums

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

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

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

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

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

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

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

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

Capturing Variables

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

We’ll have:

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

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

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

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

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

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

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

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

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

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

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

And finally, our whole Expr:

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

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

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

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

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

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

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

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

Adding in our other -XRequiredTypeArguments helpers:

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

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

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

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

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

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

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

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

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

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

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

What we gained

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

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

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

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

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

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

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

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

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

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

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

Eval with a typed environment

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

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

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

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

And so we can finally write:

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

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

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

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

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

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

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

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

Pretty-Printing Scoped Expressions

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

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

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

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

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

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

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

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

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

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

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

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

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

The Next Step

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

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

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

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

One must imagine the stubborn typer happy.

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

A Note on AI Coding

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

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

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

Special Thanks

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

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

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

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

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

With a new age of software development coming, what does it even mean to write good, robust, correct code? It is long overdue to clarify the mindset we use to define “good” coding principles.

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

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

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

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

Mix-ups Are Inevitable

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

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

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

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

Explicit Tags

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

newtype Id = Id String

type SiteId = Id
type AppId = Id

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

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

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

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

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

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

And at that point it’s all over.

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

newtype SiteId = SiteId String
newtype AppId = AppId String

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

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

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

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

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

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

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

data Id a = Id { getId :: String }

data Site
data App

type SiteId = Id Site
type AppId = Id App

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

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

Type safety doesn’t necessarily mean inflexibility!

Phantom Powers

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

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

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

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

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

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

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

newtype DbConnection (a :: Env) = DbConnection Connection

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

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

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

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

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

Correct Representations

Semantic Phantoms

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

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

If I had a function like:

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

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

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

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

We can instead use the dimensional library:

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

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

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

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

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

The Billion-Dollar Mistake

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

There are examples:

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

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

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

There’s also CVE-2008-5077, because EVP_VerifyInit returns 0 for false, 1 for true, and -1 for error! So some OpenSSL code did a simple if-then-else check (result != 0) and treated error and true the same way. Whoops.

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

data VerifyResult = Success | Failure | Error

However, it’s not easy to make an “integer or not found” type in C or JavaScript without some sort of side-channel. Imagine if JavaScript’s String.indexOf() instead expected continuations on success and failure and became much less usable as a result:

unsafeIndexOf :: String -> String -> Int

-- vs.

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

All of this just to fake having actual sum types.

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

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

Returning Maybe or Option forces the caller to handle:

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

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

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

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

Unmarked Assumptions

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

There are the simple cases — consider a mean function:

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

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

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

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

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

Separate Processed Data

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

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

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

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

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

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

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

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

newtype Username = UnsafeUsername String
  deriving (Show, Eq)

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

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

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

Now saveUser and getUser are safe at the boundaries:

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

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

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

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

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

instance ToField Username where
  toField = toField . unUsername

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

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

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

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

Boolean Blindness

At the heart of it, the previous examples’ cardinal sin was “boolean blindness”. If we have a predicate like validUsername :: String -> Bool, we will branch on that Bool once and throw it away. Instead, by having a function like mkUsername :: String -> Maybe Username, we keep the proof alongside the value for the entire lifetime of the value. We basically pair the string with its proof forever, making them inseparable.

There was another example of such a thing earlier: instead of using null :: [a] -> Bool and gating a call to mean with null, we instead use nonEmpty :: [a] -> Maybe (NonEmpty a), and pass along the proof of non-emptiness alongside the value itself. And, for the rest of that list’s life, it will always be paired with its non-emptiness proof.

Embracing total depravity means always keeping these proofs together, with the witnesses bundled with the value itself, because if you don’t, someone is going to assume it exists when it doesn’t, or drop it unnecessarily.

Boolean blindness also has another facet, which is where Bool itself is not a semantically meaningful type. This is “semantic boolean blindness”.

The classic example is filter :: (a -> Bool) -> [a] -> [a]. It might sound silly until it happens to you, but it is pretty easy to mix up if True means “keep” or “discard”. After all, a “water filter” only lets water through, but a “profanity filter” only rejects profanity. Instead, how about mapMaybe :: (a -> Maybe b) -> [a] -> [b]? In that case, it is clear that Just results are kept, and the Nothing results are discarded.

Sometimes, the boolean is ambiguous as to what it means. You can sort of interpret the 1999 Mars Polar Lander crash this way. Its functions took a boolean based on the state of the legs:

deployThrusters :: Bool -> IO ()

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

data LegState = Extended | Retracted

deployThrusters :: LegState -> IO ()

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

Resource Cleanup

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

process :: Handle -> IO ()

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

A bunch of things could go wrong —

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

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

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

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

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

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

processAll :: [Handle] -> IO ()

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

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

processAll :: Map Username Handle -> IO ()

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

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

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

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

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

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

processAll :: Map Username Handle -> IO ()

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

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

import qualified Data.Map as M

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

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

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

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

Embracing Total Depravity

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

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

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

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

In the Age of Agentic Coding

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

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

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

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

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

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

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

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

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

And…not whatever this tweet is.

The Next Step

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

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

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

Special Thanks

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

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

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

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

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

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

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

The Baby Paradox in Haskell

Justin Le — Thu, 21 Aug 2025 15:36:28 UTC

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:

If everyone loves Baby, Baby must love baby. (instantiate axiom 1 with \(x = \text{Baby}\)).
If baby loves someone, that someone must be me. (axiom 2)
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:

Logical “and” corresponds to tupling (or records of values). If (a, b) is inhabited, it means that both a and b are inhabited.
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.
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.
Any type with a constructor is “true”: (), Bool, String, etc.; any type with no constructor (data Void) is “false” because it has no inhabitants.
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:¹

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:

First, we instantiated everybodyLovesBaby with x ~ baby, to get loves baby baby.
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.

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

Faking ADTs and GADTs in Languages That Shouldn't Have Them

Justin Le — Tue, 1 Apr 2025 17:29:41 UTC

Haskell is the world’s best programming language¹, 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 bean²):

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

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 bet you thought there was going be some sort of caveat in this footnote, didn’t you?↩︎
I didn’t think I’d ever write “java bean” non-ironically on my blog, but there’s a first time for everything.↩︎
Be aware that this implementation is not necessarily appropriately lazy or short-circuiting in Ternary: it might evaluate both sides returning the chosen branch.↩︎