随伴がモテないのはどう考えてもモナドが悪い！（モナドとコモナドの関係が分かる話）

この記事が対象としている読者

コモナドって何となく聞いたことがある人
圏論よく分かんないけど、圏の定義（対象と射と合成と恒等射と……）みたいなことは聞いたことがある人

要するに、モヤモヤしてても問題ないのですけれど、最低限の知識くらいはあった方がいいってことなのですー＞ω＜

また、この記事は深淵なHaskell プログラマのみが書くことを許されると言われるモナドチュートリアルではないのでそういったものを期待されていたら、ごめんなさいなのです＞＜

コモナド（´・ω・`）

さて、みなさんはコモナドについてご存知です(・ω・？

google:コモナド Haskellで調べると、

こもなど！コモナド！Comonad！！ - capriccioso String Creating(Object something){ return My.Expression(something); }

という id:its_out_of_tune さんの記事が見つかりますです(・ω・）

この記事を読んでみると（ぜひ一読することをオススメしますです）、ふむふむ……( ,,｀･ ω´･)？

MonadとComonadの関数は以下のように対になっているのです。

Comonad Monad

extract:: w a -> a return :: a -> m a

duplicate :: w a -> w (w a) join :: m (m a) -> m a

(=>>) :: w a -> (w a -> b) -> w a (>>=) :: m a -> (a -> m b) -> m b

http://d.hatena.ne.jp/its_out_of_tune/20130413/1365837949

Comonad	Monad
extract:: w a -> a	return :: a -> m a
duplicate :: w a -> w (w a)	join :: m (m a) -> m a
(=>>) :: w a -> (w a -> b) -> w a	(>>=) :: m a -> (a -> m b) -> m b

……なるほどー＞ω＜　コモナド（Comonad）というのはつまり、モナドのそれぞれの関数の矢印をひっくり返したものみたいなのですー＞ω＜

そしてこのブログ記事ではこのあと、二値のタプルが、一方の値を与えたときコモナドになることを説明しています。

な、なるほど……( ﾟДﾟy)y !??

唐突に話が分からなくなってような気がしますです（id:its_out_of_tuneさんごめんなさいです（＿＿）

ですが、ここでこのように考えてみたりはしませんでしょうか？？？

「モナドとコモナドが対応しているんだから、あるモナドに対しても対応するコモナドがあるんじゃないです（・ω・？」

そして、このようにどのモナドがどのコモナドに対応しているのか分かれば、少しは話しが面白くなるのではないかと思うのですー＞ω＜

そこで今回はStateモナドに対応するコモナドを探ってみるのですー＞ω＜

Stateモナドに対応するコモナドは?(=ﾟωﾟ=;)

きっとGoogle先生が教えてくれるはず！　ということでgoogle:State comonadでググってみますですー＞ω＜

すると、次のStack Overflowの質問がヒットしました。

haskell - What is the Store comonad? - Stack Overflow

Stack Overflowなので当然英語なのですが、がんばって読んでみると、まず質問の部分に、

I've heard that Store = CoState, the dual of the State Monad.
http://stackoverflow.com/questions/8766246/what-is-the-store-comonad

という記述がありますです。そしてベストアンサーの方には、

As far as its relation to State goes, you could look at it like this:
type State s a = s -> (a, s)
type Store s a = (s -> a, s)
http://stackoverflow.com/questions/8766246/what-is-the-store-comonad

とありましたのです。

なるほど、Stateモナドに対応するコモナドはStoreコモナドというのですねー＞ω＜

それで、その型は……（上と少し違っていますが、dataにしただけなのです）、

data Store s a = Store (s -> a) s

となるわけなのですねー＞ω＜

って、あれれ……(ﾟ△ﾟ；)

コモナドはモナドの矢印を逆にしたものだったのに、StoreコモナドはStateモナドの矢印を逆にしたものじゃない！？

と、いうよりも、

確かにStateモナドとStoreコモナドは似ているけれど、どうしてこの二つが対応してるのです？？

一体どこからStoreコモナドはやってきたのです( ,,｀･ ω´･)？

その謎を探るべく、わたしたちは随伴関手へと飛びますですー＞ω＜

随伴関手?(=ﾟωﾟ=;)

さて、やっとのことでこの記事のタイトルにもある随伴関手という文字列が出てきたのですー＞ω＜

まずはこの随伴関手というものについて、Wikipedia大先生に聞いてみましょう。

随伴関手 - Wikipedia

数学特に圏論において、随伴関手（ずいはんかんしゅ）とは2つの関手の間にある関係である。
随伴は数学のあらゆるところに現れる。とくに、最適化と効率化を直観的に表現する。
一番簡単で対称な定義では、圏 $\mathcal{C}$ と $\mathcal{D}$ の随伴とは、2つの関手
$F: \mathcal{D} \rightarrow \mathcal{C}$ and $G: \mathcal{C} \rightarrow \mathcal{D}$
と、変数 $X$ と $Y$ について自然な全単射の族
$\mathrm{hom}_{\mathcal{C}}(FY,X) \cong \mathrm{hom}_{\mathcal{D}}(Y,GX)$
のことをいう。このとき、関手 $F$ を左随伴と呼び、関手 $G$ を右随伴と呼ぶ。また、「 $F$ は $G$ の左随伴である」 (同じことだが、「 $G$ は $F$ の右随伴である」)という関係を次のように書く。
$F\dashv G$
http://ja.wikipedia.org/wiki/随伴関手

な、なるほどー(-ω- ?)

Wikipedia大先生の言うことはきっと正しいのですが、なぜか難解に書かれる傾向がありますし、さらに言えばそれが本当に正しいかを確かめるためには結局別の資料が必要になるため、結局概観を掴む以上の価値はないのではないかと思うこの日頃なのです(´・ω・`)*1

さて、このままでは分かりにくいので、Haskellに書き下してみようと思いますです。

まず、Adjunctionという型クラスを定義しますですー＞ω＜

上のWikipediaの文章をがんばって読むと、

2つの関手
$F: \mathcal{D} \rightarrow \mathcal{C}$ and $G: \mathcal{C} \rightarrow \mathcal{D}$

この辺りから、Adjunctionは二つの関手を要求する型クラスであると想像できますですー＞ω＜

class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where

そして、この型クラスを構成する関数は、

変数 $X$ と $Y$ について自然な全単射の族
$\mathrm{hom}_{\mathcal{C}}(FY,X) \cong \mathrm{hom}_{\mathcal{D}}(Y,GX)$
のことをいう。

この辺りから、

  phiLeft  :: (f a -> b) -> (a -> g b)
  phiRight :: (a -> g b) -> (f a -> b)
  -- ただし、phiRight,phiLeftは、
  -- phiRight . phiLeft  . phiRight = phiRight
  -- phiLeft  . phiRight . phiLeft  = phiLeft
  -- を満たしますですー＞ω＜

となると想像できますですー＞ω＜

自然な全単射の族って何( ,,｀･ ω´･)？　それがどうしてこんなHaskellになるの( ,,｀･ ω´･)？

とまあ、そうなりますですよねー

一応、わたしなりに説明はしてみますですが、正しいという保証はしないことにしておきますです。

まず $\mathrm{hom}_{\mathcal{C}}(X,Y)$ が圏 $\mathcal{C}$ の対象 $X$ から $Y$ への射の集合であることは知っていますですね？

この $\mathrm{hom}_{\mathcal{C}}(X,Y)$ をHaskellで表わそうとすると、

type hom x y = x -> y

のようになりますです。

「圏 $\mathcal{C}$ の対象 $X$ から $Y$ への射の集合」の、

「圏 $\mathcal{C}$ 」を「Hask圏」に

「対象」を「型引数」に

「射」を「関数」に

「集合」を「型シノニム」

にすればその通りだと分かるはずです。（実はここで型シノニムを代数的データ型にしてもあまり問題はないのですが、後々の都合からこのようにしておきますです）

次に $\cong$ というのはこの文脈の場合、自然同型を表しますです。それでいてこの場合は全単射ですので、 $\cong$ というのは $\leftrightarrows$ に（イメージの上で）置き換えることができて、

$\mathrm{hom}_{\mathcal{C}}(FY,X) \leftrightarrows \mathrm{hom}_{\mathcal{D}}(Y,GX)$

つまり、

$\mathrm{hom}_{\mathcal{C}}(FY,X) \rightarrow \mathrm{hom}_{\mathcal{D}}(Y,GX)$

という $f \in \mathrm{hom}_{\mathcal{C}}(FY,X)$ が与えられたとき一つの $g \in \mathrm{hom}_{\mathcal{D}}(Y,GX)$ が定まる右向きの射と、

$\mathrm{hom}_{\mathcal{C}}(FY,X) \leftarrow \mathrm{hom}_{\mathcal{D}}(Y,GX)$

という $g \in \mathrm{hom}_{\mathcal{D}}(Y,GX)$ が与えられたとき一つの $f \in \mathrm{hom}_{\mathcal{C}}(FY,X)$ が定まる左向きの射がそれぞれ存在する、ということになりますですー＞ω＜

そして、これらをHaskellにすると、

  phiLeft  :: (f a -> b) -> (a -> g b)
  phiRight :: (a -> g b) -> (f a -> b)

と、なるわけなのです。 $\mathrm{hom}_{\mathcal{C}}(FY,X)$ が(f a -> b)に、 $\mathrm{hom}_{\mathcal{D}}(Y,GX)$ が(a -> g b)に対応してるのが分かると思いますですー＞ω＜

ここで勘のいい人は、 $\mathrm{hom}_{\mathcal{C}}(FY,X)$ は圏 $\mathcal{C}$ 上のhom集合で $\mathrm{hom}_{\mathcal{D}}(Y,GX)$ は圏 $\mathcal{D}$ 上のhom集合なのに、Haskellではどちらも同一の圏の上の話にしてしまっているじゃないか、と憤慨されるかもしれませんです(´・ω・`)　しかし、Haskellでプログラミングする場合は全てHask圏の上での話になるので、これで問題はないのです。*2

また、

  -- ただし、phiRight,phiLeftは、
  -- phiRight . phiLeft  . phiRight = phiRight
  -- phiLeft  . phiRight . phiLeft  = phiLeft
  -- を満たしますですー＞ω＜

という条件は、この二つが全単射であることを保証するための、モナド則みたいなものですー＞＜*3

随伴関手を実装してみる（・ω・）

実装してみると理解が深まることがある……（？？）、ので実装してみたいと思いますですー＞ω＜

まず、次のような関手二つを用意しますです。

-- type Writer s a = (s, a) としたいけどHaskellは型シノニムから型クラスのインスタンスにできないので……
data Writer s a = Writer s a

instance Functor (Writer s) where
  fmap f (Writer s x) = Writer s (f x)

-- type Reader s a = (s, a) としたいけど（ry
newtype Reader s a = Reader (s -> a)

instance Functor (Reader s) where
  fmap f (Reader g) = Reader (f . g)

普通のライターモナド（Writer）とリーダーモナド（Reader）ですー＞ω＜

この二つ、名前からして何か関係がありそうですよね？？

そうなのです！　この二つは随伴関手対となっていますのです＞ω＜　つまり、

instance Adjunction (Writer s) (Reader s) where
  phiLeft  f = \x-> Reader $ \s-> f $ Writer s x
  phiRight g = \(Writer s x)-> let Reader r = g x in r s

のようにしてAdjunctionのインスタンスにすることができますですー＞ω＜

さて、これでAdjunctionが実装できたわけなのですが……

なにか分かりましたです( ,,｀･ ω´･)？

分かったらすごいと思うのですけど……

随伴からモナドへ＞ω＜

さて、Adjunctionを実装してみたのですが、結局それの何がすごいのかよく分からなかったのです……（´・ω・`）

しかし、随伴には面白い性質があります！

それは、随伴からモナドを構成することができる、というものです。

具体的なコードを書くと、

newtype Compose f g a = Compose {
  getCompose :: g (f a) }

という、二つの関手を合成してできた型（関数の合成の型バージョンだと考えてみてくださいです）が、

instance (Functor f, Functor g, Adjunction f g) =>
    Monad (Compose f g) where
  -- 実装は後述ですー＞＜

のように、Monadのインスタンスになる、ということです！

どのようにしてMonadのインスタンスにするのか挑戦してみたい方はすぐに先へ進まずに、一旦エディターを開いてコードを書いてみてはどうです( ,,｀･ ω´･)？

この実装は結構頭を使うことになると思いますですー＞ω＜

……

………

…………

準備はよいでしょうか？　それでは正解発表ですー＞ω＜

instance (Functor f, Functor g, Adjunction f g) =>
    Functor (Compose f g) where
  fmap f (Compose m) = Compose $ fmap (fmap f) m

join :: (Functor f, Functor g, Adjunction f g) => Compose f g (Compose f g a) -> Compose f g a
join (Compose m) = Compose $ fmap (phiRight getCompose) m

instance (Functor f, Functor g, Adjunction f g) =>
    Monad (Compose f g) where
  return x = Compose $ phiLeft id x
  m >>= f = join $ fmap f m

ポイントはjoinですー＞ω＜　もちろんjoinを使わなくても(>>=)は定義できるのですが、joinを使った方が簡単です~~し、後々のコモナドと対比しやすくなるのですー~~＞ω＜

折角モナドにしたので、これを使ってみましょう。Composeに、さっきAdjunctionのインスタンスにした(Writer s)と(Reader s)を当てはめた型シノニムを作りますですー＞ω＜

type State s = Compose   (Writer s) (Reader s)

あれ？　なんでこの型シノニムの名前はStateなのです？？

それを考えるためには、これまでWriter、Reader、Composeをそれぞれ型クラスのインスタンスにするために代数的データ型を使って定義してきましたが、それを型シノニムを使ったものに書き直してみると分かると思いますですー＞ω＜

type Writer' s a = (s, a)
type Reader' s a = s -> a

type Compose' f g a = g (f a)

type State' s = Compose' (Writer' s) (Reader' s)

このState' s a型を展開するとどのような型になるです( ,,｀･ ω´･)？

Compose' (Writer' s) (Reader' s) a
= Reader' s (Writer' s a)
= s -> (s, a)

よってs -> (s, a)という型になったのです！　このs -> (s, a)という型はどこかで見たことありませんか？？

そうです！　これはStateモナドと同じ型になるのですー＞ω＜

なので、このState型に対して適切な関数を追加していくと、

put :: s -> State s ()
put s = Compose . Reader $ \_-> Writer s ()

get :: State s s
get = Compose . Reader $ \s-> Writer s s

runState :: State s a -> s -> (s, a)
runState (Compose (Reader r)) s = let Writer s' a = r s in (s', a)

Stateモナドとしてちゃんと機能していることが確かめられるのですー＞ω＜

fib :: Int -> State Int Int
fib n = do
  i <- get
  put (i + 1)
  if n <= 1
    then return 1
    else do
      x <- fib (n - 1)
      y <- fib (n - 2)
      return (x + y)

main :: IO ()
main = print $ runState (fib 10) 0

-- (177,89)
-- と表示されますですー＞ω＜

随伴からコモナドへ＞ω＜

随伴からモナドが導けることが分かったのですが、ここで、このように考えてみたりしないでしょうか？？

「さっきはCompose f g x = g (f x)というように二つの関手を合成したけれど、この合成の順序を逆にしたらどうなるんだろう( ,,｀･ ω´･)？」

つまり、

newtype Cocompose f g x = Cocompose {
  getCocompose :: f (g x) }

という合成を考えるわけです。

すると、一体どうなるのでしょうか？　って、名前から何となく想像がつきますですよね。

そう！　さっきと合成の順序を逆にすると、コモナドを作ることができますです。その実装はこんな風になりますです。

instance (Functor f, Functor g, Adjunction f g) =>
    Functor (Cocompose f g) where
  fmap f (Cocompose w) = Cocompose $ fmap (fmap f) w

instance (Functor f, Functor g, Adjunction f g) =>
    Comonad (Cocompose f g) where
  extract (Cocompose w) = phiRight id w
  duplicate (Cocompose w) = Cocompose $ fmap (phiLeft Cocompose) w

このreturnとextract、joinとduplicateの実装を比較すると、このようになりますですー＞ω＜

Monad	Comonad
return = Compose . phiLeft id	extract = phiRight id . getCocompose
join = Compose . fmap (phiRight getCompose) . getCompose	duplicate = Cocompose . fmap (phiLeft Cocompose) . getCocompose

何となくですけど、お互いに関係し合っているような印象がありますですね。

それでは、さっきと同様にこちらでもCocomposeにWriter sとReader sを当てはめてみるのです。

type Store s = Cocompose (Writer s) (Reader s)

Store、という名前が出てきましたね。こちらも型シノニムで考えてみるのです！！

Cocompose (Writer' s) (Reader' s) a
= Writer' s (Reader' s a)
= (s, s -> a)

(s, s -> a)というのは、タプルの順序が逆ですが、上の方に書いたStoreと同じになっていますですー＞ω＜

これで、なぜStateモナドに対応するコモナドがStoreコモナドなのか分かったのではないかと思いますですー＞ω＜

まとめですー＞ω＜

モナドの矢印をひっくり返すとコモナドになりますですー＞ω＜
Stateモナドに対応するコモナドはStoreコモナドですー＞ω＜
随伴は左随伴 $F$ と右随伴 $G$ 、自然な全単射の族 $\mathrm{hom}_{\mathcal{C}}(FY,X) \cong \mathrm{hom}_{\mathcal{D}}(Y,GX)$ から成り立っていて、これらを組み合わせることでモナドとコモナドを導くことができますですー＞ω＜

余談ですー＞＜

今回は話の中でいきなりWriterとReaderが出てきて、この2つで随伴になると説明しましたが、実際はStateモナドやStoreコモナドからこの2つの関手を導くことができますです。こエーレンブルク・ムーア代数というものを使うといいのですが……それについてはこの辺りを参考にしてほしいのですー＞ω＜

また、全体的に怪しい記述が多いので、私の書いた文章を端から端まで信用するのは多分よくないと思います。何か間違っているところがあったらコメントなりTwitterなりで教えてもらえるととても嬉しいのですー＞ω＜

今回作ったファイル

Adjunction.hs

{-# LANGUAGE FunctionalDependencies #-}
module Adjunction where

-- Adjunction型クラスの定義ですー＞ω＜

class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where
  phiLeft  :: (f a -> b) -> (a -> g b)
  phiRight :: (a -> g b) -> (f a -> b)


-- (Writer s) -| (Reader s)随伴対ですー＞ω＜

-- type Writer s a = (s, a) としたいけどHaskellは型シノニムから型クラスのインスタンスにできないので……
data Writer s a = Writer s a

instance Functor (Writer s) where
  fmap f (Writer s x) = Writer s (f x)

-- type Reader s a = (s, a) としたいけど（ry
newtype Reader s a = Reader (s -> a)

instance Functor (Reader s) where
  fmap f (Reader r) = Reader (f . r)


-- (Writer s) -| (Reader s) Adjunction型クラスのインスタンスですー＞ω＜

instance Adjunction (Writer s) (Reader s) where
  phiLeft  f = \x-> Reader $ \s-> f $ Writer s x
  phiRight g = \(Writer s x)-> let Reader r = g x in r s


-- 随伴からモナドへ（・ω・）

newtype Compose f g a = Compose {
  getCompose :: g (f a) }

instance (Functor f, Functor g, Adjunction f g) =>
    Functor (Compose f g) where
  fmap f (Compose m) = Compose $ fmap (fmap f) m

join :: (Functor f, Functor g, Adjunction f g) => Compose f g (Compose f g a) -> Compose f g a
join (Compose m) = Compose $ fmap (phiRight getCompose) m

instance (Functor f, Functor g, Adjunction f g) =>
    Monad (Compose f g) where
  return x = Compose $ phiLeft id x
  m >>= f = join $ fmap f m


-- 随伴からコモナドへ（・ω・）

class Functor w => Comonad w where
  extract :: w a -> a
  extend :: (w a -> b) -> w a -> w b
  duplicate :: w a -> w (w a)

  extend f = fmap f . duplicate
  duplicate = extend id

newtype Cocompose f g a = Cocompose {
  getCocompose :: f (g a) }

instance (Functor f, Functor g, Adjunction f g) =>
    Functor (Cocompose f g) where
  fmap f (Cocompose w) = Cocompose $ fmap (fmap f) w

instance (Functor f, Functor g, Adjunction f g) =>
    Comonad (Cocompose f g) where
  extract (Cocompose w) = phiRight id w
  duplicate (Cocompose w) = Cocompose $ fmap (phiLeft Cocompose) w


-- 随伴対からモナド、コモナドを作るのですー＞ω＜

type State s = Compose   (Writer s) (Reader s)
type Store s = Cocompose (Writer s) (Reader s)


-- 上のStateがStateモナドになっているのか確かめるのですー＞ω＜

put :: s -> State s ()
put s = Compose . Reader $ \_-> Writer s ()

get :: State s s
get = Compose . Reader $ \s-> Writer s s

runState :: State s a -> s -> (s, a)
runState (Compose (Reader r)) s = let Writer s' a = r s in (s', a)

Main.hs

module Main where
import Adjunction

fib :: Int -> State Int Int
fib n = do
  i <- get
  put (i + 1)
  if n <= 1
    then return 1
    else do
      x <- fib (n - 1)
      y <- fib (n - 2)
      return (x + y)

main :: IO ()
main = print $ runState (fib 10) 0

*1:この一文もややWikipedia的性質を含みますです

*2:厳密には問題になることもあるかもしれませんですが、そういうときはAgdaとかHaskellであればConstraintKinds拡張なんかを使うといいと思いますですー

*3:本当は、どちらか一つだけ満たしていれば両方が満たされますです

Moon? Shadow! - Misc Memo

Moon? Shadow!の記事にならない雑多なメモなのですー＞ω＜

この記事が対象としている読者

コモナド（´・ω・`）

Stateモナドに対応するコモナドは?(=ﾟωﾟ=;)

随伴関手?(=ﾟωﾟ=;)

自然な全単射の族って何( ,,｀･ ω´･)？　それがどうしてこんなHaskellになるの( ,,｀･ ω´･)？

随伴関手を実装してみる（・ω・）

随伴からモナドへ＞ω＜

随伴からコモナドへ＞ω＜

まとめですー＞ω＜

余談ですー＞＜

今回作ったファイル

この記事が対象としている読者

コモナド（´・ω・`）

Stateモナドに対応するコモナドは?(=ﾟωﾟ=;)

随伴関手?(=ﾟωﾟ=;)

自然な全単射の族って何( ,,｀･ ω´･)？ それがどうしてこんなHaskellになるの( ,,｀･ ω´･)？

随伴関手を実装してみる（・ω・）

随伴からモナドへ＞ω＜

随伴からコモナドへ＞ω＜

まとめですー＞ω＜

余談ですー＞＜

今回作ったファイル

自然な全単射の族って何( ,,｀･ ω´･)？　それがどうしてこんなHaskellになるの( ,,｀･ ω´･)？