Too lazy to evaluate - Control.Monad.Coの正体

TL;DR
背景
モナド Co w の具体例たち
Co wは常にStateLikeを使って表すことができる
まとめと今後

TL;DR

Control.Monad.Coにある、各コモナドwに対して定義されるモナドCo wは、Stateモナドの一般化と見なせる。

背景

kan-extensionsというパッケージに、CoTというモナド変換子が定義されています。 (Control.Monad.Co)

CoTは、“Monads from Comonads”（Comonadから作ったMonad）と形容されており、実際に以下のような定義とMonadのインスタンスを持っています。

type Co w = CoT w Identity

newtype CoT w m a = CoT
  { runCoT :: forall r. w (a -> m r) -> m r }

instance (Functor w) => Functor (CoT w m)
instance (Comonad w) => Applicative (CoT w m)
instance (Comonad w) => Monad (CoT w m)
instance (Comonad w) => MonadTrans (CoT w)

すなわち、Comonadであるwに対して、CoT w mはMonadです。

私がCoTというものを知ったのは最近のことではないのですが、「ComonadをMonadに作り変えられるとは、なんて神秘的なんだろう」「このforall r.は何だろう」「Either eが例外の作用、State sが可変状態の作用を表すなら、Co wは何の作用を表すのだろう」と思いはしたものの、特に深く考えてみようとは思っていませんでした。

ですが、最近すこし思い立って¹、一般のCoTではなくCo w = CoT w Identityに限って真面目に検討してみました。すると驚いたことに²、Co wはある意味でStateモナドの一般化であり、とても身近な作用が不思議な見た目をしているだけだということがわかりました。本記事ではこのことについて解説します。

モナド `Co w` の具体例たち

解説の本体に入る前に、まずは定義の準備をします。ここでは、モナド変換子であるCoTではなく、ただのCoについて考えます。そのため、CoTを介さないシンプルな定義を用いることにします。

-- kan-extensionsの定義とは異なる
newtype Co w = Co { runCo :: forall r. w (a -> r) -> r }

Coのモナドのインスタンスは以下のように定義されます。

instance Functor f => Functor (Co f) where
    fmap g (Co c) = Co (c . fmap (. g))

instance Comonad w => Applicative (Co w) where
    pure a = Co \war -> extract war a
    (<*>) = ap

instance Comonad w => Monad (Co w) where
    ma >>= k = joinCo $ fmap k ma

joinCo :: Comonad w => Co w (Co w a) -> Co w a
joinCo mma = Co $ runCo mma . extend (flip runCo)

「Co wがStateモナドの一般化である」と言いましたが、実際にCo wがStateモナドと同型になることがあります。Storeコモナドの場合を考えると、Co (Store s)はState sとモナドとして同型です。

data Store s a = Store (s -> a) s
newtype State s a = State (s -> (s, a))

実際、以下のような計算によって同型が確認できます。³

Co (Store s) a
 ~ ∀r. Store s (a -> r) -> r
 ~ ∀r. (s -> a -> r, s) -> r
 ~ ∀r. (s -> a -> r) -> s -> r
 ~ ∀r. s -> (s -> a -> r) -> r
 ~ s -> ∀r. (s -> a -> r) -> r
 ~ s -> (s, a)
 ~ State s a

その他のコモナドに対してもCoによってどんなモナドが得られるかを見ていくと、次のようになります。

Co (Env e) a ~ (e -> a) ~ Reader e a

[Env](https://hackage.haskell.org/package/comonad-5.0.8/docs/Control-Comonad-Env.html#g:2)コモナドは、`Co`によって`Reader`モナドになります。

Co (Env e) a
 ~ ∀r. Env e (a -> r) -> r
 ~ ∀r. (e, a -> r) -> r
 ~ ∀r. e -> (a -> r) -> r
 ~ e -> ∀r. (a -> r) -> r
 ~ e -> a
 ~ Reader e a

Co (Traced m) a ~ (m, a) ~ Writer m a

Tracedコモナドは、CoによってWriterモナドになります。

Co (Traced m) a
 ~ ∀r. Traced (a -> r) -> r
 ~ ∀r. (m -> a -> r) -> r
 ~ ∀r. ((m,a) -> r) -> r
 ~ (m,a)
 ~ Writer m a

ところで、これらのState s, Reader e, Writer mというモナドは、いずれも以下のStateLike _ _を特殊化した形になっています。

data StateLike m s a = StateLike m (s -> a)
-- State s  ~ StateLike (s -> s) s
-- Reader e ~ StateLike ()       e
-- Writer m ~ StateLike m        ()

次節では、どんなコモナドwに対しても、Co wというモナドは、 Stateモナドを一般化したStateLikeの一例になっていることを説明します。

`Co w`は常に`StateLike`を使って表すことができる

どんなFunctor fについても、Co fは以下のMove fを用いてStateLike (Move f) (f ())と同型になります。

newtype Move f = Move { appMove :: forall r. f r -> r }

これは、Co f aから同型な型を辿って変形させていくことで得られます。

Co f a
 ~ ∀r. f (a -> r) -> r
 ~ ∀r. CoYoneda f (a -> r) -> r
 ~ ∀r. (∃s. (f s, s -> (a -> r))) -> r
 ~ ∀r. ∀s. (f s, s -> (a -> r)) -> r
 ~ ∀r. ∀s. f s -> (s -> a -> r) -> r
 ~ ∀s. ∀r. f s -> (s -> a -> r) -> r
 ~ ∀s. f s -> ∀r. (s -> a -> r) -> r
 ~ ∀s. f s -> (s, a)
 ~ ((∀s. f s -> s), (∀s. f s -> a))
 ~ (Move f, (∃s. f s) -> a)
 ~ (Move f, f () -> a)
 ~ StateLike (Move f) (f () -> a)

先述したように、Storeコモナドに対してCo (Store s)はState sと同型でした。 StateLikeによる上記の表現を使っても、State sと同型になることを確認してみましょう。

Move (Store s)
 ~ ∀r. Store s r -> r
 ~ ∀r. (s -> r, s) -> r
 ~ ∀r. (s -> r) -> (s -> r)
 ~ s -> s
  
Store s ()
 ~ (s -> (), s)
 ~ ((), s)
 ~ s

Co (Store s) a
 ~ StateLike (Move (Store s)) (Store s ()) a
 ~ StateLike (s -> s) s a
 ~ (s -> s, s -> a)
 ~ s -> (s, a)
 ~ State s a

多くのコモナドwに対してCo wモナドを求める場合、StateLikeを用いたほうが簡単になる場合があります。例えば、長さ1以上のリストNonEmptyはコモナドになっています。

ghci> import Control.Comonad
ghci> import Data.List.NonEmpty
ghci> xs = 4 :| [3,2,1]
ghci> extract xs     -- == head xs
4
ghci> duplicate xs   -- == tails1 xs
(4 :| [3,2,1]) :| [3 :| [2,1],2 :| [1],1 :| []]
ghci> toList . fmap toList $ duplicate xs
[[4,3,2,1],[3,2,1],[2,1],[1]]

このことによってCo NonEmptyはモナドになっています。これがどのようなモナドなのかをCoの定義から考えると中々大変なのですが、StateLikeによる表現を用いると以下のようになります。⁴

NonEmpty ()
 ~ (NonEmptyリストの長さの集合)
 ~ (1以上の整数の集合) = N

Move NonEmpty
 ~ ∀r. NonEmpty r -> r
 ~ ∀r. (r + (r,r) + (r,r,r) + … ) -> r
 ~ ∀r. (r -> r) × ((r,r) -> r) × ((r,r,r) -> r) × … 
 ~ (∀r. r -> r) × (∀r. (r,r) -> r) × (∀r. (r,r,r) -> r) × … 
 ~ {1} × {1,2} × {1,2,3} × …
 ~ { f :: N -> N  |  ∀n. f n ≤ n }

type Shrinking = { f :: N -> N | ∀n. f n ≤ n }

Co NonEmpty
 ~ StateLike (Move NonEmpty) (NonEmpty ())
 ~ StateLike Shrinking N

ここで、Shrinking = { f :: N -> N | ∀n. f n ≤ n }は、f nがn以下になるような関数f :: N -> Nを集めた集合です。

StateLike (N -> N) NはState Nと同型でした。ShrinkingをN -> Nの部分集合と見て、その包含写像によってStateLike Shrinking NをStateLike (N -> N) Nに写す自然変換はモナド準同型になります。（ただし注意が必要で、Move NonEmptyとShrinkingの間の同型をここでは具体的には指定していません。モナド準同型にするには適切な同型を選ぶ必要があります。）

まとめと今後

Co wという「コモナドから作ったモナド」は、StateLikeというStateモナドを一般化したような形のモナドになることを大雑把ながら説明しました。

実は、Comonadのうち、「性質のよい」Functorである多項式Functor⁵でもあるものならば、どんなComonad wも、あるCategoryのインスタンスを使って表現できる、という先行研究があります。⁶

このCategoryによる表現を使うと、よりCo wがStateらしく思えるCo wの特徴付けができます。これについても書きたかったのですが、説明に必要な事項が多く私が書くことを断念してしまったので、それはいつの日にかやることにしました。⁷

https://twitter.com/viercc/status/1647938927372943360↩︎
個人的な感想です↩︎
ほんとうは、単に同型であるだけでなく、具体的に同型を構成して、その同型写像ががモナドとしての同型写像でもあることまで確認しなければいけないのですが、ここでは省略します。↩︎
ただし、無限リストの存在は無視しています↩︎
このブログではモナドを見分けるコツや多項式Applicative Functorの一般論などで使いました。↩︎
Daniel Ahman and Tarmo Uustalu “Directed Containers as Categories.” https://arxiv.org/abs/1604.01187↩︎
本当にやる気がでるのか自信がない↩︎

Control.Monad.Coの正体

TL;DR

背景

モナド Co w の具体例たち

Co wは常にStateLikeを使って表すことができる

まとめと今後

モナド `Co w` の具体例たち

`Co w`は常に`StateLike`を使って表すことができる