Haskellと随伴

随伴

随伴というのは2つの関手の関係のことです.
$ F : \mathcal{C} \to \mathcal{D} $, $ G : \mathcal{D} \to \mathcal{C} $があったとき, 随伴$F \dashv G$ とは, 自然同型 $\hom(F\cdot,\cdot) \cong \hom(\cdot,G\cdot)$ のことです(ただしこの同型はhomの左右を同時に固定して, 2変数引数としてみて考えます).

文章で読むより図式を見たほうが早いです.
コードにするのも簡単です.

class Adjunction f g where
  leftAd :: (f a -> b) -> (a -> g b)
  rightAd :: (a -> g b) -> (f a -> b)

-- Adjoint laws
-- 1. leftAd . rightAd = id
-- 2. rightAd . leftAd = id

随伴は圏論では重要な概念です.
そこでHaskellでの随伴について見ていきます.

例

(残念なことに)Haskellでの随伴の例はそこまで多くないです.
というのも, Haskellでよく見る関手(Maybe, List, Either aなど)には随伴が存在しないことが簡単に示せるからです. 随伴が存在しないことの証明についてはあとで少しだけやります.
数少ない例を紹介します.

Colimit -| Diagonal -| Limit

$\Delta : \mathcal{C} \to \mathcal{C}^\mathcal{J} ;; a \mapsto (\cdot \mapsto a)$
なる関手を, Diagonal functorといいます. $\Delta(a)$は全てをaにうつす定数関手です.

このとき $\mathrm{Colim}_J \dashv \Delta \dashv \mathrm{Lim} _{J} $ なる随伴があります.

例としては, 直積をlimitとして捉えます. $J=\mathbb{2}$ (離散2点圏)とすれば, $\Delta : \mathcal{C} \to \mathcal{C} \times \mathcal{C} ;; a \mapsto (a,a)$ とみなせます. このとき, $\hom_{\mathcal{C} \times \mathcal{C}}((a,a), (b,c)) \cong \hom_{\mathcal{C}}(a,b \times c)$
なる同型が随伴の例になっています.

Product -| Exponential

Haskellでは最もtypicalな例です. $s \times - \dashv (-)^s$ という形の随伴です. Haskellでexponentialはただのhomになるので, (,) s -| (->) s というやつです.

instance Adjunction ((,) s) ((->) s) where
  leftAd k a s = k (s,a)
  rightAd k (s,a) = k a s

Free -| Forgetful -| Cofree

ある構造を忘れる関手をForgetful functorといい, その右随伴をFree, 左随伴をCofreeといいます.
例としては適当な代数的構造の入った空間から底集合を取り出す関手($\bf{Mon} \to \bf{Set}$とか$\bf{Grp} \to \bf{Set}$など)が典型例です.
みんな大好きFree monadはこの意味でのFree functorです. つまり, "MonadとMonad準同型のなす圏" から "Functorと自然変換のなす圏" への忘却関手が標準的に定義されますが(全てのMonadはFunctorなので), これの左随伴がみんな大好きFree Monadです.

同型は $\hom_{\bf{Monad}}(\langle \text{Free f, return, join} \rangle, \langle b, \eta_b, \mu_b \rangle) \cong \hom_{\bf{Functor}}(\text{f}, b)$ です. (ただしfは任意のfunctor. 左辺はMonadの圏でのhomなのでmonad tripleの間の射. Free fはdata Free f a = Pure a | Free (f (Free f a))で定義されるmonad.)
右辺のhomはfunctor fからfunctor bへの自然変換なので, 上で定義したようなclass Adjunctionでは表現できません. Haskellで書くならleftAd, rightAdの型を少し変えて, 自然変換同士の対応を与えるようにする必要があります.

-- Functor(の構造を持つ)圏の間の随伴

class AdjunctionNat domCat codCat f g where
  leftAdNat :: (domCat a, codCat b) => (forall x. f a x -> b x) -> (forall x. a x -> g b x)
  rightAdNat :: (domCat a, codCat b) => (forall x. a x -> g b x) -> (forall x. f a x -> b x)

-- data Free f a = Pure a | Free (f (Free f a)) deriving (Functor)

newtype Forgetful (f :: * -> *) a = Forgetful { unForgetful :: f a } deriving (Functor)

instance AdjunctionNat Functor Monad Free Forgetful where
  leftAdNat p z = Forgetful $ p (Free $ fmap Pure z)
  rightAdNat p f0 = go f0 where
    go (Free fx) = join $ liftM go (unForgetful $ p fx)
    go (Pure x) = return x

Lan -| inverse -| Ran

Kan拡張が存在したとすると, それはinverse functor(関手の合成の順番を逆にしたfunctor; $F ^{-1} (p) = p \circ F$)の随伴になります.

newtype Inverse f p a = Inverse (p (f a)) deriving (Functor)
newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b } deriving (Functor)

instance AdjunctionNat Functor Functor (Inverse f) (Ran f) where
  leftAdNat p z = Ran $ \k -> p $ Inverse $ fmap k z
  rightAdNat p (Inverse z) = runRan (p z) id

Ranの定義についてはData.Functor.Kan.Ranを見てください. ここで, Ranは本来の右Kan拡張とは全然違う形をしているように見えますが, 実は$(-)^{-1} \dashv \rm{Ran}$の随伴からこのような形になることが分かります. Codensity Monadという記事で軽く触れたこともあるのでよければ参考にしてください.

モナドとの関連

モナドと随伴は関連します.
随伴があれば, 標準的な方法によってモナドとコモナドが構成できます. つまり,

命題 $F \dashv G$とする. このとき, $\langle GF, \eta, F\epsilon G \rangle$はmonadであり, $\langle FG, \epsilon, G\eta F \rangle$はcomonad.

ここで, $\eta : 1 \to GF$とは, 上のAdjunction型クラスの言葉を使えばleftAd idである, unit と呼ばれる自然変換です. $\epsilon : FG \to 1$はrightAd idで, __counit__と呼ばれます.(unit, counitから逆に随伴を構成することもできるので, これらは重要です.)

class Adjunction f g where
  leftAd :: (f a -> b) -> (a -> g b)
  rightAd :: (a -> g b) -> (f a -> b)

  unit :: a -> g (f a)
  unit = leftAd id

  counit :: f (g a) -> a
  counit = rightAd id

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

-- join = F . counit . G
join' :: (Functor f, Functor g, Adjunction f g) => Compose g f (Compose g f a) -> Compose g f a
join' = Compose . fmap (counit . fmap getCompose) . getCompose

instance (Functor f, Functor g, Adjunction f g) => Monad (Compose g f) where
  return = Compose . unit
  m >>= f = join' $ fmap f m

instance (Functor f, Functor g, Adjunction f g) => Comonad (Compose f g) where
  extract = counit . getCompose
  duplicate = Compose . fmap (fmap Compose . unit) . getCompose

そこで, 上で出てきた(,) s -| (->) sの随伴に対してこのモナドとコモナドの構成法を適用します. そうして得られるのが __Stateモナド, Storeコモナド__です.

-- State / Store

instance Adjunction ((,) s) ((->) s) where
  leftAd k a s = k (s,a)
  rightAd k (s,a) = k a s

type State s = Compose ((->) s) ((,) s)
type Store s = Compose ((,) s) ((->) s)

では逆に, (コ)モナドが与えられたら, そのモナドを与えるような, 元の随伴は復元できるでしょうか？
実は答えはYesで, しかもそのような方法は2通り知られています.
一つはT-algebra圏を使った構成法で, もうひとつはKleisli圏を使った構成法です. (ここでは述べませんが)

随伴の存在・非存在

随伴が存在することよりも, 存在しないことのほうが示すのが簡単なことが多いです.
例として, 上で(,) s -| (->) sの随伴関係があることを説明しましたが, (->) sは一般のsに対しては右随伴を持たないことを示してみましょう.

(Proof) (->) s -| G なる右随伴が存在したとする. このとき$\hom(a^s,b) \cong \hom(a, G b)$なる同型がある. ここで$a=1$(terminal object; Haskellで言うところのdata One = One)とすると, HaskはCCCだから, $\hom(1^s,b) \cong \hom(1,b) \cong b$ 及び $\hom(1,G b) \cong Gb$ より, $Gb \cong b$. すると$\hom(a^s,b) \cong \hom(a,b)$. よって(->) sが右随伴を持つのは$a^s \cong a$が任意の型aに対して成り立つときだけである. (qed)

また, 以下の定理は有用です.

定理 $F \dashv G$とする. このとき, Gはlimitを保ち, Fはcolimitを保つ.

コメント

Haskellでは随伴の例がほとんどないのであまり面白いことは発見できませんでした. 逆に, HaskellのFunctorは随伴を持たないことが多いので, 随伴が存在しないことを示す良い練習になるかもしれません.
Haskellで役に立つ場面があるとしたら, Ranのデータ型の導出みたいに, 型の間の同型を作ってそれをHaskellで使う, みたいな状況くらいしか今のところは思いつきません.
いずれにせよ何かの役に立つ日が来るといいなと思います. なお全ての概念はKan拡張なので随伴はKan拡張です. ありがとうございました.

参考文献

• http://alg-d.com/math/category/ 定義の確認用に
• CWM, Categories for the Working Mathematician 主にモナドのところを参照しました
• From Adjunction to Monads 随伴からモナドを作る構成法について
• 随伴がモテないのはどう考えてもモナドが悪い！（モナドとコモナドの関係が分かる話） Stateモナドを中心に, 随伴からモナドを導く話がもっと丁寧に書いてあります
• package kan-extensions LanとかRanとかCodensityが定義されてるパッケージ