Haskell GADT Typed Expressions
A typed expression is an expression whose result type is recorded in its own type. Its constructors choose Int or Bool as the result.
Lit builds an integer expression
Lit 42 is an Expr Int value. eval returns 42.
{-# 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 = print (eval (Lit 42))
Add builds an integer expression from two parts
Add joins two Expr Int values. eval adds their results.
{-# 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 = print (eval (Add (Lit 2) (Lit 3)))
IsZero builds a boolean expression
IsZero tests one Expr Int value. eval returns True for zero and False otherwise.
{-# 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 (Lit 0)))
print (eval (IsZero (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
main :: IO ()
main = do
print (eval (Add (Lit 10) (Lit 5)))
print (eval (IsZero (Add (Lit 2) (Lit (-2)))))
Key points
- Typed expression: an expression whose result type appears in its type.
- Lit: Lit builds an Expr Int value from one integer.
- Add: Add builds an Expr Int value from two Expr Int values.
- IsZero: IsZero builds an Expr Bool value from one Expr Int value.
- Evaluator: eval returns the exact result type recorded by the expression.
In this example, Add joins 10 and 5 into one integer expression, and IsZero tests the sum of 2 and negative 2. The main action prints the integer result first and the boolean result second.
Note
an ordinary data type cannot give Lit, Add and IsZero different result types.
Try it Yourself
Edit the code, then press Run.
Running is simulated · Haskell Playground
Exercise
What is the type of IsZero (Lit 0)?