TravelコモナドとFlowモナド

% basic set manipulation
  \gdef\id{\mathop{\mathrm{id}}}
  \gdef\comp{\circ}
  \gdef\placeholder{{-}}
  \gdef\setsum{\operatorname{\raisebox{-0.2em}{$\Large\Sigma$}}}
  \gdef\setprod{\operatorname{\raisebox{-0.2em}{$\Large\Pi$}}}
% category theory
  \gdef\Set{\mathrm{\mathbf{Set}}}
  \gdef\Cat{\mathrm{\mathbf{Cat}}}
  \gdef\Functors#1{\mathrm{\mathbf{Fun}}\left({#1}\right)}
  \gdef\Monads#1{\mathrm{\mathbf{Monads}}\left({#1}\right)}
  \gdef\Comonads#1{\mathrm{\mathbf{Comonads}}\left({#1}\right)}
  \gdef\CatC{\Cat^\sharp}
  \gdef\Ob{\mathop{\mathrm{Ob}}}
  \gdef\Mor{\mathop{\mathrm{Mor}}}
  \gdef\dom{\mathop{\mathrm{dom}}}
  \gdef\cod{\mathop{\mathrm{cod}}}
  \gdef\map{\mathop{\mathrm{map}}}
  \gdef\binprod{\mathbin{\Pi}}
  \gdef\bincoprod{\mathbin{\amalg}}
  \gdef\Id{\mathrm{Id}}
% custom notations
  \gdef\homset#1#2#3{{#1}\! \left\lbrack {#2}, {#3} \right\rbrack}
  \gdef\homsetl#1#2{{#1}\! \left\lbrack {#2} \right\rbrack}
  \gdef\asfunctor#1{\left. \llbracket {#1} \rrbracket^{c} \right.}
  \gdef\Cont{\mathrm{\mathbf{Cont}}}
  \gdef\Poly{\mathrm{\mathbf{Poly}}}
  \gdef\PolyFunctor#1{\mathrm{\mathbf{PFun}}\left({#1}\right)}
  \gdef\contcomp{\lhd}
  \gdef\inl{\operatorname{\mathtt{inl}}}
  \gdef\inr{\operatorname{\mathtt{inr}}}
  \gdef\divleft#1#2{\frac{{#1}, \_}{{#1}, {#2}}}
  \gdef\divright#1#2{\frac{\_, {#2}}{{#1}, {#2}}}
  \gdef\rootpos{o}
  \gdef\nextshape{\darr}
  \gdef\posplus{\oplus}
  \gdef\retroarr{\nrightarrow}
  \gdef\Travel{\operatorname{\mathrm{Travel}}}
  \gdef\Flow{\operatorname{\mathrm{Flow}}}

Travel: Categoryから作るComonad

以前、多項式コモナドと小さい圏の間に対応があるという論文の解説を行いました。 この記事では「小さい圏Cが与えられたとき、対応する多項式コモナドWを構成する方法」があることを暗黙に示しています。 この構成方法に名前をつけて明示的に書くことにしましょう。

(定義)コモナド\Travel_{C}

小さい圏Cに対して、C上のtravelコモナドを次の多項式コモナド\Travel_{C} : \Set \to \Setと定義する。

  \begin{align*}
    & \begin{aligned}
      & \Travel_{C} : \Set \to \Set \\
      & \Travel_{C} X = \setsum (c : \Ob(C)). \left(\homsetl{C}{c} \to X \right)
    \end{aligned} \\
    & \begin{aligned}
        & \operatorname{extract} : \forall \alpha. \Travel_{C}\alpha \to \alpha \\
        & \operatorname{extract} (c, f) = f \id_c \\
    \end{aligned} \\
    & \begin{aligned}
        & \operatorname{duplicate} : \forall \alpha. \Travel_{C}\alpha \to \Travel_{C}(\Travel_{C}\alpha)\\
        & \operatorname{duplicate} (c, f) = \left(c, \lambda p. (\cod p, \lambda q. f (p;q)) \right)
    \end{aligned}
  \end{align*}

さて、Haskellには圏を表す型クラスCategoryがありました。Haskell内でCategoryをもとにComonadを構成するような 型Travelは、標準のHaskellではありませんが、GHC拡張をふんだんに使って依存型を表すことで実現可能です。 実際に私が書いてみたものがこちらにあります: polynomial-functors/polynomial-comonad

-- https://github.com/viercc/polynomial-functor/blob/17404603235028fe9b10af72a0eaf96a01dae7c2/polynomial-comonad/src/Control/Comonad/Travel.hs

-- | Make 'Polynomial' 'Comonad' from 'Category'.
--
-- @Travel cat@ is a polynomial functor for any type constructor
-- @cat@.
--
-- @
-- Travel cat r ~ ∑a. ((∑b. cat a b) -> r)
-- @
--
-- @Travel cat@ is a @Comonad@ if @cat@ is a @Category@.
type Travel :: (k -> k -> Type) -> Type -> Type
data Travel (cat :: k -> k -> Type) r where
  MkTravel ::
    forall k (cat :: k -> k -> Type) (r :: Type) (a :: k).
    Sing a ->
    (Sigma k (TyCon (cat a)) -> r) ->
    Travel cat r

SingやSigmaといった型はsingletonsパッケージ由来です。 このsingletonsパッケージは、依存型がはじめから使える言語に存在する「依存積型(\setprod-型)」「依存和型(\setsum-型)」 に相当する型をHaskellで書くために必要な「singleton型」というテクニックに関する便利な機能を提供しています。

例えば、集合の依存積\setprod (i \in I). P(i)に相当する型を以下のProdPのように表すことができます。

type I :: Type
type P :: I -> Type

-- ProdP = Π(i ∈ I). P(i)
type ProdP = forall (i :: I). Sing i -> P i

Sing を用いずに以下のように定義してしまうと、依存積になりません。

type ForallP = forall (i :: I). P i

例えば、I = Boolであり、PはGADTを使って定義される以下のFooである場合を考えます。

data Foo (i :: Bool) where
  FooAny :: Foo i
  FooFalse :: Foo False
  FooTrue :: Foo True

Fooの依存積はΠ(i ∈ I) Foo(i) ~ (Foo False, Foo True)です。これは

(FooAny, FooAny) :: (Foo False, Foo True)
(FooFalse, FooTrue) :: (Foo False, Foo True)

のように、第一成分はFooAnyとFooFalseから、第二成分はFooAnyとFooTrueから任意に選んだ組の型です。 しかし、ForallPのようにforall i. Foo iという型がつく項はFooAnyしかありません。 Haskellには型変数に対するパターンマッチが存在しないので、型変数iが実際にとる型に依存する項 というものが書けないのです。しかし、Sing (i :: Bool)という型 の値レベルの引数に対してはパターンマッチが可能であり、以下のように書くことができます。

-- (FooFalse, FooTrue)に対応する依存積の値をSingを使って表現
prodValue :: forall (i :: Bool). Sing i -> Foo i
prodValue singI = case singI of
  SFalse -> FooFalse
  STrue -> FooTrue

同じように、集合の依存和\setsum (i \in I). P(i)に相当する型は¹

type SumP = Sigma' I P
data Sigma' k t where
  (:&:) :: Sing k -> t k -> Sigma' k t

として書くことができます。

Flow: Categoryから作るMonad

ComonadからMonadを作ることができるCoという型を以前紹介しました。

• Control.Monad.Coの正体

再掲すると、以下のように定義されるCo型を用いると、任意のComonad wに対してCo wはMonadになります。

newtype Co w = Co { runCo :: forall r. w (a -> r) -> r }
instance Functor f => Functor (Co f)
instance Comonad w => Applicative (Co w)
instance Comonad w => Monad (Co w)

前述した通り、Comonad wが多項式関手でもあった場合、wは適当なCategory catを用いて Travel catと同型なコモナドです。したがって、Co wはCo (Travel cat)と同型なモナドです。

では、Co (Travel cat)とはどのようなモナドなのか？ということが気になります。 Co (Travel cat)を同型な型に変形させていくと、Flowモナドを以下のように得ることができます。²

-- Control.Monad.Flow
-- https://github.com/viercc/polynomial-functor/blob/17404603235028fe9b10af72a0eaf96a01dae7c2/polynomial-comonad/src/Control/Monad/Flow.hs
-- より改変

newtype Flow (cat :: k -> k -> Type) x = MkFlow {
    runFlow :: forall (a :: k). Sing a -> (x, Sigma k (TyCon (cat a)))
  }
  deriving (Functor)

instance Category cat => Applicative (Flow cat) where
  pure x = MkFlow $ \sa -> (x, sa :&: id)
  (<*>) = ap

instance Category cat => Monad (Flow cat) where
  ma >>= k = MkFlow $ \sa ->
    case runFlow ma sa of
      (y, sb :&: f) -> case runFlow (k y) sb of
        (z, sc :&: g) -> (z, sc :&: (f >>> g))

以前の記事で、Co wというモナドはStateモナドの一般化StateLike m eと見做せる、と述べました。 特にwが多項式コモナドであり圏catを使って表現できる場合に、Co wと同型なFlow catモナドは、 よりはっきりとStateモナドとの対応をみることが可能です。

モナドState sにおいて、State s αという値の実体は、s -> (α, s)型の関数でした。特に言うと、 State s α型の値は、現在の状態s0 :: sが与えられると、そこでのモナドの実行結果x :: αと実行後の状態s1 :: sを返す関数でした。 一方、Flow catモナドでは、圏cat :: k -> k -> Typeの対象を”状態”、射を”状態遷移の経路”と呼ぶことにすると、Flow cat α型の値は、現在の”状態” a :: k が与えられると、そこでのモナドの実行結果x :: αと、 実行後の状態への”状態遷移の経路” f :: Σ(b :: k). (cat a b)を返す関数であると考えることができます。

すなわち、Flow catモナドは、catの対象を状態とするStateモナドのようなものであって、 遷移後の状態bだけでなく「どう遷移するか」を表すcatの射f :: cat a bも持っているものです。

ついでに、Stateモナドに対してStateTモナド変換子があるのと同じ調子で、 FlowモナドにもFlowTを考えることができます。

newtype FlowT (cat :: k -> k -> Type) m x = MkFlowT {
    runFlowT :: forall (a :: k). Sing a -> m (x, Sigma k (TyCon (cat a)))
  }
  deriving (Functor)

instance (Category cat, Monad m) => Applicative (FlowT cat m) where
  pure x = MkFlowT $ \sa -> pure (x, sa :&: id)
  (<*>) = ap

instance (Category cat, Monad m) => Monad (FlowT cat m) where
  mx >>= k = MkFlowT $ \sa ->
    do (y, sb :&: f) <- runFlowT mx sa
       (z, sc :&: g) <- runFlowT (k y) sb
       pure (z, sc :&: (f >>> g))

instance (Category cat) => MonadTrans (FlowT cat) where
  lift mx = MkFlowT $ \sa -> mx <&> \x -> (x, sa :&: id)

このFlowTの理論的背景は私はよくわかっていませんが、なんとなく「こうじゃないかな〜」と思っていることが

Flow catモナドを随伴に分解する方法のひとつに

Flow cat ~ U ∘ F
-- U :: (k -> Type) -> Type
-- F :: Type -> (k -> Type)

という型になるものがあって、FlowTは

FlowT cat m ~ U ∘ Compose m ∘ F
-- F         :: Type -> (k -> Type)
-- Compose m :: (k -> Type) -> (k -> Type)
-- U         :: Type -> (k -> Type)

としてMonadになっているんではないか？

というものです。