GADTs

GADTs let constructors specify refined return types, so pattern matching teaches the type checker facts ("in this branch, a ~ Int"). Uses: typed interpreters, protocols, state machines, well-typed ASTs.

{-# LANGUAGE GADTs, KindSignatures #-}

-- A type-safe expression language: ill-typed expressions can't be constructed
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
  Eq :: Expr Int -> Expr Int -> Expr Bool
  Pair :: Expr a -> Expr b -> Expr (a, b)
  Fst :: Expr (a, b) -> Expr a

eval :: Expr a -> a                  -- the return type is refined per constructor
eval (IntE n) = n
eval (BoolE b) = b
eval (Add a b) = eval a + eval b
eval (If c t e) = if eval c then eval t else eval e
eval (Eq a b) = eval a == eval b
eval (Pair a b) = (eval a, eval b)
eval (Fst p) = fst (eval p)

-- eval (If (Eq (IntE 1) (Add (IntE 0) (IntE 1))) (IntE 10) (IntE 20)) == 10
-- Add (IntE 1) (BoolE True)   -- rejected at compile time

-- Length-indexed vectors (with DataKinds, Module 38)
data Nat = Z | S Nat
data Vec (n :: Nat) a where
  VNil :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a

vhead :: Vec ('S n) a -> a           -- can only be called on non-empty vectors: total!
vhead (VCons x _) = x

vtail :: Vec ('S n) a -> Vec n a
vtail (VCons _ xs) = xs