SLC.hs

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

import Control.Monad.Reader

data Typ t where
  TBool  :: Typ Bool
  TArrow :: Typ a -> Typ b -> Typ (a -> b)

deriving instance Show (Typ a)

data ExpP v t where
   VarP :: v t -> ExpP v t
   ApP :: ExpP v (a -> b) -> ExpP v a -> ExpP v b
   LamP :: Typ a -> (v a -> ExpP v b) -> ExpP v (a -> b)
   TrueP :: ExpP v Bool

newtype Exp t = Exp (forall v. ExpP v t)

eval :: Exp t -> t
eval (Exp e) = evalP e

newtype Prim a = Prim a

-- PHOAS項の実行 --------
evalP :: ExpP Prim t -> t
evalP (VarP (Prim a)) = a
evalP (ApP e1 e2) = evalP e1 $ evalP e2
evalP (LamP _ f) = evalP . f . Prim
evalP (TrueP) = True

-- typeof

typeofP :: ExpP Typ a -> Typ a
typeofP (VarP ty) = ty
typeofP (ApP e1 _) =
  case typeofP e1 of
    TArrow _ ty -> ty
typeofP (LamP ty f) =
  TArrow ty $ typeofP $ f ty
typeofP (TrueP) = TBool
  
-- PHOAS項の表示 --------
-- めんどいので de Bruijn indicesで表現することに
newtype Var a = Var Int

-- reader モナドを使って freshな変数を供給
showExp :: ExpP Var a -> ShowS
showExp t = runReader (showExpR t) 0
  where
    showExpR :: ExpP Var a -> Reader Int ShowS
    showExpR (VarP (Var i)) = return (shows i)
    showExpR (ApP e1 e2)    = return $ \s -> showExp e1 $ " " ++ showExp e2 s
    showExpR (LamP _ f)    = 
       do i<-ask; 
          fstr <- local (+1) $ showExpR (f (Var i)); 
          return $ \s -> "\\" ++ shows i "-> " ++  fstr s
    showExpR (TrueP) = return ("True"++)

-- 試す
test = LamP (TArrow TBool TBool) $ \x -> (LamP TBool $ \y -> ApP (VarP x) (VarP y)) 
-- evalP test (+1) 2 ==> 3
-- putStrLn $ showExp test "" ==> \0-> \1-> 0 1