Type Families and the Kind Tower
Base Camp's newtype trick — Age and UserId can't be mixed up — turns out to be the beginning of a much bigger idea: types that compute other types, checked entirely at compile time, with zero runtime cost.
The tower, one more rung up
Base Camp’s “Kinds: types of types” section already introduced the first two steps of a pattern this chapter climbs one rung higher. Every value has a type — 42 :: Int. Every type, in turn, has a kind — Int :: *, where * (pronounced “type”) is the kind of every ordinary, fully-applied type. Type constructors that still need an argument have more interesting kinds: Maybe :: * -> * says “give Maybe a type, get a type back.”
Figure: Each rung classifies the one below it. A type family lives among ordinary types — it’s still just a type, once fully applied — but it behaves like a function: computing a new type (or kind) from its arguments, entirely at compile time, with the same Bool -> Bool-style kind signature an ordinary type constructor would have.
That’s the whole tower: values are classified by types, types are classified by kinds. What’s new in this chapter is realizing that “type-level function” isn’t a contradiction — GHC lets you write functions whose inputs and outputs are themselves types, checked and fully resolved before your program ever runs.
DataKinds: promoting ordinary values to the type level
The DataKinds extension is the bridge that makes this practical: it takes an ordinary data declaration and promotes its constructors to live at the type level too, as members of a brand-new kind named after the type.
{-# LANGUAGE DataKinds, KindSignatures #-}
data Unit = Meters | Feet -- an ordinary type ...
-- ... whose constructors DataKinds also promotes to the type level,
-- as members of a new kind 'Unit', inhabited by the types 'Meters and 'Feet
newtype Length (u :: Unit) = Length Double
addLength :: Length u -> Length u -> Length u
addLength (Length a) (Length b) = Length (a + b)
Length is parameterized not by an ordinary type, but by a promoted value — 'Meters or 'Feet — living at the type level, purely as a compile-time tag. addLength’s type signature, Length u -> Length u -> Length u, forces both arguments to share the same u: adding a Length 'Meters to a Length 'Feet simply doesn’t typecheck. This is Base Camp’s UserId/Age newtype trick, generalized — instead of one fixed wrapper per unit, Length is a single type, parameterized by which unit, with the compiler tracking and enforcing the distinction automatically.
The ' before Meters (as in Length 'Meters) is optional in most contexts, but worth knowing about: it disambiguates a promoted data constructor (living at the type level) from an ordinary type sharing the same name — genuinely necessary when both a type and a promoted constructor could plausibly be spelled the same way. GHC will often infer the right one without it, but reaching for the tick when kinds get confusing is a cheap way to make the intent explicit.
Type families: functions that compute types
DataKinds gets values onto the type level; type families are what let you actually compute with them. A closed type family looks almost exactly like an ordinary function definition, just one level up:
{-# LANGUAGE TypeFamilies, DataKinds #-}
type family Not (b :: Bool) :: Bool where
Not 'True = 'False
Not 'False = 'True
Read this exactly like not :: Bool -> Bool’s equations — because structurally, it is the same thing, just operating on the promoted 'True/'False types from DataKinds instead of ordinary Bool values. Not 'True doesn’t run when your program runs; it’s resolved once, by GHC, while type-checking, and the result — 'False — is baked into the compiled code with no residual computation left over.
A more directly useful example: computing the result type of an operation from its inputs, rather than just enforcing that two inputs match.
type family Combine (u1 :: Unit) (u2 :: Unit) :: Unit where
Combine 'Meters 'Meters = 'Meters
Combine 'Feet 'Feet = 'Feet
-- deliberately no equation for mixed units: that case fails to typecheck
convert :: Length u1 -> Length u2 -> Length (Combine u1 u2) -> Length (Combine u1 u2)
Because Combine is a closed type family (all its equations are given together, right here), GHC knows it has seen every case — there’s no way to sneak in a “convert Meters and Feet and hope for the best” call, because Combine 'Meters 'Feet has no equation to reduce to, and the program simply fails to compile.
Type families come in two flavors: closed (all equations given together, as above — GHC can check exhaustiveness and even do some case-order reasoning) and open (equations can be added later, from other modules — used for things like associated types in typeclasses, where each instance contributes its own equation). Closed families are the right default when the full set of cases is known upfront; open families are what typeclasses with type-level configuration, like Element c mapping a container type to its element type, are built from.
GADTs: letting the return type vary by constructor
Ordinary data declarations (Base Camp) give every constructor the same return type — Circle and Rectangle both produce a Shape, no matter which one you use. Generalized Algebraic Data Types (GADTs) relax exactly that restriction, letting each constructor specify its own, more precise return type:
{-# LANGUAGE GADTs #-}
data Expr a where
IntLit :: Int -> Expr Int
BoolLit :: Bool -> Expr Bool
Add :: Expr Int -> Expr Int -> Expr Int
If :: Expr Bool -> Expr a -> Expr a -> Expr a
eval :: Expr a -> a
eval (IntLit n) = n
eval (BoolLit b) = b
eval (Add x y) = eval x + eval y
eval (If c t e) = if eval c then eval t else eval e
Expr a is a single type, but IntLit can only ever produce an Expr Int, and BoolLit only an Expr Bool — the constructor itself pins down a, something an ordinary data Expr = IntLit Int | BoolLit Bool | ... fundamentally cannot express, since every branch of an ordinary sum type shares one type. The payoff shows up immediately in eval: its return type is exactly a, meaning eval (IntLit 5) :: Int and eval (BoolLit True) :: Bool are tracked precisely, not both collapsed into some shared “value” type that would need a runtime check to interpret.
-- Add (BoolLit True) (IntLit 5) -- won't compile: Add demands Expr Int on both sides,
-- and BoolLit True :: Expr Bool
That last line is the entire point: an expression that adds a boolean to an integer is not merely a bug this evaluator would catch at runtime — it’s not a well-typed Expr at all, and GHC rejects it before eval is ever called.
GADTs are a genuine extension of what ordinary algebraic data types can express, but the underlying idea is still built on the same foundation Chapter 4 introduced: a constructor is a function, and its type signature is a promise. Ordinary data declarations just require every constructor’s promise to end in the same type; GADT syntax is simply Haskell letting you write that promise down explicitly, constructor by constructor, instead of inferring one shared conclusion for all of them.
Where this all lands: encoding an API’s shape as a type
The payoff for all of this — DataKinds, type families, and GADT-adjacent machinery working together — shows up dramatically in Servant, a library for building web APIs where the API’s entire shape lives in a type:
type UserAPI =
"users" :> Get '[JSON] [User]
:<|> "users" :> Capture "id" Int :> Get '[JSON] User
"users" here is a type-level string (a promoted Symbol, DataKinds’ cousin for strings rather than data constructors), and :> and :<|> are type-level operators describing “this URL segment, then this,” and “this route, or this other route.” UserAPI is not documentation about the API — it is the API’s shape, as far as the compiler is concerned, and Servant uses that type to generate the actual routing logic, client functions, and even API documentation automatically, all checked for consistency at compile time.
This “encode the specification as a type, let the compiler check everything against it” pattern shows up constantly once type families and DataKinds are second nature: persistent and esqueleto use it for database schemas (a malformed query fails to compile, not just to run), and fixed-vector/vector-sized use it to track array lengths in the type itself, catching out-of-bounds access before the program ever starts. None of these libraries invented new language features to do this — they’re all built from exactly the tower this chapter climbed.
The tower doesn’t stop here, either — full dependent types (where types can depend on runtime values, not just other types) are the next mountain range over, and Haskell’s singletons library is the closest thing to a bridge across, if this vantage point was the one that grabbed you the most.