GADTs evaluator example

Gadts.hs

{-# LANGUAGE GADTs #-}

module Gadt where

import Data.Monoid

data Expr a where
    EI :: Int -> Expr Int
    EB :: Bool -> Expr Bool
    Plus :: Expr Int -> Expr Int -> Expr Int
    If :: Expr Bool -> Expr a -> Expr a -> Expr a

data Val a where
    VI :: Int -> Val Int
    VB :: Bool -> Val Bool

instance Show (Val a) where
    show (VI i) = "VI " ++ show i
    show (VB b) = "VB " ++ show b

example = If (EB True) (EI 1) (EI 2)

eval :: Expr a -> Val a
eval (EI i) = VI i
eval (EB b) = VB b
eval (Plus l r) =
    let (VI i) = eval l
        (VI j) = eval r
    in VI (i + j)
eval (If p t e) =
    let (VB b) = eval p
    in if b then eval t else eval e