result.txt

*Main> r
TArrow TBool TBool
TArrow (TArrow TBool TBool) (TArrow TBool TBool)
(\a -> (\b -> a b)) (\a -> if a then False else True) True
(\a -> (\a -> if a then False else True) a) True
(\a -> if a then False else True) True
if True then False else True
False

やったーできました

STLC.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}

import Control.Monad.Reader

data Typ where
  TBool  :: Typ
  TArrow :: Typ -> Typ -> Typ
  deriving (Show, Eq)

data Val v where
  VBool :: Bool -> Val v
  VAbs :: Typ -> (v -> Term v) -> Val v

data Term v where
  TmVal :: Val v -> Term v
  TmVar :: v -> Term v
  TmApp :: Term v -> Term v -> Term v
  TmIf  :: Term v -> Term v -> Term v -> Term v

joinTerm :: Term (Term v) -> Term v
joinTerm (TmVal (VBool v)) = TmVal (VBool v)
joinTerm (TmVal (VAbs ty f)) = TmVal (VAbs ty $ joinTerm . f . TmVar)
joinTerm (TmVar t) = t
joinTerm (TmApp t1 t2) = TmApp (joinTerm t1) (joinTerm t2)
joinTerm (TmIf t1 t2 t3) = TmIf (joinTerm t1) (joinTerm t2) (joinTerm t3)

isval :: Term a -> Bool
isval (TmVal _) = True
isval _ = False

eval1 :: Term (Term a) -> Term a
eval1 tm = case tm of
  TmVar v -> v
  TmApp (TmVal v1) t2@(TmVal _) ->
    case v1 of
      VAbs _ f -> joinTerm $ f $ joinTerm t2
      _ -> error "Not applicative"
  TmApp t1@(TmVal _) t2 -> TmApp (joinTerm t1) (eval1 t2)
  TmApp t1 t2 -> TmApp (eval1 t1) (joinTerm t2)
  TmIf (TmVal (VBool True))  t2 _ -> joinTerm t2
  TmIf (TmVal (VBool False)) _ t3 -> joinTerm t3
  TmIf (TmVal _) _ _ -> error "Not bool"
  _ -> error "No rule applies"

showsTerm :: Term Char -> ShowS
showsTerm tm = runReader (showR tm) 'a'
  where
    showR :: Term Char -> Reader Char ShowS
    showR (TmVal (VBool True)) = return ("True"++)
    showR (TmVal (VBool False)) = return ("False"++)
    showR (TmVal (VAbs _ f)) =
      do i <- ask
         s <- local succ $ showR (f i)
         return $ ("(\\"++) . (i:) . (" -> "++) . s . (")"++)
    showR (TmVar i) = return $ (i:)
    showR (TmApp t1 t2) = return $ showsTerm t1 . (" "++) . showsTerm t2
    showR (TmIf t1 t2 t3) =
      return $ ("if "++) . showsTerm t1 . (" then "++) . showsTerm t2 . (" else "++) . showsTerm t3

instance (v ~ Char) => Show (Term v) where
  show t = showsTerm t ""

typeof :: Term Typ -> Typ
typeof tm = case tm of
  TmVal (VBool _) -> TBool
  TmVal (VAbs ty f) -> TArrow ty (typeof (f ty))
  TmVar v -> v
  TmApp t1 t2 ->
    case typeof t1 of
      TArrow ty1 ty2 | ty1 == typeof t2 -> ty2
      _ -> err
  TmIf t1 t2 t3 ->
    case typeof t1 of
      TBool | ty2 == ty3 -> ty2
      _ -> err
    where
      ty2 = typeof t2
      ty3 = typeof t3
  where
    err = error "type check failed"

termNot = TmVal $ VAbs TBool $ \x -> TmIf (TmVar x) (TmVal $ VBool False) (TmVal $ VBool True)
testFun = TmVal (VAbs (TArrow TBool TBool) $ \x -> TmVal (VAbs TBool $ \y -> TmApp (TmVar x) (TmVar y)) )
test v = TmApp (TmApp testFun termNot) (TmVal $ VBool v)

r = do print (typeof termNot)
       print (typeof testFun)
       go (test True)
  where
    go :: (forall v. Term v) -> IO ()
    go t = do
      print t
      unless (isval t) (go (eval1 t))