GADTs.hs

{-# LANGUAGE GADTs #-}

import Numeric

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 n) = n
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq  e1 e2) = eval e1 == eval e2

data Bit = O | Z deriving Show

serialise :: Expr a -> [Bit]
serialise (I x) = foldl (\acc -> \e -> if e == '1' then O:acc else Z:acc) [] $ showIntAtBase 2 ("01" !!) x ""
serialise (B True) = [O]
serialise (B False) = [Z]
serialise (Add e1 e2) = serialise $ I ((eval e1) + (eval e2))
serialise (Mul e1 e2) = serialise $ I ((eval e1) * (eval e2))

main :: IO ()
main = do
  putStrLn . show $ eval (Add (I 32) (I 10))
  putStrLn . show $ eval (Add (Add (I 32) (I 10)) (I 33))
-- putStrLn . show $ eval (Eq (Add (B False) (B True)) (B False)) -- no longer allowed
-- putStrLn . show $ eval (Eq (Mul (B False) (B True)) (B False)) -- no longer allowed
  putStrLn . show $ eval (Eq (Add (I 32) (I 10)) (I 42))
  putStrLn . show $ eval (Eq (Add (I 33) (I 10)) (I 42))
  putStrLn . show $ serialise (Add (Add (I 33) (I 10)) (I 42))
  putStrLn . show $ serialise (Mul (Add (I 33) (I 10)) (I 42))