Learn

GADTs (Generalized Algebraic Data Types) let constructors return a more specific type than the family. Phantom types parameterize types without storing values. Together they enable powerful type-level programming. Real World Haskell touches GADTs; serious type-driven Haskell code uses them.

Phantom types

newtype Tagged tag a = Tagged { unTagged :: a }

-- Tagged Int Email is different from Tagged Int Username,
-- but both are just Int at runtime

The tag parameter is a phantom — it appears in the type but not in any constructor. Pure type-level marker.

data Validated
data Unvalidated

newtype Email s = Email String

validate :: Email Unvalidated -> Maybe (Email Validated)
validate (Email s)
    | '@' `elem` s = Just (Email s)
    | otherwise = Nothing

sendMail :: Email Validated -> IO ()
sendMail = ...

Now sendMail ONLY accepts validated emails — the type system enforces it. You can't pass an unvalidated Email to sendMail; you have to call validate first.

Classic pattern: state machines / workflows where each step changes the type tag.

GADTs syntax

Enable with {-# LANGUAGE GADTs #-}. The new syntax:

{-# 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

Each constructor has its OWN return type — a specific instance of Expr. IntLit returns Expr Int; BoolLit returns Expr Bool. Adding two Expr Bool values is a TYPE ERROR.

Type-safe interpreter

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

The return type of eval depends on the constructor — the type system tracks that IntLit 5 :: Expr Int so eval (IntLit 5) :: Int. Statically guaranteed type safety in the AST.

When to use GADTs

• Embedding typed DSLs (like the expression language above)
• Type-safe state machines
• Recovering type info inside pattern matches
• Singleton types for type-level computation

Type families — relating types

For more complex type-level programming, GHC has type families:

{-# LANGUAGE TypeFamilies #-}

type family Result a where
    Result Int = String
    Result Bool = Int

Functions on types. Used in libraries like servant for type-level URL routing.

DataKinds and type-level data

{-# LANGUAGE DataKinds, KindSignatures #-}

data Status = Active | Pending | Closed

newtype Account (s :: Status) = Account { balance :: Int }

close :: Account 'Active -> Account 'Closed
close (Account b) = Account b

The Status data constructor names are PROMOTED to types via DataKinds. Now Account is parameterized by a type-level Status — Account 'Active and Account 'Closed are different types, can't be mixed.

Production Haskell uses these patterns sparingly — they're powerful but increase compilation time and code complexity. Reach for them when type safety wins justify the cost.

Common mistakes

• Reaching for GADTs without need — most code is fine with regular ADTs. Use GADTs when you genuinely need different return types per constructor.
• Phantom types without enforcement — if every function passes through arbitrary tags, the phantom isn't doing anything.
• DataKinds explosion — type-level state machines get complex fast. Keep them minimal.
• Skipping language extensions — GADTs, DataKinds, etc. all need {-# LANGUAGE #-} pragmas. Without, compile error.
• Mixing GADTs and regular ADTs in unfamiliar contexts — they have different match exhaustiveness rules.