Num-using binop

general eval.hs

-- Written by Eitan Chatav, cleaned up by me

{-# language GADTs #-}

import Type.Reflection
import Data.Constraint

data U_Expr
  = U_Bool Bool
  | U_Int Int
  | U_Double Double
  | U_And U_Expr U_Expr
  | U_Num2 Num2 U_Expr U_Expr

type Num2 = forall a. Num a => a -> a -> a

data T_Expr x where
  T_Bool :: Bool -> T_Expr Bool
  T_Int :: Int -> T_Expr Int
  T_Double :: Double -> T_Expr Double
  T_And :: T_Expr Bool -> T_Expr Bool -> T_Expr Bool
  T_Num2 :: Num x => (x -> x -> x) -> T_Expr x -> T_Expr x -> T_Expr x

data Type x where
  TypeBool :: Type Bool
  TypeInt :: Type Int
  TypeDouble :: Type Double

data (:::) f g = forall x. Typeable x => (:::) (f x) (g x)

check :: U_Expr -> Maybe (T_Expr ::: Type)
check expr = case expr of
  U_Bool x -> return $ T_Bool x ::: TypeBool
  U_Int x -> return $ T_Int x ::: TypeInt
  U_Double x -> return $ T_Double x ::: TypeDouble
  U_And x y -> do
    tx ::: tyx <- check x
    ty ::: tyy <- check y
    HRefl <- eqTypeRep (typeOf tyx) (typeOf tyy)
    HRefl <- eqTypeRep (typeOf tyx) (typeOf TypeBool)
    return $ T_And tx ty ::: TypeBool
  U_Num2 f x y -> do
    tx ::: tyx <- check x
    ty ::: tyy <- check y
    HRefl <- eqTypeRep (typeOf tyx) (typeOf tyy)
    Dict <- checkNum tyx
    return $ T_Num2 f tx ty ::: tyx

    where checkNum :: Type x -> Maybe (Dict (Num x))
          checkNum TypeInt = Just Dict
          checkNum TypeDouble = Just Dict
          checkNum _ = Nothing

eval :: T_Expr a -> a
eval (T_Bool a) = a
eval (T_Int a) = a
eval (T_Double a) = a
eval (T_And x y) = eval x && eval y
eval (T_Num2 f x y) = f (eval x) (eval y)

main = do
  case check (U_Num2 (*) (U_Int 3) (U_Int 3)) of
     Just (expr ::: TypeInt) -> print $ eval expr
     _ -> pure ()