typecheck and eval.hs

thing.hs

-- Written by Eitan Chatav, cleaned up by me

{-# language GADTs #-}
module Wibble where

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_Add U_Expr U_Expr

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_Add :: Num x => T_Expr x -> T_Expr x -> T_Expr x
deriving instance Show (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_Add x y -> do
    tx ::: tyx <- check x
    ty ::: tyy <- check y
    HRefl <- eqTypeRep (typeOf tyx) (typeOf tyy)
    Dict <- checkNum tyx
    return $ T_Add 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_Add x y) = eval x + eval y