🐈‍⬛

2023/04/03に公開

## 例

``````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があるエラーが（型チェックの結果）出ます。

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

## 実装

と「エフェクトに部分型のある代数的効果」

を混ぜたものです。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."
``````

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

``````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つきラムダ計算に型をつけたい、というのは昨年からの夢だった

ので、ひとまず実装できてよかったです。