Proof of type

type.hs

import Data.Either

data Term = TTrue
          | TFalse
          | TIf Term Term Term
          | TZero
          | TSucc Term
          | TPred Term
          | TIsZero Term

instance Show Term where
    show TTrue          = "#t"
    show TFalse         = "#f"
    show TZero          = "0"
    show (TIf t1 t2 t3) = "if " ++ show t1 ++ " then " ++ show t2 ++ " else " ++ show t3
    show (TSucc nv)     = "(succ " ++ show nv ++ ")"
    show (TPred nv)     = "(pred " ++ show nv ++ ")"
    show (TIsZero t)    = "(iszero " ++ show t ++ ")"

isnumerical :: Term -> Bool
isnumerical (TSucc t) = isnumerical t
isnumerical TZero = True
isnumerical _ = False

isval :: Term -> Bool
isval TTrue = True
isval TFalse = True
isVal t = isnumerical t

eval' :: Term -> Either Term Term

-- (E-IfTrue)
-- if true then t2 else t3   -> t2
eval' (TIf TTrue t2 _) = Right t2

-- (E-IfFalse)
-- if false then t2 else t3  -> t3
eval' (TIf TFalse _ t3) = Right t3

-- (E-If)
-- if t1 then t2 else t3     -> (t1 -> t1')
eval' (TIf t1 t2 t3)    = let t1' = eval' t1
                          in fmap (\t -> TIf t t2 t3) t1'

-- (E-Succ)
-- succ t -> (t -> t')
eval' (TSucc t) = let t' = eval' t
                  in fmap (\t -> TSucc t) t'


-- (E-PredZero)
-- pred 0 -> 0
eval' (TPred TZero) = Right TZero

-- (E-PredSucc)
-- pred (succ nv) -> nv
eval' (TPred (TSucc nv))
        | isnumerical nv = Right nv
        | otherwise      = Left $ TPred (TSucc nv)

-- (E-Pred)
-- pred t -> (t -> t')
eval' (TPred t) = let t' = eval' t
                  in fmap (\t -> TPred t) t'

-- (E-IsZeroZero)
-- iszero 0 -> true
eval' (TIsZero TZero) = Right TTrue

-- (E-IsZeroSucc)
-- iszero (succ nv) -> false
eval' (TIsZero (TSucc nv))
        | isnumerical nv = Right TFalse
        | otherwise      = Left $ TIsZero (TSucc nv)

-- (E-IsZero)
-- iszero t -> (t -> t')
eval' (TIsZero t) = let t' = eval' t
                    in fmap (\t -> TIsZero t) t'

eval' t = Left t

eval :: Term -> Term
eval t = case eval' t of Right t' -> eval t'
                         Left  t' -> t

inttoterm :: Int -> Term
inttoterm 0 = TZero
inttoterm n = TSucc (inttoterm (n-1))

exprstr :: Term -> String
exprstr t = (show t) ++ " = " ++ (show . eval) t


expressions = [TTrue
              , TIf TFalse TTrue TFalse
              , TZero
              , TSucc (TPred TZero)
              , TIsZero (TPred (TSucc $ TSucc TZero))]

main :: IO()
main = mapM_ putStrLn $ map exprstr expressions