GADTs

Source: https://en.wikibooks.org/wiki/Haskell/GADT

Allows you to explicitly write down the data constructors thus enabling you to constrain (type level guarantee) the return types.

Embeds the smart constructor type logic of phantom types into the data constructors of a type

Running Example

(from https://en.wikibooks.org/wiki/Haskell/GADT)

AST Using Normal Data Type

#!haskell

data Expr = I Int         -- integer constants
          | Add Expr Expr -- add two expressions
          | Mul Expr Expr -- multiply two expressions
          deriving Show

eval :: Expr -> Int
eval (I n)       = n
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2

(5+1) x 7 would be represented as:

#!bash
>> (I 5 `Add` I 1) `Mul` I 7 :: Expr.

Extending the language

Now, imagine that we would like to extend our language with other types than just integers. For instance, let's say we want to represent equality tests, so we need booleans as well. We augment the Expr type to become:

#!haskell

data Expr = I Int
          | B Bool           -- boolean constants
          | Add Expr Expr
          | Mul Expr Expr
          | Eq  Expr Expr    -- equality test

5+1 == 7 would be represented as:

#!bash
>> (I 5 `Add` I 1) `Eq` I 7.

eval has issues

#!haskell
eval :: Expr -> Either Int Bool
eval (I n) = Left n
eval (B b) = Right b

will not type check:

#!haskell
eval (Add e1 e2) = eval e1 + eval e2  --

can represent illegal states:

#!haskell
B True `Add` I 5 :: Expr

would have to add another layer in return type to represent failure:

#!haskell
eval :: Expr -> Maybe (Either Int Bool)
eval = ...

Now, we could write this function just fine, but that would still be unsatisfactory, because what we really want to do is to have Haskell's type system rule out any invalid expressions; we don't want to check types ourselves while deconstructing the abstract syntax tree.

Interim Step - Phantom Type

#!haskell
data Expr a = I Int
            | B Bool
            | Add (Expr a) (Expr a)
            | Mul (Expr a) (Expr a)
            | Eq  (Expr a) (Expr a)

Note that an expression Expr a does not contain a value a at all; that's why a is called a phantom type, it's just a dummy variable. Compare that with, say, a list [a] which does contain a bunch of as.

The key idea is that we're going to use a to track the type of the expression for us. Instead of making the constructor available to users of our small language, we are only going to provide a smart constructor with a more restricted type

#!haskell
add :: Expr Int -> Expr Int -> Expr Int
add = Add

All add does is constrain the type of expression to an Int so the following would not type check.

#!haskell
i :: Int  -> Expr Int
i = I

b :: Bool -> Expr Bool
b = B

b True `add` i 5

eval is implemented as before

#!haskell
eval (I n) = n

But there is still a problem

At the type level there is nothing preventing any of the following (although users could be shielded by only exposing smart constructors).

The following would type check

#!haskell
I 5 :: Expr Bool
I 5 :: Expr String

What we need is a way to constrain the return types of the constructors themselves, and that's exactly what generalized data types do.

IE. Move the smart constructor type logic into the data constructors

GADTs

#!haskell
data Expr a where
    I   :: Int  -> Expr Int
    B   :: Bool -> Expr Bool
    Add :: Expr Int -> Expr Int -> Expr Int
    Mul :: Expr Int -> Expr Int -> Expr Int
    Eq  :: Eq a => Expr a -> Expr a -> Expr Bool

eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq  e1 e2) = eval e1 == eval e2

So now the following would not type check:

#!haskell
demo2 = eval $ Mul (I 5) (B False)

#!bash
src\GADTs.hs:23:27-33: error:
    * Couldn't match type `Bool' with `Int'
      Expected type: Expr Int
        Actual type: Expr Bool
    * In the second argument of `Mul', namely `(B False)'
      In the second argument of `($)', namely `Mul (I 5) (B False)'
      In the expression: eval $ Mul (I 5) (B False)
   |
23 | demo2 = eval $ Mul (I 5) (B False)