Monad
Menu Menu
Monad とは?
Haskell では IO や、Error を表す返り値、Exception などで Monad が頻繁に使われている。IO などを表すデータ構造 (= Functor ) を定義して、Functor に作用する自然変換を通して、そのデータ構造を操作するのが Monad である。このデータ構造は文脈と呼ばれることもある。
もともと圏論の概念であり、少々複雑であるが、折角なので、ちゃんと数学的な定義を理解しよう。
Functor T と二つの自然変換からなる Monad Monad から作られる Kleisli Categoryを理解する。Monad のプログラミングは、Kleisli Category の射(普通のデータを受け取って、Monad を返す関数)を定義して、Monad の自然変換で合成していくことになる。
Monad を自分で定義するには、Monad の自然変換を自分で定義すれば良い。
Monad の Functor T によって、以下のような機能を持つ計算を定義することができる。(x は集合の直積、+ は排他的和)
最も単純な計算 | T(A) = A | ||||||
部分計算 | T(A) = A + ⊥ (⊥は未定義値) | ||||||
非決定的な計算 | T(A) = A2 | ||||||
副作用のある計算 | T(A) = (A x S)s (Sは状態の集合) 例外のある計算 | A + E (E は例外の集合) | 継続のある計算 | R R A R は計算結果 | 計算量を持つ計算 | A x N (N は計算量) | |
Maybeの復習
class Monad1 t where eta :: a -> t a mu :: t ( t a ) -> t a instance Monad1 MyMaybe where eta x = MyJust x mu MyNothing = MyNothing mu (MyJust MyNothing) = MyNothing mu (MyJust (MyJust x)) = MyJust x instance Monad MyMaybe where return x = MyJust x (>>=) MyNothing f = MyNothing (>>=) (MyJust x) k = k xMyJust が値を返し、MyNothing は計算が失敗して値がないことを示している。
eta は自然変換で、1 (identityFunctor) から t (この場合はMyMaybe )へのデータ構造の変換。
eta :: a -> t aこれが Monad の return になる。普通に値を返す時には return 1 とかすれば良い。
mu も自然変換で t の入れ子を解消するデータ変換になる。
mu :: t ( t a ) -> t aこれを組み合せて、MyMaybe を返す関数 f と g の合成を計算することができる。
f :: b -> t c g :: a -> t bの時に、
f ・ g :: a -> t c f ・ g = \ x -> mu ( fmap f (g x) )とすればよい。
Monad が作る圏
圏(category)は、集合である関数の型を対象とし、射を関数とする構造体で、射の結合 o に対して、単位元idがあり、左単位元 id a o f = f 右単位元 f o id a = f 結合法則 (f o g ) o h = f o (g o h )
が成り立つものだった。
f :: a -> t bに、これらが成り立てば、Monad を返す関数は、圏の射になる。この圏を Monad t の Kliesli 圏という。
id :: a -> t x id x = return x f ・ id = \ x -> mu ( fmap f (id x) ) id ・ f = \ x -> mu ( fmap id (f x) ) f ・ (g ・ h) = \ x -> ? (f ・ g) ・ h = \ x -> ?
問題
MyMaybe に関して上の性質が成り立っていることを具体的な値について確認せよ。
mu と eta が自然変換であることを示せ。
Monadの自然変換μ
μ : TT → T μ(a) TT(a) -------> T(a) | | TT(f)| |T(f) | | v μ(b) v TT(b)---------->T(b)が可換である必要がある。μの引数は型変数。
Monadの自然変換η
η(a) a ------------> T(a) | | f| |T(f) | | v η(b) v b ------------->T(b)
Monad の構文
Haskell の Monad では様々な構文が用意されている。
f ・ g = \ x -> mu ( fmap f (g x))これを、Haskell では、
g >>= fと書く。方向が逆だが、gの方が先に計算されるので、この方が良い。
eta は return と書く。
infixl 1 >>, >>= class Monad m where (>>=) :: m a -> (a -> m b) -> m b return :: a -> m a instance Monad (T1 a) where return a = eta a (>>=) = \t \f -> mu (fmap f t)という風に定義されている。m は Functor である。
join は自然変換μを使わずに、>>= を直接定義すると Haskell では効率が良い。
instance Monad (Maybe a) where return x = just x nothing >>= _ = nothing just x >>= k = k x良く使われる形は、
g >>= (\x → ... x ... )だが、これを
do x <- g ... x ...と書く構文がHaskellには用意されている。Monad T は T を返す必要があるので、
return aつまり、η : 1 → T が返す T を返すのが普通。例えば、fをMonadを返さない普通の関数だとして、
do x <- g return (f x)となる。gが返すのはMonadで、f x は通常の値を返す。return がそれを (η : 1 → T)を用いてTに変換している。
fが直接Tを返すなら、
do x <- g f x
Applicative
Haskell では Monad は Applicative であることが要請される。
x24 = pure (+) <*> mydiv 3 1 <*> mydiv 3 0あるいは
x24 = (+) <$> mydiv 3 1 <*> mydiv 3 0Applicative で書く方が効率が良いと言われてる。(本当?)
Monoid Monad
ここではListをMonoid として使う。計算の履歴を取ったりするのに便利なMonad。data T1 m a = T [m] a deriving (Show) instance Functor T1 where fmap f ( T m a ) = T m ( f a )ηは eta 、μ は mu として定義する
eta a = T [] a mu (T m (T m' a)) = T (m ++ m') aこれの Monad と Applicative の実装は?
factorial の計算の履歴を見てみる。
fact1 0 = return 1 fact1 n = do c <- fact1 (n -1) Tn [c] ( n * c )
IO Monad
Haskell では IO は Monad として実装されている。
IO Monad は見れない
getChar から getLine を作る
getll = do c <-getChar if c=='\n' then return [] else do l <- getll return (c:l)
問題
getChar/putChar の型を確認せよ
putll を作り、putll getll してみる。
IO Monadを作ってみる
data IOTeletype a = GetChar (Char -> IOTeletype a) | PutChar Char (IOTeletype a) | ReturnTeletype a mu :: IOTeletype ( IOTeletype a ) -> IOTeletype a mu (GetChar f) = GetChar ( \ c -> mu ( f c) ) mu (PutChar c f) = PutChar c ( mu f ) mu (ReturnTeletype x) = x -- return : (x : a) -> IOTeletype a -- _>>=_ : IOTeletype a -> ( a -> IOTeletype b ) -> IOTeletype b instance Monad IOTeletype where return = ReturnTeletype (GetChar f) >>= g = GetChar (\c -> (f c >>= g)) (PutChar c f) >>= g = PutChar c (f >>= g) (ReturnTeletype x) >>= g = g xこのままでは動かない。IOTeletypeはメタ計算なので、この部分を解釈する driver が必要。
runTT :: (IOTeletype a) -> ([ Char ] , [Char ] ) -> ( a, [Char] ) runTT (ReturnTeletype a) (i,o) = (a , o ) runTT (GetChar f) ((h:t),cs) = runTT (f h) (t,cs) runTT (PutChar c f) (cs,h) = runTT f (cs, h ++ [c])これを show に埋め込むこともできる。
-- simple driver for IOTeletype instance (Show a) => Show (IOTeletype a) where show t = showTT t ("test\nabcd\n",[]) where showTT (GetChar f) ((h:t),cs) = showTT (f h) (t,cs) showTT (PutChar c f) (cs,h) = showTT f (cs, h ++ [c]) showTT (ReturnTeletype x) (i,o) = "TTY output = " ++ o ++ "\nResult =" ++ show xもう少し細かく
-- detailed driver for IOTeletype instance (Show a) => Show (IOTeletype a) where show t = showTT t ("test\nabcd\n",[]) where showTT (GetChar f) ((h:t),cs) = "GetChar(" ++ (showTT (f h) (t,cs)) ++ ")" showTT (PutChar c f) (cs,h) = "PutChar(" ++ [c] ++ ", " ++ ( showTT f (cs, h ++ [c])) ++ ")" showTT (ReturnTeletype x) (i,o) = "ReturnTeletype(" ++ show x ++ "," ++ show ( i,o ) ++ ")"runTT は IO Monad が返ってから計算されるように見えるが、実際には get/put の event とともに解釈される。
Haskell 内部で、こうなっているとは限らない。
Hakell の IO Monad をSimulate する
Monad の組み合せ
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 )でいけそうである
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)となっている。
instance (Functor m) => Functor (T1T n m) where fmap f (T1T x) = T1T ( fmap (fmap f) x ) -- instance (Monad m,Functor m) => Applicative (T1T n m) where pure x = T1T ( return ( eta x ) ) (<*>) (T1T f) (T1T x) = T1T $ do Tn m f'' <- f Tn m' x'' <- x return $ Tn ( m ++ m') ( f'' x'' ) instance Monad m => Monad (T1T n m) where return a = T1T $ return $ eta a n >>= k = T1T $ do Tn m a <- runT1T n Tn m' a' <- runT1T (k a) return $ Tn (m++m') a' instance MonadTrans (T1T n) where lift m = T1T $ do t <- m return ( Tn [] t ) -- lift = T1T . liftM ( Tn [] )この Monad の切り替えには lift という関数を使う。これを IO Monad (あるいは他の Monad)に付ける必要があるので、class 経由で定義する必要がある。
instance (MonadIO m) => MonadIO (T1T n m) where liftIO = lift . liftIO fact3 :: (Eq n, Num n, Show n) => n -> T1T n IO n fact3 0 = return 1 fact3 n = do lift $ putStrLn (show n) c <- fact3 (n -1) T1T $ return $ Tn [c] ( c * n )monoidT