GADTs and Type Families

Haskell's type system can express more than "this is a list of Int". This lesson is a short introduction to two widely used type-level features. You won't need them every day, but you'll meet them in libraries.

GADTs: constructors with precise types

With an ordinary data type, an expression evaluator must handle mistakes like adding a number to a boolean at runtime. A generalized algebraic data type (GADT) lets each constructor state exactly which type it produces, so ill-typed expressions can't even be built:

{-# LANGUAGE GADTs #-}

data Expr a where
  IntE :: Int -> Expr Int
  BoolE :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int
  If :: Expr Bool -> Expr a -> Expr a -> Expr a
  Equal :: Expr Int -> Expr Int -> Expr Bool

eval :: Expr a -> a
eval (IntE n) = n
eval (BoolE b) = b
eval (Add x y) = eval x + eval y
eval (If c t e) = if eval c then eval t else eval e
eval (Equal x y) = eval x == eval y

main :: IO ()
main = do
  let expr = If (Equal (Add (IntE 2) (IntE 3)) (IntE 5)) (IntE 100) (IntE 0)
  print (eval expr)
  print (eval (Equal (IntE 1) (IntE 2)))

100
False

• eval :: Expr a -> a returns an Int for integer expressions and a Bool for boolean ones — no wrapper type, no runtime type checks.
• Add (IntE 1) (BoolE True) is a compile-time error.
• When eval matches IntE n, GHC learns that a is Int in that equation. That's what makes GADTs more powerful than normal ADTs.

Type families: functions on types

A type family computes a type from other types:

{-# LANGUAGE TypeFamilies #-}

import qualified Data.Map as Map
import Data.Kind (Type)

class Container f where
  type Key f :: Type
  empty :: f v
  insert :: Key f -> v -> f v -> f v
  toPairs :: f v -> [(Key f, v)]

newtype Assoc v = Assoc [(String, v)]
newtype IntMap v = IntMap (Map.Map Int v)

instance Container Assoc where
  type Key Assoc = String
  empty = Assoc []
  insert k v (Assoc xs) = Assoc ((k, v) : xs)
  toPairs (Assoc xs) = xs

instance Container IntMap where
  type Key IntMap = Int
  empty = IntMap Map.empty
  insert k v (IntMap m) = IntMap (Map.insert k v m)
  toPairs (IntMap m) = Map.toList m

type family Elem c where
  Elem [e] = e
  Elem (Maybe e) = e

firstElem :: [e] -> Maybe (Elem [e])
firstElem [] = Nothing
firstElem (x : _) = Just x

main :: IO ()
main = do
  print (toPairs (insert "b" 2 (insert "a" 1 (empty :: Assoc Int))))
  print (toPairs (insert 2 "two" (insert 1 "one" (empty :: IntMap String))))
  print (firstElem "xyz")

[("b",2),("a",1)]
[(1,"one"),(2,"two")]
Just 'x'

• type Key f is an associated type: each instance says what its key type is.
• Elem is a closed type family: a type-level function defined by equations, like a normal function with pattern matching.

Where you'll see these

• Servant describes whole web APIs as types, using type-level strings and type families.
• Database libraries (Persistent, Beam, Opaleye) use them for type-safe queries.
• DataKinds lifts values to the type level, so types can carry units, states (Door 'Open), or vector lengths.

The rule of thumb: reach for these when they remove a whole class of runtime errors, not just because they're available.