GADTs To Eliminate Runtime Checks

Type system help programmers ensure that the software they write behave correctly. They detect errors and also serve as documentation. A good type system allow abstracting domain specific concepts. Haskell’s much appreciated ADTs though powerful, is still lacking in few aspects. GADTs fill that gap.

This article explains GADTs with simple examples.

Algebraic Data Types (ADTs)

ADTs are composite types, i.e., types formed by combining other types. Depending on how the types are combined, we can have either a sum type or a product type.

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

In the example above Point and Expr are called type constructors and Pt, Number, and Boolean are called value constructors. If a type has more than one value constructor, they are called alternatives: one can use any of these alternatives to create a value of that type.

1ghci> let a = Number 10
2ghci> let b = Boolean True
3
4ghci> :t a
5a :: Expr
6
7ghci> :t b
8b :: Expr

Notice that the type of both a and b is Expr. This is because of the type of the value constructors.

1ghci> :t Number
2Number :: Integer -> Expr
3
4ghci> :t Boolean
5Boolean :: Bool -> Expr

To showcase how this complicates code, let us extend our type a bit and also add a expression evaluator.

 1data Expr = Number Int
 2          | Succ Expr
 3          | IsZero Expr
 4          | If Expr Expr Expr
 5
 6data Value = IntVal Int | BoolVal Bool
 7
 8eval :: Expr -> Value
 9eval (Number i) = IntVal i
10eval (Succ e) = case eval e of
11        IntVal i -> IntVal (i+1)
12eval (IsZero e) = case eval e of
13        IntVal i -> BoolVal (i==0)
14eval (If b e1 e2) = case eval b of
15        BoolVal True  -> eval e1
16        BoolVal False -> eval e2

If you notice carefully, this allows for some invalid expressions to type check successfully.

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

Also, notice how our eval function is partially implemented. We do not know what to evaluate a expression Succ (IsZero (Number 1)) to. We could allow the function to indicate error by using a Maybe or Either type, but that complicates the eval function further as we recursively call eval. Try it out for fun.

Generalised ADTs

The idea behind GADTs is to allow arbitrary return types for value constructors. They generalize ordinary data types. GADTs are provided in GHC as a language extension. We can enable this feature using the LANGUAGE pragma. It provides a new syntax for defining data types. We specify type for each value constructor. We can now redefine our Expr type like below:

1{-# LANGUAGE GADTs #-}
2
3data Expr a where
4  Number :: Int -> Expr Int
5  Succ   :: Expr Int -> Expr Int
6  IsZero :: Expr Int -> Expr Bool
7  If     :: Expr Bool -> Expr a -> Expr a -> Expr a

Notice that return type for value constructor can differ. This allows our program to be more strict. The value constructor Succ, for example, expects a Expr Int. The compiler can now reject code if you provide Expr Bool or anything else.

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

Now, with the refined Expr type, the evaluation of expression become simple. The expression evaluator need not worry about cases where the type do not match (ill-typed expression we saw earlier). The new evaluator is easy to write and read.

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

This version of eval is complete unlike the previously implemented one. If we are evaluating an expression, the expression is guaranteed to be valid and no failure cases are possible. Compile time guarantee is always better than a runtime check.