Catching DSL Type Errors at Compile Time with Haskell GADTs

The runtime crash you can prevent

You are building a small expression language—maybe a query builder or a configuration parser. With a standard algebraic data type, every node looks the same to the compiler:

data Expr = ILit Int | SLit String | Add Expr Expr

Nothing stops you from writing Add (SLit "hello") (ILit 1). The type checker accepts it because every branch is just Expr. The mistake surfaces later, when your interpreter pattern-matches on the wrong shape and crashes, or worse, silently produces garbage.

Generalized Algebraic Data Types (GADTs) move that failure from runtime to compile time.

What a GADT changes

A GADT lets each constructor declare its own return type. The type parameter stops being a vague label and becomes an index that the compiler tracks through pattern matching. The examples below assume a recent GHC release; the GADTs extension itself has been available for many years.

{-# LANGUAGE GADTs #-}

data Expr a where
  ILit :: Int    -> Expr Int
  SLit :: String -> Expr String
  Add  :: Expr Int -> Expr Int -> Expr Int

Now ILit produces an Expr Int and SLit produces an Expr String. When you pattern-match on an Add node, GHC refines the types of the arguments to Expr Int locally, so you cannot accidentally treat a string as an integer.

A typed evaluator

Because the type index is precise, the evaluator becomes total—every input has a well-typed result, and there are no partial functions or default error branches.

eval :: Expr a -> a
eval (ILit n)      = n
eval (SLit s)      = s
eval (Add e1 e2)   = eval e1 + eval e2

Try to compile Add (SLit "x") (ILit 1) and GHC rejects it before the program runs. The error message points at the constructor mismatch rather than a segfault three layers deep in your interpreter.

The cost: signatures and heterogeneous lists

GADTs are not free. Type signatures become more explicit, and if you need a list of expressions with different result types—say [Expr Int, Expr String]—you run into existential witnesses or rank-n types. A plain [Expr a] forces every element to share one a. You either wrap them in an existential type or restructure the problem.

Error messages can also be harder to read. When a deeply nested expression fails to typecheck, GHC may report a confusing mismatch involving type variables that are not written explicitly in your source. For teams unfamiliar with type theory, that raises the learning curve.

How to check the result

Save the definitions above in a file named Expr.hs. In a terminal, run:

ghci Expr.hs

Then evaluate a valid expression:

eval (Add (ILit 1) (ILit 2))

The expected result is 3. Next, try the invalid one:

eval (Add (SLit "x") (ILit 1))

GHC should reject the expression with a type error before evaluation. If you forget the {-# LANGUAGE GADTs #-} pragma, a parse error appears instead, so enable that extension first.

When to use them

Reach for GADTs when you are writing an interpreter, a type-safe query builder, or any DSL where invalid operations have a clear type-level meaning. Skip them for simple records or sum types where a plain ADT already gives you enough safety. The payoff is a compiler that rejects nonsensical programs; the price is more explicit types and steeper error messages.