Haskell GADTs Versus ADTs
A GADT differs from an ordinary algebraic data type in the result type of its constructors. A GADT constructor chooses its own result type and an ordinary constructor shares one result type.
Ordinary constructors share one result type
SInt and SBool both build a Simple value. simpleKind names the shape of each value.
data Simple = SInt Int | SBool Bool
simpleKind :: Simple -> String
simpleKind (SInt _) = "int"
simpleKind (SBool _) = "bool"
main :: IO ()
main = do
putStrLn (simpleKind (SInt 7))
putStrLn (simpleKind (SBool True))
GADT constructors choose their own result types
VInt builds a Val Int value. VBool builds a Val Bool value.
{-# LANGUAGE GADTs #-}
data Val a where
VInt :: Int -> Val Int
VBool :: Bool -> Val Bool
needInt :: Val Int -> Int
needInt (VInt n) = n
needBool :: Val Bool -> Bool
needBool (VBool b) = b
main :: IO ()
main = do
print (needInt (VInt 7))
print (needBool (VBool True))
An ordinary evaluator must encode a boolean answer
evalOld returns an Int for every OldExpr value. A zero test becomes 1 for True and 0 for False.
data OldExpr = OldLit Int | OldAdd OldExpr OldExpr | OldIsZero OldExpr
evalOld :: OldExpr -> Int
evalOld (OldLit n) = n
evalOld (OldAdd x y) = evalOld x + evalOld y
evalOld (OldIsZero x) = if evalOld x == 0 then 1 else 0
main :: IO ()
main = do
print (evalOld (OldIsZero (OldLit 0)))
print (evalOld (OldIsZero (OldLit 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
data OldExpr = OldLit Int | OldAdd OldExpr OldExpr | OldIsZero OldExpr
evalOld :: OldExpr -> Int
evalOld (OldLit n) = n
evalOld (OldAdd x y) = evalOld x + evalOld y
evalOld (OldIsZero x) = if evalOld x == 0 then 1 else 0
main :: IO ()
main = do
print (evalOld (OldIsZero (OldLit 0)))
print (eval (IsZero (Lit 0)))
Key points
- Shared result: every constructor of an ordinary data type returns the same result type.
- Chosen result: each constructor of a GADT returns the result type it chooses.
- Simple ADT: SInt and SBool both return the same Simple type.
- Encoded result: an ordinary evaluator must encode a boolean answer as a number.
- Exact result: a GADT evaluator returns the boolean answer directly.
In this example, evalOld encodes a zero test as the number 1 and eval returns the boolean True directly. The main action prints the ordinary encoded result first and the GADT exact result second.
Note
choose a GADT when constructors need different result types and choose an ordinary type otherwise.
Try it Yourself
Edit the code, then press Run.
Running is simulated · Haskell Playground
Exercise
Why can a GADT evaluator return True directly while an ordinary evaluator cannot?