GADT Code Samples

gadt1.hs

data Point = Pt Int Int
data Expr a = Number Integer | Boolean Bool

gadt2.hs

ghci> let a = Number 10
ghci> let b = Boolean True

ghci> :t a
a :: Expr

ghci> :t b
b :: Expr

gadt3.hs

ghci> :t Number
Number :: Integer -> Expr

ghci> :t Boolean
Boolean :: Bool -> Expr

gadt4.hs

data Expr = Number Int
          | Succ Expr
          | IsZero Expr
          | If Expr Expr Expr

data Value = IntVal Int | BoolVal Bool

eval :: Expr -> Value
eval (Number i) = IntVal i
eval (Succ e) = case eval e of
        IntVal i -> IntVal (i+1)
eval (IsZero e) = case eval e of
        IntVal i -> BoolVal (i==0)
eval (If b e1 e2) = case eval b of
        BoolVal True  -> eval e1
        BoolVal False -> eval e2

gadt5.hs

expr1 = Succ (Number 1)          -- valid and type checks
expr2 = Succ (IsZero (Number 1)) -- invalid but type checks

gadt6.hs

{-# LANGUAGE GADTs #-}

data Expr a where
  Number :: Int -> Expr Int
  Succ   :: Expr Int -> Expr Int
  IsZero :: Expr Int -> Expr Bool
  If     :: Expr Bool->Expr a->Expr a->Expr a

gadt7.hs

ghci> :t Succ (Number 10)
Succ (Number 10) :: Expr Int

ghci> :t Succ (IsZero (Number 0))
<interactive>:1:7: error:
     Couldn’t match type Bool with Int
      Expected type: Expr Int
        Actual type: Expr Bool
     In the first argument of Succ, namely (IsZero (Number 0))
      In the expression: Succ (IsZero (Number 0))

gadt8.hs

eval :: Expr a -> a
eval (Number i) = i
eval (Succ e) = 1 + eval e
eval (IsZero e) = 0 == eval e
eval (If b e1 e2) = if eval b then eval e1 else eval e2