η簡約器
モナドなしで一意名生成 - www.kotha.netの裏のアイディアを検証するための例題として、λ式をη簡約するプログラムを書いてみる。構文をパース→処理→PrettyPrint、という流れを最低限要求する問題としてη簡約が手頃だと思った。
構文木を表現するデータとしては、Higher Order Abstract Syntaxを試みたけれど挫折したので、存在量化を使って一意名を直接保持する方針で行く。
{-# LANGUAGE RankNTypes, ScopedTypeVariables, ExistentialQuantification #-} import MyUnique import Control.Monad.Error import Data.Maybe import qualified Data.Map as M import qualified Data.Set as S import Text.ParserCombinators.Parsec import Text.ParserCombinators.Parsec.Language(haskell) import Text.ParserCombinators.Parsec.Token as Parsec import Text.PrettyPrint.HughesPJ as Ppr import Unsafe.Coerce newtype Var s = Var (MyUnique s) deriving (Eq, Ord) data Exp s = Ref (Var s) | forall t. (Subset s t) => Lam (Maybe String) (MyUnique t -> Maybe (MyUnique s)) (Var t) (Exp t) | App (Exp s) (Exp s) instance Show (Exp s) where show = render . ppr embedV :: (Subset s t) => Var s -> Var t embedV (Var x) = Var (embed x) embedM :: (Subset s t) => M.Map String (Var s) -> M.Map String (Var t) --embedM = fmap embedV -- inefficient! embedM = unsafeCoerce parseRef, parseLam, parseApp, parsePrim, parseExp :: forall s. M.Map String (Var s) -> CharParser () (Exp s) parseRef env = do name <- identifier haskell case M.lookup name env of Just v -> return $ Ref v Nothing -> fail $ "unbound variable: " ++ name parseLam env = fresh1 (undefined :: MyUnique s) $ \une u -> do reservedOp haskell "\\" name <- identifier haskell reservedOp haskell "->" body <- parseExp $ M.insert name (Var u) $ embedM env return $ Lam (Just name) une (Var u) body parseApp env = do es <- many1 $ parsePrim env return $ foldl1 App es parsePrim env = parseRef env <|> Parsec.parens haskell (parseExp env) parseExp env = parseLam env <|> parseApp env parseAll :: String -> Exp EmptySet parseAll s = case parse p "" s of Left err -> error $ "parse error: " ++ show err Right r -> r where p = do v <- parseExp M.empty eof return v ppr :: Exp s -> Doc ppr = f False 0 M.empty where f :: Bool -> Int -> M.Map (Var s) String -> Exp s -> Doc f paren n env e = case e of Ref v -> case M.lookup v env of Just s -> text s Nothing -> text "<free variable>" Lam name une v body -> par $ let str = fromMaybe "" name ++ "[" ++ show n ++ "]" in fsep [text $ "\\" ++ str, text "->", f False (n+1) (M.insert v str $ embedM1 env) body] App fun arg -> par $ f True n env fun <+> f True n env arg where par = if paren then Ppr.parens else id embedM1 :: (Subset s t) => M.Map (Var s) a -> M.Map (Var t) a --embedM1 = M.mapKeys embedV embedM1 = unsafeCoerce eta :: Exp s -> Exp s eta = fst . f where f :: Exp s -> (Exp s, S.Set (Var s)) f e = case e of Ref v -> (e, S.singleton v) Lam name une v@(Var u) (App body (Ref z)) | z == v && not (S.member v fvs) -> (unsafeCoerce body', unsafeCoerce fvs) | otherwise -> (Lam name une v (App body' (Ref z)), uneSet une u $ S.insert z fvs) where (body', fvs) = f body Lam name une v@(Var u) body -> (Lam name une v body', uneSet une u fvs) where (body', fvs) = f body App fun arg -> (App fun' arg', S.union fvf fva) where (fun', fvf) = f fun (arg', fva) = f arg uneSet :: (MyUnique t -> Maybe (MyUnique s)) -> MyUnique t -> S.Set (Var t) -> S.Set (Var s) --uneSet une u = S.map (fromJust . une') . S.filter (isJust . une') -- where -- une' (Var u) = fmap Var (une u) uneSet une u = unsafeCoerce . S.delete (Var u) main = do ln <- getLine print $ eta $ parseAll ln main
これで一応動くことは動くのだが、安全に一意名を生成したいのにこんなにunsafeCoerceを使っていては本末転倒だ。何か考える必要がある。