Software Engineering Lecture s07
Menu Menu
Monad の組み合わせ
今日の元ネタはここ。http://www.slideshare.net/tanakh/monad-tutorial これと、
http://d.hatena.ne.jp/m-hiyama/20070507/1178496486 これ。
T1 という Monad を作ったのは良いが、これと、IO Monad は一緒に使えるのか。使うにはどうすれば良いのか?
Monad M と Monad N があったとする。この合成 Monad MN は、どうすれば作れるのか?
M : A -> A, N : A -> A の Functor なので、T = MN とすれば良さそうである。
ηm : 1->M
μm : MM->M
ηn : 1->N
μn : NN->N
これから、
μt : 1->T
ηt : TT->T
ができれば良い。ηt は、
ηt = ηm( ηn ) : 1->MN
とすれば良い。しかし、 μ = μm( μn ) とすると、
μm(a)
MM(a) ----------> M(a)
μn(a)
NN(a) ----------> N(a)
μ(a)
MMNN(a) ----------> MN(a)
となる。これは、MMNN -> MN であって、TT -> T つまり MNMN -> MN とは異なる。
ここで、
swap(a)
NM(a) ----------> MN(a)
という自然変換があったとする。
M swap(N a)
MNMN(a) ----------------> MMNN(a)
となるので、
μt = μm ( μη(a) ) ○ M swap ( N a )
でいけそうである。しかし、これから、Monad 則、μ ○ T η = μ ○ η T = 1, μ μ T = μ T μ が成立するように swap を定義して、実際に成立を確かめるのは厄介である。
つまり、Monad が二つあっても、それを組み合わせることは自明ではない。
Agda での Monad の組合せ
Agda による Monad Transちょっとやってみる
monoidT.hs
import Control.Monad.Trans
import Control.Monad (MonadPlus(..), liftM)
--import Control.Monad.IO.Class
class Monad1 t where
eta :: a -> t a
mu :: t ( t a ) -> t a
--class Monad1T t where
-- liftM :: Monad m => m a -> t m a
data T1 m a = Tn [m] a
deriving (Show)
instance Functor (T1 m) where
fmap f (Tn m a) = Tn m (f a)
instance Monad1 (T1 a) where
eta a = Tn [] a
mu (Tn m (Tn m' a)) =
Tn (m ++ m') a
instance Monad (T1 a) where
return a = eta a
(>>=) = \t f -> mu (fmap f t)
まず普通の。
fact0 0 = return 1
fact0 n = do
putStrLn (show n)
c <- fact0 (n -1)
return ( n * c )
当然動く。
fact1' 0 = return 1
fact1' n = do
putStrLn (show n)
c <- fact1' (n -1)
Tn [] ( n * c )
は型エラーとなる。 putStrLn (show n) は IO () を返すが、Tn は IO ではない。
mylift m =
Tn [] ( do
c <- m
putStrLn (show c)
return c
)
fact2 0 = return 1
fact2 n = do
mylift $ putStrLn (show n)
c <- fact2 (n -1)
Tn [c] ( n * c )
これで型は合うが、うまくうごかない。IO () を返すptStrLn が動作するためには、top level に IO () を返さなければならないので当然である。
つまり、IO Monad の中に Tn を持ってくる必要がある。そこで、newtype というものを使う。
newtype
newtype は機能的には data とそれにつく record field と同じ。ただし、filed は一つだけ。つまり、1対1対応になる。isomorphic とも言う。
newtype T1T n m a = T1T {
runT1T :: m ( T1 n a )
}
この m が T1 を格納する Monad のつもりである。:t を使って型をチェックしてみると、
T1T :: m (T1 n a) -> T1T n m a
runT1T :: T1T n m a -> m (T1 n a)
となっている。
Haskell では class に対応する実装は型一つに対して一つになっている。newtype で型を別にしてやると別な実装が可能になる。
T1T は Constructor で、T1 を格納する Monad ( m (T1 n a )) を受け取って、T1T n m a を返す。n m a は型変数であって、格納したのは、Monad 1 つと、それに包まれた T1 である。
runT1T は T1T を受け取って Monad を返す。
T1T の引数に Monad を渡してみる。
*Main> T1T ( do putStrLn "test" ;return ( Tn "T1 monad" 0))
<interactive>:248:1:
No instance for (Show (T1T Char IO a0))
IO は show できないが、うまく行っているようである。これから runT1T を使って、IO を取り出す。
runT1T ( T1T ( do putStrLn "test" ;return ( Tn "T1 monad" 0)))
test
Tn "T1 monad" 0
これで、top level に IO Monad を渡すことができた。このnewtype T1T が、
swap(a)
NM(a) ----------> MN(a)
の役割を果たしている。T1T で T1 の方を表に持ってきて、runT1T で(IO Monad の)後ろに持っていく感じである。
instance の定義と Type constraint
この Monad の切り替えには lift という関数を使う。これを IO Monad (あるいは他の Monad)に付ける必要があるので、class 経由で定義する必要がある。まず、T1T を Monad として定義するために、return と >>= を定義する。煩雑だが以下のようにする。
instance (Monad m) => Monad (T1T n m) where
return a = T1T $ return $ eta a
n >>= k = T1T $ do
t <- runT1T n
case t of
Tn m a -> do
t' <- runT1T (k a)
case t' of
Tn m' a' -> return $ Tn (m++m') a'
ここで、 (Monad m) => Monad (T1T n m) は m が Monad の型を持つ(つまり、return と >>= を持つ)ことを示している。これは type constraint と呼ばれる。Agda の{} に似ている。Agda と違い type constraint には限られた型しか置くことはできない。どれくらいの型が置けるかは、ghc の option とかで異なる。Haskell は Agda ほど強力な型を持たない。
定義は複雑だが、
return a = T1T $ return $ eta a
これは、
return a = T1T ( return ( Tn [] a))
の別構文である。() が減るので見やすくなると感じる人もいる。return は Monad を返すので、T1T が Monad を含む型に変換する。
>>= の方は、
n >>= k = T1T $ do
t <- runT1T n
で、T1T $ が最終的に T1T への変換を行うことを記述している。do は Monad の処理である。runT1T n の n は T1T Monad であり、そこから runT1Tが IO Monadを取り出している。 t <- runT1T n とすることにより、IO Monad の中身の値と取り出すのと、IO Monad の join が行われる。
t には、T1 が入っているが、T1 は nest してないので mu を使うことはできない。Monad の合成(join)を自分で行う必要がある。ここでは、case 文により、n と kのから m と m' を取り出して、m++m' を自分で計算している。
Tn m' a' -> return $ Tn (m++m') a'
は、T1 を含む IO Monad を返すが、先頭にT1T $ があったので、最終的には T1T が返ることなる。
n >>= k の定義の中では、do が二回使われているが、これは、T1T に含まれた Monad に対する do である。つまり、IO Monad になっている。runT1T で取り出して、T1T で合成することで、MM を MNMN に変換している。
Monad Transform
これで、T1T を Monad として定義できたが、lift をまだ定義してない。 lift の型
class MonadTrans t where
-- | Lift a computation from the argument monad to the constructed monad.
lift :: Monad m => m a -> t m a
なので、
instance MonadTrans (T1T n) where
lift m = T1T $ do
t <- m
return ( Tn [] t )
とする。lift は m か t<- m で中身を取り出して、それを T1 にして return で Monad m にする。それを T1T $ が T1T に変換する。これは Monad では定型的な処理であり、liftM として定義されているので、それを使っても良い。
instance MonadTrans (T1T n) where
lift = T1T . liftM ( Tn [] )
ここでは $ の代わりに . を使ってみた。
MonadTrans のinstallの仕方
cabal update cabal install mtlstack を使う場合は、
stack setup stack install mtl stack ghci --package mtlとするらしい。stackを使った Haskell環境構築
合成した Monad の使い方
fact3 0 = return 1
fact3 n = do
lift $ putStrLn (show n)
c <- fact3 (n -1)
T1T $ return $ Tn [c] ( c * n )
main = runT1T (fact3 3)
T1T を返す Monad 関数を作れば良い。
T1T $ return $ Tn [c] ( c * n )
は汚いが、なんらかの関数で隠すことはできる。ここでは return は使えないが、
fact3 :: (Eq n, Num n, Show n) => n -> T1T n IO n
と型を明示すれば、return で良いなら return を使える。
fact3 3 の結果は T1T なので直接表示はできない。
*Main> fact3 3
<interactive>:3:1:
No instance for (Show (T1T n0 IO n0))
runT1T で IO Monad を取り出して表示する。
*Main> runT1T (fact3 4)
4
3
2
1
Tn [1,1,2,6] 24
これで、IO Monad と自分で作った T1 Monad を同時に使うことができた。
返されているのは T1T Monad なので、これを、もう一度自分に接続することもできる。(階乗なので、あまり大きな数値を渡さないように)
*Main> runT1T (fact3 3 >>= fact3 )
liftIO
Monadの合成は多段で行われるが、IO はどこでも呼び出したいのが普通だろう。
instance (MonadIO m) => MonadIO (T1T n m) where
liftIO = lift . liftIO
とすると、IO Monad を持つ Monad まで上昇して IO を実行できる。
fact3' 0 = return 1
fact3' n = do
liftIO $ putStrLn (show n)
c <- fact3' (n -1)
T1T $ return $ Tn [c] ( c * n )
などとする。
これで、合成可能なMonadを作ることができた。
合成した Monad が Monad 則を満たしているかどうかを調べよう。( a >>= (b >>= c)) が ((a>>=b) >>= c) と同じ動作をするかどうかを確認する。
合成可能な Monad に IdentityMonad を組み合わせれば、元の Monad が得られる。つまり、Monad を自分で作る(ことはほとんど必要ないが)時には、MonadTrans などを定義できる形にしておくのが良い。
その他の Monad Transformers
さまざまな組み込み Monad で、MonadTrans がどのように定義されているかを調べよう。http://hackage.haskell.org/packages/archive/mtl/2.1.2/doc/html/Control-Monad-Error.html