Too lazy to evaluate - Trail: 踏跡モナド

モチベーション: ListT done right を FreeT から作る

ListT done right （ちゃんとした方のListT）というモナド変換子をご存知でしょうか？ ListT (done wrong) はこのブログで度々取り上げました（2020年, 2021年）が、done right はこれとは別物です。(done wrong)はほぼ使われることはない¹のですが、done right は結構便利なモナドです。

さて、本記事では ListT done right にしか用がないので、それをListTとだけ呼ぶことにします。 ListT m aは、要素aを一つ取り出すたびにモナドmの副作用が必要になるようなリストを表している、と考えることができます。例えば、ネットワーク越しの通信によってデータを少しづつ読み出すときには ListT IO ByteStringが使えます。

ListTにはlist-t, list-transformer, List など複数の実装があります²。初めてこのモナドに触れる方にはlist-transformerのドキュメントが最もわかりやすいかと思います。

list-transformer のListTの定義を以下に引用します。

newtype ListT m a = ListT { next :: m (Step m a) }
data Step m a = Cons a (ListT m a) | Nil

さて、このListTですが、モナドの演算を忘れて単なる型として見れば、 FreeTモナド変換子（Control.Monad.Trans.Free）の特殊ケースになっています。

FreeTは以下のように定義されています。

newtype FreeT f m a = FreeT { runFreeT :: m (FreeF f a (FreeT f m a)) }
data FreeT f a r = Pure a | Free (f r)

このとき、次のような同型があります³。

ListT m a <-> FreeT ((,) a) m ()

ここで、((,) a)はタプル型のコンストラクタ(,)にaを部分適用した関手、つまり((,) a) b = (a,b)のことです。読みやすさのために、Pair = (,)という別名を付けて書くことにします。

type Pair = (,)
ListT m a <-> FreeT (Pair a) m ()

さて、モナドmを固定したとき、FreeT f m は、適当なFunctorであるfから別のFunctorであるFreeT f mを構成していると見なすことができます。

そのような性質の型コンストラクタmm、すなわちFunctor fに対してmm fもFunctorであるようなmmについて、 mm (Pair a) ()がMonadとして振る舞うような一般化、つまり

GeneralizedListT mm a <-> mm (Pair a) ()

として、GeneralizedListT mmがMonadになるよう、FreeTを一般化できないか、と考えると、 FFunctorとFMonadという抽象化にたどり着きます。

Trailモナド: FMonadから作ったMonad

以前、Functor上のモナドFMonadというものを紹介しました。

過去記事
上記記事の内容をHaskellのライブラリとして整理したものがGitHubにあります。本記事ではしばしばこのリポジトリ上のソースコードへのリンクを張ります。
- 見ればわかるように未完成(本記事投稿時点でのHEAD)ですし、Hackageには出していません

FFunctorとFMonadについておさらいします。FFunctorは、 Functorにおける関数の型 a -> b を自然変換 f ~> g = (∀x. f x -> g x) に置き換えたようなクラスです。つまり、Functor f が a -> b を f a -> f b に写すように、 FFunctor ffは g ~> h を ff g ~> ff h に写します。

type f ~> g = ∀x. f x -> g x

class (forall g. Functor g => Functor (ff g)) => FFunctor ff where
    ffmap :: (Functor g, Functor h) => (g ~> h) -> ff g x -> ff h x
    --    :: (Functor g, Functor h) => (g ~> h) -> (ff g ~> ff h)

FMonadは、同様に、Monadに対して関数を自然変換に置き換えたクラスです。

class FFunctor ff => FMonad ff where
    fpure :: Functor g => g ~> ff g
    fjoin :: Functor g => ff (ff g) ~> ff g

あるffがFMonadだからといって、ff gがMonadになったりはしないことに注意してください。以下の2組の操作はまったく別のことを意味しています。

-- FMonad ff のときできる操作
fpure :: g a -> ff g a
fjoin :: ff (ff g) a -> ff g a

-- Monad (ff g) のときできる操作
pure :: a -> ff g a
join :: ff g (ff g a) -> ff g a

しかし、FMonadからMonadを新たに作りだす方法があります。その方法の一つがTrailモナドです。（Control.Monad.Trail参照）

-- | Trail は FMonad をとって Monad を作る
type Trail :: ((Type -> Type) -> Type -> Type) -> Type -> Type
-- --          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^     ^^^^^^^^^^^^
--             FMonadのカインド                      |
--                                                Monadのカインド
newtype Trail mm a = Trail { runTrail :: mm (Pair a) () }

これを行う既存の概念はなさそうなので、勝手に命名しちゃいました。“trail”というのは野山を通る小道のことで、舗装されていない踏み跡が道になったようなイメージです。けもの道が”animal trail”ですね。このMonadをtrailと名付けた理由は、ListTの一般化である、という所からです。ListT m aは、 m ()の計算過程にa型のデータを足跡のようにつけて行ったものというイメージをしていたので、そこから取っています。

まず、Trail mmがFunctorであることを見てみます。Trail mm aは mm (Pair a) ()をラップした型なので、関数f :: a -> bに対してmm (Pair a) () -> mm (Pair b) ()という関数を作れればfmapになります。

instance (FFunctor mm) => Functor (Trail mm) where
    fmap f = Trail . ffmap (first f) . runTrail

ffmap (first f)は所望の型を持っていますね！ first fで、関数f :: a -> bを自然変換∀c. Pair a c -> Pair b cとして表してくれたおかげで、自然変換をとるffmapに渡せることがポイントです。

f               ::           a   ->      b
first f         :: ∀c. Pair a c -> Pair b c
first f         ::      (Pair a) ~> (Pair b)
ffmap (first f) ::   mm (Pair a) ~> mm (Pair b)

FMonad mmが与えられたとき、Trail mmがMonadになる理由も見てみましょう。

pureTrail :: FMonad mm => a -> Trail mm a
pureTrail a = Trail $ fpure (a,())

joinTrail :: FMonad mm => Trail mm (Trail mm a) -> Trail mm a
joinTrail = Trail . fjoin . ffmap (plug . first runTrail) . runTrail

plug :: forall f x. Functor f => Pair (f ()) x -> f x
plug (f_,a) = a <$ f_

instance FMonad mm => Applicative (Trail mm) where
    pure = pureTrail
    (<*>) = ap

instance FMonad mm => Monad (Trail mm) where
    ma >>= k = joinTrail (fmap k ma)

pureTrailの「型が合っている」様子は次の通りです。

(a, ())       ::     Pair a  ()
fpure (a, ()) :: mm (Pair a) ()
pureTrail a   :: Trail mm a

joinTrailは結構複雑です。1ステップずつ追っていくと、次のようになっています。

runTrail              :: Trail mm a -> mm (Pair a) ()
first runTrail        :: Pair (Trail mm a) ~> Pair (mm (Pair a) ())
plug                  ::                      Pair (f           ()) ~> f
plug . first runTrail :: Pair (Trail mm a)         ~>                  mm (Pair a)

let pf = plug . first runTrail -- 省略

pf               ::     Pair (Trail mm a)  ~>     mm (Pair a)
ffmap pf         :: mm (Pair (Trail mm a)) ~> mm (mm (Pair a))
fjoin            ::                           mm (mm f)        ~> mm f
fjoin . ffmap pf :: mm (Pair (Trail mm a))           ~>           mm (Pair a)
fjoin . ffmap pf :: mm (Pair (Trail mm a)) ()        ->           mm (Pair a) ()
joinTrail        :: Trail mm (Trail mm a)            ->           Trail mm a

この定義がMonad則を満たしている証明はここでは省略します。等式を並べただけの荒いものですが、証明はソースコード中にコメントとして残してあります。

ListT を FreeT から作れるか

さて、FMonadはListTをFreeTとして表すことの一般化を狙っていた、と言いました。実際にこれは達成できています。

FreeT f m aの引数fとmを入れ替えた型をFreeT'と定義します。

import qualified Control.Monad.Trans.Free as Original

newtype FreeT' m f b = WrapFreeT' { unwrapFreeT' :: Original.FreeT f m b }

mがMonadならばFreeT' mはFMonadになります。

instance Monad m => FMonad (FreeT' m)

したがって、Trail (FreeT' m) aもMonadになりますが、newtypeによる読み替えを外していけば

Trail (FreeT' m) a <-> FreeT' m (Pair a) ()
                   <-> FreeT (Pair a) m ()

となり、これはListT m aと同型なのでした。そして期待通りに、Monadとしても同じになるよう定義できています⁴。

Trail は ListT 以外にどんな Monad を作れるの？

FreeT' 以外の FMonad mm を入れてみて、 Trail mm がどのようなモナドになったか調べてみましょう。

Free (Freeモナド)

Trail Freeはリストモナド[]になります。

data Free f x = Pure x | Free (f (Free f x))

Trail Free a <-> Free (Pair a) ()
             <-> Either () (Pair a (Free (Pair a) ()))
             <-> Maybe (a, Trail Free a)

Ap (Free Applicative)

Trail Ap もリストモナド[]になります。
```
data Ap f a where
  Pure :: a -> Ap f a
  Ap   :: f a -> Ap f (a -> b) -> Ap f b
```
疑似コードですが、上の定義で Ap f () の場合を考えると、とても単純な形になることがわかります。
```
data Ap f () where
  Pure :: () -> Ap f ()
  Ap :: f a -> Ap f (a -> ()) -> Ap f ()
```
ここで a -> () は () と同型、存在量化された型変数 a は何も使いみちがないため任意の型を入れてよく、 a = ()を代入できます。すると
```
data Ap f () where
  Pure :: Ap f ()
  Ap :: f () -> Ap f () -> Ap f ()
```
これは[f ()]と完全に同じです。したがって、
```
Trail Ap a <-> Ap (Pair a) () <-> [Pair a ()] <-> [a]
```
となります。

Compose

Trail (Compose m) はモナドとしてはただの m になります。

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

Trail (Compose m) a
  <-> Compose m (Pair a) ()
  <-> m (Pair a ())
    = m (a, ())
  <-> m a

ComposePre

Trail (ComposePre m) a はモナドとしては Writer (m ()) になります。ここで m () は(>>) :: m () -> m () -> m () によってMonoidになっています。

newtype ComposePre g f x = ComposePre { getComposePre :: f (g x) }

Trail (ComposePre m) a
  <-> ComposePre m (Pair a) ()
  <-> Pair a (m ())
    = (a, m ())

この辺りはよく見知ったMonadしか出てきませんね。ですが複雑であまり見たことがないものも現れます。

ApT (Free Applicative Transformer⁵)
```
data ApT f g x =
    PureT (g x)
  | forall a b c. ApT (g a) (f b) (ApT f g c) (a -> b -> c -> x)
```
ApT は２通りの方法でFMonadになります。 1つ目はApT f gでfを固定してgを引数と見たとき、もう一つはgを固定してfを引数と見たときです。
```
instance Functor f => FMonad (ApT f)
instance Applicative g => FMonad (Flip1 ApT g)

newtype Flip1 t g f x = Flip1 { unFlip1 :: t g f x }
```
ApT の定義はやや複雑ですが、Apのときと同様、x = ()に限って考えると単純化できます。
```
data ApT f g () =
    PureT (g ())
  | ApT (g ()) (f ()) (ApT f g ())
```
これはg ()とf ()が交互に並んだリストになっています。つまり、以下のように定義されるAltList型を使って、 ApT f g () は AltList (f ()) (g ()) と同型になっています。
```
-- [b,a,b,a,...,b] と交互に並んだリスト
data AltList a b = Last b | Next b a (AltList a b)

-- 実際のHaskellではできませんが、ここでは、`AltList a b`をリストの記法で以下のように
-- 書いてよいことにします。
[b]             :: AltList a b
[b, a, b]       :: AltList a b
[b, a, b, a, b] :: AltList a b
-- ...
```
- Trail (ApT f) bは次のように「bとf ()とが交互に並んだリスト」と同型です。
```
[b, f (), b, f (), b, f (), ..., b] 
```
  Monadとしては、Monad (AltList a)というインスタンスにa = f ()とした場合になっています。このMonadがどのようなものか例を挙げると、
```
pure b = [b]
join [[b], a, [b,a,b,a,b], a, [b,a,b]]
    =  [ b,  a,  b,a,b,a,b,  a,  b,a,b ]
```
  のように、ネストしたAltList a (AltList a b)を平坦にする操作をjoinとするMonadです。
- もう一方のTrail (Flip1 ApT g) a は、 g ()とaが交互に並んだリストです。
```
[g (), a, g (), a, ..., g ()]
```
  Monadとしては、AltListの引数を入れ替えた
```
newtype AltList' b a = AltList' (AltList a b)
```
  が持つ、Monoid b => Monad (AltList' b)というインスタンスがベースになります。このモナドは次のような演算を持ちます。
```
pure a = [mempty, a, mempty]
join [b,  [b],  b,  [b, a, b, a, b],  b]
    =  [b <> b <> b <> b, a, b, a, b <> b]
```
  Trail (Filp1 ApT g)は、g ()をApplicativeを使ってMonoidとみなし、AltList' (g ())と同型になります。

さて、FreeTを使ってListTを作り出したとき、FreeT f mのmを固定してfを引数とみなしました。実は、fを固定してmを引数とみなしても、FreeTはFMonadになります。

instance Functor f => FMonad (FreeT f)

Trail (FreeT f) aはどのようなMonadでしょうか？t a = Trail (TreeT f) aと置いて定義を展開していくと次のようになります。

t a = Trail (FreeT f) a
 <-> FreeT f (Pair a) ()
 <-> Pair a (FreeF f () (FreeT f (Pair a) ()))
 <-> Pair a (FreeF f () (t a))
 <-> Pair a (Either () (f (t a)))
 <-> Pair a (Maybe (f (t a)))
   = (a, Maybe (f (t a)))
t a <-> (a, Maybe (f (t a)))

すなわち、以下のように定義された型がMonadになって、それがTrail (FreeT f)と同型になります。

data T f a = a :< Maybe (f (T f a))

このMonad、私は全く見たことがなかったので⁶、Tという味気ない一文字の代わりにEfreetという名前を勝手に付けてtwitterでやいのやいのしていました。この型はComonadにもなっているので、ちょっと面白かったんですよね。

理論的には面白いモナドなんですが、実用する機会は無いと言っていいと思います。↩︎
どれも事実上同じモナドを実装しています。実装方法の違いによる性能差はあるかもしれませんが私は検証していません。パッケージ間の主な違いはモナドを使いやすくするAPIです。↩︎
Monadとしての同型ではなく、ListT mのモナド演算とFreeT f mのモナド演算に直接の関係はありません。↩︎
同じになっていることの証明はhandwaveさせて下さい。ごめんなさい・・・↩︎
freeパッケージにも”Free Applicative Transformer”と呼ばれているもの（Control.Applicative.Trans.Free）が含まれますが、それとは異なります。↩︎
Twitterで”ちょっと違うけど似ているMonadを使ったことがあるよ”と教えていただきました(twitter)。この違いがどの程度影響しているのか等、自分はまだよく解っていませんので、理解が進んだらまた紹介するかもしれません。↩︎