Generalized Algebraic Datatypes (GADTs)
Overview
GADTs are a tool we can use to provide extra type information by matching on constructors. They use a slightly different syntax than normal Haskell data types.
GADTs allows you to explicitly write down the types of the constructor
The data constructor of GADTs can be thought of as a function returning type i.e. it is the type of type. In Haskell this is called #Kinds code:gadt.hs
data Maybe a = Nothing | Just a -- without GADTs
data Maybe a where -- with GADTs
Nothing :: Maybe a
Just :: a -> Maybe a
In a normal algebraic data type, data constructors are separated by |, but in GADTs, each data constructor is expressed like a function, and the last type concatenated with -> is the result type of the data constructor.
Example code
code:withoutGADT.hs
data Term a
= Lit a
| Succ (Term a)
| IsZero (Term a)
-- can't be well-typed :(
eval (Lit i) = i
eval (Succ t) = 1 + eval t
eval (IsZero i) = eval i == 0
Problems arise between the clash whether (a ~ Bool) or (a ~ Int) when trying to write the evaluator.
code:gadtExample.hs
module GADT where
data Term a where
Lit :: a -> Term a
Add :: Term Int -> Term Int -> Term Int
IsZero :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
eval :: Term a -> a
eval (Lit i) = i -- Term a
eval (Add a b) = eval a + eval b -- Term (a ~ Int)
eval (IsZero i) = eval i == 0 -- Term (a ~ Int)
eval (If b e1 e2) = if eval b then eval e1 else eval e2 -- Term (a ~ Bool)
example :: Int
example = eval $ If (Lit True) ((Lit 4) Add (Lit 10)) (Lit 3)
Using a GADT, we can express the type invariants for our language (i.e. only type-safe expressions are representable). Pattern matching on this GADTs then carries type equality constraints without the need for explicit tags.
Useful links