PHOAS - Parametric Higher Order Abstract Syntax - を Haskellで

当該タイトルの論文は http://dx.doi.org/10.1145/1411203.1411226
論文では Coqで書いてあるが、同じことが Haskell (+GADT) でもできるようで、Haskell-cafe に投稿されていた：
http://www.mail-archive.com/haskell-cafe@haskell.org/msg48913.html

HOASとは

http://en.wikipedia.org/wiki/Higher-order_abstract_syntax
コンパイラやインタプリタ等で(?)、 ターゲット言語のλ式やlet文みたいな 変数束縛を ホスト言語のλ式で表現してやろうぜというお話
変数の管理をしなくてよいのが楽。 あと domain specific language の変数束縛をお手軽に実装したり

PHOASとは

HOASだと λ式で書いた部分が 関数になってしまうので、関数本体のコードを表示したり解析したりpartial evaluationしたりということができない。
PHOASならそれができる（論文は読んでないけど上のpostを読むかぎりそういうことが分かった）
(というか、PHOASだとその辺を parametricにできるという事か。)

で、上のpostで 式を表示する関数 showExp をどうかく？というのが excerciseになっていたので書いた。あとちょっと修正

-- from http://www.haskell.org/pipermail/haskell-cafe/2008-November/050768.html
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

import Control.Monad.Reader

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

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  -- この2行が誤っていたのでちょっと修正した
evalP (LamP f) = evalP . f . Prim        -- 


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

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

時間がない…

こんなことやってる場合か＜俺