FOAS, HOAS, PHOAS - もうちょっとわかりやすく
絶賛現実逃避中。
先のエントリ PHOAS - Parametric Higher Order Abstract Syntax - を Haskellで - keigoiの日記 は phantom typeやら GADTやらを含んでいてわかりにくかったので もっと簡単にした
FOAS
{-# LANGUAGE FlexibleInstances #-} import Control.Monad.Reader import Data.Maybe (fromJust) -- FOAS data Term1 = Var String | Lam String Term1 | App Term1 Term1 | Con Int -- FOASなid関数 testFOAS :: Term1 testFOAS = Lam "x" (Var "x") badFOAS :: Term1 badFOAS = Lam "x" (Var "y") -- closed でない… -- FOASのevalは略
HOAS その1
-- HOAS その1 -- varに相当する項は無い。 data TermH = LamH (TermH -> TermH) | AppH TermH TermH | ConH Int -- evalってみる。非常に簡単。 evalH :: TermH -> TermH evalH x@(LamH _) = x evalH (AppH t1 t2) = case evalH t1 of { LamH f -> evalH (f (evalH t2)); ConH _ -> error "" } evalH x@(ConH _) = x -- HOASの項を表示 (関数の中身はわからない) instance Show TermH where show (LamH _) = "<fun>" -- λ抽象の中身はわからない show (AppH t1 t2) = show t1 ++ " " ++show t2 show (ConH i) = show i -- HOASなid関数 idH :: TermH idH = LamH (\x -> x) -- 中身はわからない -- *Main> idH -- <fun> -- HOASのテスト (\f -> f 1) (\x -> x) に相当 testHOAS = AppH (LamH $ \f -> AppH f (ConH 1)) (LamH $ \x -> x) -- 中身はわからない -- *Main> testHOAS -- <fun> <fun> -- evalのは簡単 -- *Main> evalH testHOAS -- 1
HOAS その2 ... 関数の中身を表示できるように
data VarE = VarE Char data TermH2 = LamH2 (VarE -> TermH2) | AppH2 TermH2 TermH2 | ConH2 Int | VarH2 VarE -- HOASの項を表示 (関数の中身もわかる) instance Show TermH2 where show t = runReader (showR t) 'a' where showR (LamH2 f) = do fresh <- ask body <- local succ (showR (f (VarE fresh))) return $ "(\\"++[fresh]++" -> "++body++")" showR (AppH2 t1 t2) = do t1' <- showR t1 t2' <- showR t2 return $ t1' ++ " " ++ t2' showR (ConH2 i) = return $ show i showR (VarH2 (VarE c)) = return $ [c] -- evalってみる。変数のルックアップが必要に。現実的でない。 evalH2 :: TermH2 -> TermH2 evalH2 t = runReader (evalH2R t) ([],'a') where evalH2R (AppH2 t1 t2) = do t2' <- evalH2R t2 t1' <- evalH2R t1 (_,fresh) <- ask case t1' of LamH2 f -> local (\(dic,var)->((fresh,t2'):dic,succ var)) (evalH2R (f (VarE fresh))) _ -> error "not function" evalH2R (VarH2 (VarE name)) = do (dic,_) <- ask return $ fromJust (lookup name dic) evalH2R x@(ConH2 _) = return x evalH2R x@(LamH2 _) = return x testHOAS2 = AppH2 (LamH2 $ \f -> AppH2 (VarH2 f) (ConH2 1)) (LamH2 $ \x -> VarH2 x) -- (\f -> f 1) (\x -> x) -- 関数の中身がわかる -- *Main> testHOAS2 -- (\a -> a 1) (\a -> a) -- *Main> evalH2 testHOAS2 -- 1
PHOAS -- HOAS2 の VarEの部分を 型変数 v で パラメータ化
data TermP v = VarP v | LamP (v -> TermP v) | AppP (TermP v) (TermP v) | ConP Int instance Show (TermP VarE) where show t = runReader (showR t) 'a' where showR :: TermP VarE -> Reader Char String -- 表示するときは freshな名前をぶちこむ showR (LamP f) = do fresh <- ask let body = f (VarE fresh) bodystr <- local succ $ showR body return $ "(\\" ++ [fresh] ++ " -> " ++ bodystr ++ ")" showR (AppP t1 t2) = do t1s <- showR t1; t2s <- showR t2; return $ t1s++" "++t2s showR (ConP i) = return $ show i showR (VarP (VarE name)) = return [name] newtype Id = Id (TermP Id) evalP :: TermP Id -> Int evalP t = case evalP t of ConP i -> i where evalP :: TermP Id -> TermP Id evalP x@(LamP _) = x -- evalるときは 項をそのままぶちこむ。 evalP (AppP t1 t2) = case evalP t1 of LamP f -> evalP (f (Id $ evalP t2)) ConP _ -> error "not a function" evalP x@(ConP _) = x evalP (VarP (Id t)) = t -- VarP (Id t) のt に項がそのまま入っているので 変数のルックアップは必要ない -- PHOASのテスト (\f -> f 1) (\x -> x) に相当 testPHOAS = AppP (LamP $ \f -> AppP (VarP f) (ConP 1)) (LamP $ \x -> (VarP x)) -- (\f -> f 1) (\x -> x) -- 表示ができる -- *Main> testPHOAS :: TermP VarE -- (\a -> a 1) (\a -> a) -- 評価もできる -- *Main> evalP testPHOAS -- 1
GADTとか
前回のエントリは GADTによって evalのエラーが起こらないことが保証されている (そのかわり \x -> x x みたいな項は書けない。)
