η簡約器

モナドなしで一意名生成 - 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を使っていては本末転倒だ。何か考える必要がある。