Effの型シグネチャの理解
全てのEffectは、Eff rで表現されている
mtlがモナドスタックだったことに対称的mrsekut.icon
code:hs
data Void
run :: Eff Void w -> w
code:hs
type Reader e
ask :: (Typeable e, Member (Reader e) r) => Eff r e
local :: (Typeable e, Member (Reader e) r) => (e -> e) -> Eff r a -> Eff r a
runReader :: Typeable e => Eff (Reader e :> r) w -> e -> Eff r w
code:hs
type Exc e
throwError :: (Typeable e, Member (Exc e) r) => e -> Eff r a
catchError :: (Typeable e, Member (Exc e) r) => Eff r w -> (e -> Eff r w) -> Eff r w
runError :: Typeable e ⇒ Eff (Exc e :> r) w -> Eff r (Either e w)
code:hs
type State s
get :: (Typeable s, Member (State s) r) => Eff r s
put :: (Typeable s, Member (State s) r) => s -> Eff r ()
runState :: Typeable s => Eff (State s :> r) w -> s -> Eff r (w, s)
code:hs
type Lift m
lift :: (Typeable1 m, MemberU2 Lift (Lift m) r) => m w -> Eff r w
runLift :: (Monad m, Typeable1 m) => Eff (Lift m :> Void) w -> m w
Exc eのeとか、State sのsとか
Int :> String :> Bool :> Voidのような型は
'[Int, String, Bool, Void]のような型レベルリストと読み替えればいい
論文内では「集合」と呼んでいるが、型レベルリストと考えた方がイメージがしやすいmrsekut.icon
m :> r'
論文内では以下のように説明している
集合rを、2つの集合{m}とr'に分けていることを表す
$ r = \{m\} \cup r'
これをリストと読み替えて、普通のListにおける:みたいに、m : r'をイメージすれば良い
そうすれば、m :> r'が、r == '[m] ++ r'のようなものだと理解できる
Member m r
mが、型レベルリストrの要素であることを表す
論文では集合扱いなので、$ m \sub rの意味である
具体的にはMember m '[Int, Bool, String]なら、
mが、IntやBoolやStringなら制約を満たすことになる
Effectの文脈では、mは常にMonadである
だから、具体的にはMember m '[Reader Int, Reader Bool, State Int]のようなものの話をしている
Eff型
Eff r e
rは
「request」の意
上の例では、runHoge以外はここは開かれている
具体例を見ればわかりやすい
Eff (Reader Int :> Reader String :> Void) a
eは
普通に返り値
そんな重要ではない
普通のMonadの話と同じ
トップダウン的にはこういう要望である
Eff r eがある時に、
「あるEffect mが、このrに含まれる」ということを言いたい
そうじゃないと「Readerが含まれている」などを言えないのでmrsekut.icon
方法は2つある
Member m rという制約を書く
明示的にm :> r'と書く
結合したものを見る
Eff Void a
Voidは空リストだと考えられる
Eff Void a型は、何のEffectも持っていないという意味になるので、
つまりこれはpureな計算を表す
Eff (Reader Int :> Reader String :> Void) a
Reader Int :> Reader String :> Voidという一連のEffectを実行する関数だと見ることができる
つまり、IntとStringの2つのEnvにaccessするものだとわかる
小さい例
code:hs
t1 :: Member (Reader Int) r => Eff r Bool
t1 = do
n <- ask
return $ n == 1
型を見れば、Intの環境にアクセスして、Bool値を返すことがわかる
code:hs
t1 :: Member (Reader Int) r => Eff r Int
t1 = do
v <- ask
return $ (v+1 :: Int)
Intの環境から取ってきて、それincrementしてIntを返す
code:hs
t1r = run $ runReader t1 (10 :: Int) -- 11
t1rの型は、(Readerの制約のない)Effect r Intになる
つまり、runReaderを介することで、rのリストからReaderが排除されたものが返る
filterされる
code:hs
runReader :: Typeable e => Eff (Reader e :> r) w -> e -> Eff r w
これを繰り返して、最後までrを減らしていき、完全に空Voidになったら、runで単純な値Intを取り出すことができる
code:hs
run :: Eff Void w -> w
型を無視して式だけ見ると、t1の実装はmtlでの実装と全く同じ
code:hs
t1 :: ReaderT Int Int
t1 = do
v <- ask
return $ (v+1 :: Int)
実際、mtlで実装できるものはEffで実装できる
しかし、Effの方が一般的なので、逆はできない
例えば、複数のReaderを重ねるときは、mtlの場合はliftでアクセスする必要がある
code:hs
t2 :: ReaderT Int (Reader Float) Float
t2 = do
v1 <- ask
v2 <- lift ask
return $ fromIntegral (v1 + (1 :: Int)) + (v2 + (2 :: Float))
Ext Effではそのまま書ける
制約に複数のReaderを追加するだけで良い
code:hs
t2 :: (Member (Reader Int) r, Member (Reader Float) r) => Eff r Float
t2 = do
v1 <- ask
v2 <- ask
return $ fromIntegral (v1 + (1 :: Int)) + (v2 + (2 :: Float))
またExt Effの方は、2つのReader間に順序がない
mtlの方はFloatの方をliftしなければならなかった
この順序はrunする時に決定される
code:hs
t2r = run $ runReader (runReader t2 (10 :: Int)) (20 :: Float)
逆に書いてもよい
しかし、例外とかがある場合は順序は関係ある
code:hs
ter1 :: (Eiter String String, Int)
ter1 = run $ runState (runError tes1) (1 :: Int) -- (Left "exc", 2)
ter2 :: Eiter String (String, Int)
ter2 = run $ runError (runState test1 (1::Int)) -- Left "exc"
IOなどをリストに入れるためにはLiftを使う
code:hs
tl1 :: (MemberU2 Lift (Lift IO) r, Member (Reader Int) r) => Eff r ()
tl1 = ask >>= \x -> lift . print $ (x+1 :: Int)