Zenn
🐈‍⬛

HaskellでAlgebraic Effectsつき型付きラムダ計算

2023/04/03に公開
Haskell
tech

はじめに

前回の記事ではHaskellで単純型付きラムダ計算を実装しました。ですので（？）、今回はAlgebraic Effectsをつけます。

例

実際どんな式が評価できるか例をあげます。見やすいように式は適宜改行しています。

assume double: int -> int
let h = handler double (val x: int -> x) (
	(x: int, k: int -> int{}) -> (k (k x))
)　in with h handle (perform double 3 + 10)

これは型チェックが通り、値は23になります。
他にも

assume double: int -> int
assume doublee: int -> int
let h = handler double (val x: int -> x) (
	(x: int, k: int -> int{}) -> (k (x + 1))
) in with h handle 
	let hh = handler doublee (
		val x: int -> (x + perform double 2)
	) (
		(x: int, k: int -> int{double}) -> (k (x + 1))
	) in with hh handle (10 + perform doublee 3)

は17です。
ここで

assume double: int -> int
assume doublee: int -> int
let hh = handler doublee (
	val x: int -> (x + perform double 2)
) (
	(x: int, k: int -> int{double}) -> (k (x + 1))
) in with hh handle (10 + perform doublee 3)

とすると、"Unhandled Effects exist"とハンドルされていないEffectがあるエラーが（型チェックの結果）出ます。

実際にはHaskellのコードだと以下です。改行を（assumeの後を除いて）許さないので見にくいですが。。。

main :: IO ()
main = do
    print .run $ "assume double: int -> int\nlet h = handler double (val x: int -> x) ((x: int, k: int -> int{}) -> (k (k x))) in with h handle (perform double 3 + 10)" -- Right (Int 23)
    print .run $ "assume double: int -> int\nassume doublee: int -> int\nlet h = handler double (val x: int -> x) ((x: int, k: int -> int{}) -> (k (x + 1))) in with h handle let hh = handler doublee (val x: int -> (x + perform double 2)) ((x: int, k: int -> int{double}) -> (k (x + 1))) in with hh handle (10 + perform doublee 3)" -- Right (Int 17)
    print .run $ "assume double: int -> int\nassume doublee: int -> int\nlet hh = handler doublee (val x: int -> (x + perform double 2)) ((x: int, k: int -> int{double}) -> (k (x + 1))) in with hh handle (10 + perform doublee 3)" -- Left "Unhandled Effects exist"

実装

前回の記事の単純型付きラムダ計算にλeff
https://github.com/Nymphium/lambdaeff

と「エフェクトに部分型のある代数的効果」
https://nymphium.github.io/2019/12/22/effsub.html

を混ぜたものです。Efficient compilation of algebraic effects
and handlersも参考にしています。と言ってもどれも参考にしているだけなのでおかしい部分は私がおかしいだけです。

前回の記事の差分に重点的にコメントをつけています。

まずASTは以下。

import Text.Parsec
import Text.Parsec.String (Parser)
import Data.Either

data Exp
    = Var String
    | Lam String PureType Exp
    | Exp :@: Exp
    | Exp :+: Exp
    | Int Int
    | Eff_ String -- effect
    | Handler String (String, PureType, Exp) (String, PureType, String, PureType, DirtyType, Exp) -- handler　<effect> <value handler> <effect handler>式
    | WithH Exp Exp -- with <handler> <exp>式
    | Let String Exp Exp
    | Perform String Exp -- perform <effect> <exp>式
    | Assume String PureType PureType -- assume <effect> <type> <type>式。パースの都合でここに入れているが、完全に特別扱いしても良い
    | Abort -- 型チェックが通れば起こらないはず。。。
    deriving (Show, Eq)

ここで型は以下。Dirty/Pureの単語はEfficient compilation of algebraic effects
and handlersより。

data DirtyType
    = Dirt PureType [String] -- effectをリストでもつ。Setの方が良いが力尽きた
    deriving (Show, Eq)

data PureType
    = TInt -- base type
    | TArrow PureType DirtyType -- 関数型
    | THandler DirtyType DirtyType -- ハンドラ型
    | THole -- Holeの型
    deriving (Show, Eq)

data Type
    = PType PureType
    | DType DirtyType
    | TEff PureType PureType -- effectそのものの型
    deriving (Show, Eq)

type TEnv = [(String, Type)]

そうしたら型チェックは以下。基本的に「エフェクトに部分型のある代数的効果」の図を見れば良い。subtyping対応が面倒だが、

  • e: tはe: t{}でもある
  • t{}はtのsubtypeである
  • t{eff1}はt{eff1, eff2}のsubtypeであるし、t{eff1, eff2}はt{eff1, eff2, eff3}のsubtypeである

に注意すれば良い。例えば足し算なら

  • int + intはint
  • int{} + intはint{}がintのsubtypeなのでint + intになり、int
  • int{eff1} + int{eff2}は両方int{eff1, eff2}のsubtypeなので、int{eff1, eff2}

となる。はず。

-- 補助関数。ちゃんとSetを使えばいらない
uniq :: Eq a => [a] -> [a]
uniq [] = []
uniq (x:xs) = (if x `elem` xs then id else (x:)) $ uniq xs

subset :: [String] -> [String] -> Bool
subset [] _ = True
subset (x:xs) y = if x `elem` y then subset xs y else False

-- 型チェック
typeOf:: TEnv -> Exp -> Either String Type
typeOf env (Var x) = case lookup x env of
    Just t -> Right t
    Nothing -> Left $ "Unbound Variable: " ++ x
typeOf env (Lam x tx e) = do
    ty <- typeOf ((x, PType tx): env) e
    case ty of
        DType dtype -> Right . PType $ TArrow tx dtype
        PType ptype -> Right . PType $ TArrow tx $ Dirt ptype [] -- 関数型は返り値がDirtyTypeなので
typeOf env (e1 :@: e2) = do
    ty1 <- typeOf env e1
    ty2 <- typeOf env e2
    case (ty1, ty2) of
        (PType (TArrow t1 t2), PType pty2) | t1 == pty2 -> Right $ DType t2
        (PType (TArrow t1 t2), DType (Dirt pty2 [])) | t1 == pty2 -> Right $ DType t2 -- subtyping. int{}<intみたいなケース
        _ -> Left $ "Type Mismatch."
typeOf env (e1 :+: e2) = do
    ty1 <- typeOf env e1
    ty2 <- typeOf env e2
    case (ty1, ty2) of
        (PType TInt, PType TInt) -> Right . PType $ TInt
        (DType (Dirt TInt []), PType TInt) -> Right . PType $ TInt -- ここから下はsubtyping対応
        (PType TInt, DType (Dirt TInt [])) -> Right . PType $ TInt
        (DType (Dirt TInt eff), PType TInt) -> Right . DType $ Dirt TInt eff
        (PType TInt, DType (Dirt TInt eff)) -> Right . DType $ Dirt TInt eff
        (DType (Dirt TInt eff1), DType (Dirt TInt eff2)) -> Right . DType $ Dirt TInt $ uniq eff1 ++ eff2
        _ -> Left $ "Type Mismatch."
typeOf _ (Int _) = Right . PType $ TInt
typeOf env (Let x e1 e2) = do
    ty1 <- typeOf env e1
    ty2 <- typeOf ((x, ty1):env) e2
    case (ty1, ty2) of
        (PType _, PType _) -> Right $ ty2
        (DType (Dirt _ effs), PType ptype) -> Right . DType $ Dirt ptype effs -- ここから下はsubtyping.
        (PType _, DType (Dirt ptype effs)) -> Right . DType $ Dirt ptype effs
        (DType (Dirt _ effs1), DType (Dirt ptype effs2)) -> Right . DType $ Dirt ptype $ uniq　effs1 ++ effs2
typeOf env (WithH e1 e2) = do
    ty1 <- typeOf env e1
    ty2 <- typeOf env e2
    case (ty1, ty2) of
        (PType (THandler t1 t2), DType t3) | t1 == t3 -> Right $ DType t2
        (PType (THandler (Dirt ptype1 effs1) t2), DType (Dirt ptype2 effs2)) | ptype1 == ptype2 && subset effs2 effs1 -> Right $ DType t2 -- subtyping. effectは増やせる
        _ -> Left $ "Type Mismatch."
typeOf env (Perform sigma v) = do
    ty <- typeOf env v
    let eff = lookup sigma env
    case (ty, eff) of
        (PType pty, Just(TEff ptype1 ptype2))| pty == ptype1 -> Right $ DType $ Dirt ptype2 [sigma]
        _ -> Left $ "Type Mismatch."
typeOf env (Handler sigma (x, ptype3, e) (y, ptype4, k, ptype5, dtype1, e')) = do
    ty1 <- typeOf ((x, PType ptype3):env) e
    case (ty1, lookup sigma env) of
        (DType dtype2, Just(TEff ptypel ptyper)) | dtype2 == dtype1 && ptypel == ptype4  && ptyper == ptype5 -> f sigma y ptype4 k dtype1 env e'
        (PType ptype, Just(TEff ptypel ptyper)) | Dirt ptype [] == dtype1 && ptypel == ptype4  && ptyper == ptype5 -> f sigma y ptype4 k dtype1 env e' -- subtyping.
        _ -> Left $ "Type Mismatch."
        where 
            f :: String -> String -> PureType -> String -> DirtyType -> TEnv -> Exp -> Either String Type
            f sigma y ptype4 k dtype env e'= do
                ty2 <- typeOf ((y, PType ptype4):(k, PType (TArrow ptype5 dtype1)):env) e'
                case ty2 of
                    DType (Dirt ptype effs) -> Right $ PType $ THandler (Dirt ptype (sigma:effs)) dtype
                    _ -> Left $ "Type Mismatch."

次は評価ですが、これはλeffのものとほぼ同じなので省略します。これでeval1関数を得ます。

パーサーは以下のように書きました。

assumeParser :: Parser Exp
assumeParser = Assume <$ string "assume" <* spaces <*> many1 letter
            <* char ':' <* spaces <*> pureTypeParser <* spaces
            <* string "->" <* spaces <*> pureTypeParser

pureTypeParser :: Parser PureType
pureTypeParser = try funcTypeParser <|> varTypeParser

effectsTypeParser :: Parser [String]
effectsTypeParser = (many1 letter) `sepBy` char ','

dirtyTypeParser :: Parser DirtyType
dirtyTypeParser = Dirt <$> pureTypeParser <* char '{' <*> effectsTypeParser <* char '}'

funcTypeParser :: Parser PureType
funcTypeParser = TArrow <$> varTypeParser <* string "=>" <*> dirtyTypeParser

varTypeParser :: Parser PureType
varTypeParser = TInt <$ string "int"

typeParser :: Parser Type
typeParser = try (PType <$> pureTypeParser) <|> DType <$> dirtyTypeParser

termParser :: Parser Exp
termParser = try assumeParser <|> try letinParser <|> try handlerParser
            <|> try performParser <|> try withhParser <|> try lamParser
            <|> try appParser <|> try plusParser <|> try numParser
            <|> varParser


lamParser :: Parser Exp
lamParser = Lam <$ char '(' <* string "fn" <* space <*> many1 letter
            <* spaces <* char ':' <* spaces <*> pureTypeParser <* spaces
            <* string "->" <* spaces <*> termParser <* char ')'

appParser :: Parser Exp
appParser = do
    char '('
    t1 <- termParser
    spaces
    t2 <- termParser
    char ')'
    return $ t1 :@: t2

plusParser :: Parser Exp
plusParser = do
    char '('
    t1 <- termParser
    spaces
    char '+'
    spaces
    t2 <- termParser
    char ')'
    return $ t1 :+: t2

letinParser :: Parser Exp
letinParser = Let <$ string "let" <* spaces <*> many1 letter
            <* spaces <* char '='
            <* spaces <*> termParser <* spaces <* string "in" <* spaces
            <*> termParser

handlerParser :: Parser Exp
handlerParser = Handler <$> (string "handler" *> spaces *> many1 letter)
            <*> ((,,) <$ spaces <* char '(' <* string "val" <* spaces <*> many1 letter
            <* char ':' <* spaces <*> pureTypeParser <* spaces
            <* string "->" <* spaces <*> termParser <* char ')')
            <*>((,,,,,) <$ spaces <* string "((" <*> many1 letter
            <* char ':' <* spaces <*> pureTypeParser <* char ','
            <* spaces <*> many1 letter <* char ':' <* spaces
            <*> pureTypeParser <* spaces <* string "->" <* spaces
            <*> dirtyTypeParser <* char ')' <* spaces <* string "->" <* spaces
            <*> termParser <* char ')')

performParser :: Parser Exp
performParser = Perform <$ string "perform" <* spaces <*> many1 letter
            <* spaces <*> termParser

withhParser :: Parser Exp
withhParser = WithH <$ string "with" <* spaces <*> termParser
            <* spaces <* string "handle" <* spaces <*> termParser

varParser :: Parser Exp
varParser = Var <$> many1 letter

numParser :: Parser Exp
numParser = (Int . read) <$> many1 digit

parseTerm :: String -> Either ParseError Exp
parseTerm = parse termParser ""

とします。
最後に

-- effectをassume文で型環境に入れる
assume :: TEnv -> Exp -> TEnv
assume env (Assume x ptype1 ptype2) = (x, (TEff ptype1 ptype2)):env
assume env _ = env

parseAll :: String -> [Either ParseError Exp]
parseAll = map parseTerm . lines 

processAssume :: Foldable t => t Exp -> TEnv
processAssume = foldr (flip assume) []

-- λeffを参照
eval :: Exp -> Stack -> Stack -> Exp
eval t s es = go (t, s, es)
  where
    go mod =
      case eval1 mod of
        (v, [], _) | valuable v -> v
        mod' -> go mod'

notAssume :: Exp -> Bool
notAssume (Assume _ _ _) = False
notAssume _ = True

run :: String -> Either String Exp
run strExp = do
    -- assume文複数＋式1つの形しか評価できない
    let allAsts = rights $ parseAll strExp -- 文字式を改行で分けEXPのリストに
    let tenv = processAssume allAsts -- assume文の処理
    let ast = head $ filter notAssume allAsts -- 残った式
    case effectful <$> typeOf tenv ast of
        Left err -> Left err -- 型エラー
        Right True -> Left "Unhandled Effects exist" -- effect残り
        Right False -> Right $ eval ast [] []

として与えられた文字式をパースし型＆エフェクトのチェックをした後評価するrun関数が定義できました。

おわりに

Algebraic Effectsつきラムダ計算に型をつけたい、というのは昨年からの夢だった

型付きも実装してみたいですね。

https://zenn.dev/catminusminus/articles/64715088613417
ので、ひとまず実装できてよかったです。

Discussion