GADTExpr

{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE StandaloneDeriving        #-}

module GADTExpr where

import Data.Function(on)
import Data.Ord(comparing)

class (Eq a, Ord a, Show a) => ExprType a where
    toExpr :: a -> Expr a

instance ExprType Bool where toExpr = Bin
instance ExprType Int  where toExpr = Num

data Expr a where
    Bin    :: Bool -> Expr Bool
    Num    :: Int  -> Expr Int

    (:+:)  :: Expr Int -> Expr Int -> Expr Int
    (:-:)  :: Expr Int -> Expr Int -> Expr Int

    (:=:)  :: ExprType a => Expr a -> Expr a -> Expr Bool
    (:<:)  :: ExprType a => Expr a -> Expr a -> Expr Bool

    (:/\:) :: Expr Bool -> Expr Bool -> Expr Bool
    (:\/:) :: Expr Bool -> Expr Bool -> Expr Bool

instance Eq  (Expr a) where (==) = (==) `on` show
instance Ord (Expr a) where compare = comparing show
deriving instance Show (Expr a)

eval :: ExprType a => Expr a -> Expr a
eval = toExpr . evalExpr

evalExpr :: ExprType a => Expr a -> a
evalExpr (Bin i) = i
evalExpr (Num i) = i
evalExpr (a :+: b) = evalExpr a +  evalExpr b
evalExpr (a :-: b) = evalExpr a -  evalExpr b
evalExpr (a :=: b) = evalExpr a == evalExpr b
evalExpr (a :<: b) = evalExpr a <  evalExpr b

transform :: (ExprType a, ExprType b) => (Expr b -> Expr b) -> Expr a -> Expr a
transform = undefined