Haskell GADT Pattern Matching
GADT pattern matching is matching that refines the result type in each branch. A Lit branch knows its result is Int and an IsZero branch knows its result is Bool.
One evaluator serves two result types
eval returns an Int for an Add expression. It returns a Bool for an IsZero expression.
{-# LANGUAGE GADTs #-}
data Expr a where
Lit :: Int -> Expr Int
Add :: Expr Int -> Expr Int -> Expr Int
IsZero :: Expr Int -> Expr Bool
eval :: Expr a -> a
eval (Lit n) = n
eval (Add x y) = eval x + eval y
eval (IsZero x) = eval x == 0
main :: IO ()
main = do
print (eval (Add (Lit 2) (Lit 3)))
print (eval (IsZero (Lit 0)))
Each result type gets its own function
intVal accepts an Expr Int value. boolVal accepts an Expr Bool value.
{-# LANGUAGE GADTs #-}
data Expr a where
Lit :: Int -> Expr Int
Add :: Expr Int -> Expr Int -> Expr Int
IsZero :: Expr Int -> Expr Bool
eval :: Expr a -> a
eval (Lit n) = n
eval (Add x y) = eval x + eval y
eval (IsZero x) = eval x == 0
intVal :: Expr Int -> Int
intVal e = eval e
boolVal :: Expr Bool -> Bool
boolVal e = eval e
main :: IO ()
main = do
print (intVal (Add (Lit 2) (Lit 3)))
print (boolVal (IsZero (Lit 0)))
Nested matching refines each level
The outer IsZero branch handles a Bool result. The inner Add branch handles an Int result.
{-# LANGUAGE GADTs #-}
data Expr a where
Lit :: Int -> Expr Int
Add :: Expr Int -> Expr Int -> Expr Int
IsZero :: Expr Int -> Expr Bool
eval :: Expr a -> a
eval (Lit n) = n
eval (Add x y) = eval x + eval y
eval (IsZero x) = eval x == 0
main :: IO ()
main = do
print (eval (IsZero (Add (Lit 1) (Lit (-1)))))
print (eval (IsZero (Add (Lit 3) (Lit 4))))
Example
{-# LANGUAGE GADTs #-}
data Expr a where
Lit :: Int -> Expr Int
Add :: Expr Int -> Expr Int -> Expr Int
IsZero :: Expr Int -> Expr Bool
eval :: Expr a -> a
eval (Lit n) = n
eval (Add x y) = eval x + eval y
eval (IsZero x) = eval x == 0
incInt :: Expr Int -> Int
incInt e = eval e + 1
main :: IO ()
main = do
print (incInt (Add (Lit 2) (Lit 3)))
print (eval (IsZero (Lit 0)))
Key points
- Refinement: matching a GADT constructor narrows the result type inside that branch.
- Lit branch: the Lit branch returns an integer because its result type is Int.
- IsZero branch: the IsZero branch returns a boolean because its result type is Bool.
- Evaluator type: eval has type Expr a to a so one function serves both result types.
- Nested match: matching inside a nested expression refines each level in turn.
In this example, incInt takes an Expr Int value, evaluates it, and adds 1 to the result. The main action prints the increased integer first and the evaluated boolean second.
Note
refinement happens at compile time and needs no runtime type test.
Try it Yourself
Edit the code, then press Run.
Running is simulated · Haskell Playground
Exercise
Inside the IsZero branch of eval, what is known about the result type?