Too lazy to evaluate - 随伴から作られるMonad(準備編)

\gdef\Set{\mathrm{\mathbf{Set}}} \gdef\Hask{\mathrm{\mathbf{Hask}}} \gdef\Vect{\mathrm{\mathbf{Vect}}} \gdef\Mon{\mathrm{\mathbf{Mon}}} \gdef\id{\mathrm{id}} \gdef\map{\mathrm{map}} \gdef\op#1{{#1}^{\mathrm{\scriptsize op}}}

前回まで、各種モナド/モナド変換子を理解するために、ストリング図という武器を使っていくつものモナドを見てきました。

State ーストリング図でMonad再入門(1)
StateT ーストリング図でMonad再入門(2)
WriterT, ReaderT, ExceptT ーストリング図でMonad再入門(3)

これら記事で使ったストリング図は、「抽象度を下げたもの」でした。つまり、ストリング図は実はもっと色々なものを表現できる記法です。第一回では次のように説明しました。

ストリング図が表すものは、Functorの間の自然変換です。改めて明示的に定義するなら、 Functor fとFunctor gに対して、型∀a. f a -> g aが付くような関数が、fからgへの自然変換です。

ストリング図は、Functor間の自然変換を表すと書きました。しかし、実はどんな関手の間の自然変換でもよかったのです。

今度は、Functor以外の関手を使って、次のモナドを分析していこうと思います。

Cont (Control.Monad.Trans.Cont)
ListT m (Control.Monad.Trans.List, “ListT done wrong”)

ただ、関手とは何か、自然変換とは何か、という説明を端折ったままここまで来てしまいました。このブログではまだきちんと書いていませんでしたので、この記事ではまず圏論の最序盤あたりを説明します。

私のつたない説明で伝えられるのはほんの一部なので、以下の参考図書のような教科書にあたってくれたらそれが一番です。

Category Theory (Oxford Logic Guides)
- 定評のある教科書（らしい）
- 日本語訳圏論第2版もあるけど、数学的内容に影響のある誤訳が結構な数あるので、正誤表を探しておいて覚悟して読むべし
ベーシック圏論普遍性からの速習コース
- こちらも定評のある教科書（らしい）
- これも日本語訳だけど翻訳の正確さは信頼できるそうです
Category Theory for Programmers
- 英語、新し目、pdfは無料
- （紙の本を日本から買うやりかたがわからない）
- プログラミングでの実例豊富

圏、関手、自然変換

圏

どんなものを圏と呼ぶのかから始めます。

ある記号Cについて、「Cが圏(Category)である」ことを、次のように定義します。

Cが圏であるとは、
- 対象と呼ばれるものを（通常たくさん）持っている。
- 射と呼ばれるものを（通常たくさん）持っている。Cの射fは、それぞれCの2つの対象間をつなぐ矢印のようなもので、その矢印が出る対象aと矢印が向かう対象bが決まっている。
  - aから出てbに向かう射の集まりが集合になっていないこともあるが、ここではそんな圏は考えない。C(a,b)でそのような射の集合を表すことにする。
- 任意の対象aについて、aから出てそのままaに入る射 \id_a \in C(a,a)を持っている。
  - この射は恒等射と呼ぶ。
- 任意の二つの射f,gについて、gの行き先の対象とfの出元の対象が同じであるとき、これらを合成した射f\circ gも存在する。
  - より詳しく言うなら、f \in C(b,c)とg \in C(a,b)に対して、 f \circ g \in C(a,c)を決める二項演算\circを、すべての対象の組み合わせa,b,cについて持っている。
- 射に恒等射を合成しても変化しない。
  - 任意の射f \in C(a,b)についてf \circ \id_a = \id_b \circ f = f
- 射の合成は結合法則に従っている。
  - 任意の3つの射f,g,hがあってf\circ gもg\circ hも定義できるとき、 (f \circ g) \circ h = f \circ (g \circ h)

これらは、集合と写像を一般化したものです。なので、圏の一番はじめの例は集合と写像の圏\Setです。

圏\Set
- \Setの対象は集合である。
- \Setの射は関数である。集合aを定義域、集合bを値域とする関数を、 aから出てbに入る射と考える。
  - そのような関数の集合として\Set(a,b)をとることができる。
- 集合a上の恒等関数\id_aと関数の合成が、そのまま恒等射と射の合成である。
- 「関数に恒等関数を合成しても変化しない」「関数の合成は結合法則に従っている」は明らか。（むしろ、この規則が関数の合成を一般化しようとして決められている。）

数学では「何らかの演算を備えた集合」と、「演算を保つ写像」を考えることがよくあります。例えば体k上のベクトル空間は足し算、引き算、そしてスカラー倍ができる集合で、これらの演算がベクトル空間の公理を満たすものです。ベクトル空間の間の線形写像は、足し算、ゼロ、…といった演算を保つ写像です。

こういった「演算を備えた集合」と「演算を保つ写像」からなる圏を考えることもよくあります。

体k上のベクトル空間の圏k\Vect
- k\Vectの対象はkベクトル空間V
- k\Vectの射は線形写像
モノイドの圏\Mon
- \Monの対象はモノイド
- \Monの射はモノイド準同型

また、Haskellの型と関数も、\Setにそっくり似た圏になります¹。よく\Haskと呼ばれる圏です。

\Hask
- \Haskの対象は型（詳しく言えば、型変数のない具体的に一つ決まった型）
- \Haskの射は関数です。A -> B型の関数を、 Aから出てBに入る射と考える
- 恒等関数idと関数の合成(.)を、そのまま恒等射と射の合成とする
- 「関数に恒等関数を合成しても変化しない」「関数の合成は結合法則に従っている」を満たしている

これはHaskellで書いてあったほうが理解しやすいかもしれません。Control.Categoryに、圏を定義するための型クラスCategoryがあります。

-- Control.Category
class Category cat where
  -- 恒等射
  id :: cat a a
  -- 射の合成
  (.) :: cat b c -> cat a b -> cat a c

type Hask = (->)
instance Category Hask where
  id :: Hask a a   --   a -> a
  id = \x -> x

  (.) :: Hask b c -> Hask a b -> Hask a c
      -- (b -> c) -> (a -> b) -> (a -> c)
  f . g = \x -> f (g x)

\Haskの射を逆向きにした圏\op\Haskというものも考えられます。つまり、 A -> BをBからAに向かう射とした圏です。 GHCのbaseパッケージにはこの圏がすでに実装されていて、 Data.Functor.Contravariant.Opにあります。

newtype Op b a = Op (a -> b)

instance Category Op where
  id :: Op a a
  id = Op id

  (.) :: Op b c   -> Op a b   -> Op a c
      -- (c -> b) -> (b -> a) -> (c -> a)
  Op f . Op g = Op (g . f)

一般に、どんな圏Cに対しても、すべての射の向きを反対にすることで得られる圏\op{C}があります。これもHaskellで書けば次のようになります。

-- C^{op}
newtype Opposite cat a b = Opposite (cat a b)

instance Category cat => Category (Opposite cat) where
  id :: Opposite cat a a
  id = Opposite id
  
  (.) :: Opposite cat b c -> Opposite cat a b -> Opposite cat a c
  Opposite f . Opposite g = Opposite (g . f)
    -- f :: cat c b
    -- g :: cat b a
    -- g . f :: cat c a

Opは実質的にOpposite Haskです。

Haskellでの例をもう一つ挙げると、a -> Maybe bの形をした関数を射とする圏Partialを考えることができます。

-- | "部分関数"@a -> Maybe b@を射とする圏
newtype Partial a b = Partial { runPartial :: a -> Maybe b }

instance Category Partial where
  id :: Partial a a
  id = Partial return

  (.) :: Partial b c -> Partial a b -> Partial a c
  Partial f . Partial g = Partial $ f <=< g

関手

関手(functor)とは、二つの圏C, Dに対して、次の二つを合わせたものです。

Cの対象xをDの対象Fxに対応させるF
Cの射g \in C(a,b)をDの射\map_F(g) \in D(Fa,Fb)に写す関数\map_F

ただし、以下の等式を満たしている必要があります。

\map_Fは、Cの恒等射\id_xをDの恒等射\id_{Fx}に写す。すなわち

\map_F(\id_x) = \id_{Fx}
\map_Fは、Cの射g,hの合成g\circ hをDに写しても保つ。すなわち

\map_F(g \circ h) = \map_F(g) \circ \map_F(h)

Haskellの型クラスFunctorは、関手全般を表しておらず、 \Haskから\Haskへの関手のための型クラスになっています。

Functor fは、fが型aを型f aに対応させる型コンストラクタであるときに宣言できる。

\Haskの対象は型なので、\Haskの対象aを\Haskの対象f aに対応させているとも読み替えられる。
Functor fならば、fmap :: (a -> b) -> (f a -> f b)を持つ。これは、fmap :: Hask a b -> Hask (f a) (f b)といっても同じである。つまり、fmapは\Haskの射を\Haskの射にうつす関数である。
Functor則は、関手であるための条件そのものである。
- fmap id = id
- fmap (f . g) = fmap f . fmap g

関手を表すクラスは他にもあります。baseパッケージのContravariantクラス（Data.Functor.Contravariant）は、 \op\Haskから\Haskへの関手のための型クラスといえます。

class Contravariant f where
  contramap :: (a' -> a) -> f a -> f a'

Contravariant fは、fが型aを型f aに対応させる型コンストラクタであるときに宣言できる。

\Haskの対象も\op\Haskの対象も型なので、\op\Haskの対象aを\Haskの対象f aに対応させているとも読み替えられる。
Contravariant fならば、contramap :: (a' -> a) -> f a -> f a'を持つ。これは、newtypeを無視すれば、contramap :: Op a a' -> Hask (f a) (f a')といっても同じである。つまり、contramapは\op\Haskの射を\Haskの射にうつす関数である。
Contravariant則は、関手であるための条件そのものである。
- contramap id = id
- contramap (g . f) = contramap f . contramap g

Partialから\Haskへの関手も当然考えられます。3rd partyなライブラリにある型クラス Filterable ² は、そのような関手の型クラスと見なせます。

class Filterable t where
  mapMaybe :: (a -> Maybe b) -> t a -> t b
           -- Partial a b    -> Hask (t a) (t b)

Functorが合成できたように、一般の関手も合成関手を作ることができます。これはほぼFunctorの合成（Data.Functor.Compose）そのまま、どの圏のあいだの関手なのかが一般化されただけです。

Fが圏Dから圏Eへの関手、Gが圏Cから圏Dへの関手のとき、 CからEへの関手F\circ Gが定義できます。

Cの対象aに対して、Eの対象(F\circ G)a=F(Ga)を対応させます。
Cの射に対してEの射を与える関数\map_{F\circ G}を、\map_{F\circ G}(f)=\map_F(\map_G(f)) と定義します。

自然変換

圏Cから圏Dへの関手がふたつ、F,Gとあったとします。自然変換を次のように定義します。

自然変換tとは、すべてのCの対象aについてそれぞれ選ばれた Dの射t_a \in D(Fa, Ga)の族であって、次の条件を満たすものである。
- 任意のCの射f \in C(a,b)に対して、t_b \circ \map_F(f) = \map_G(f) \circ t_aが成り立つ

Haskell脳を働かせて、添字を全部省略して”型推論”してよいことにすると、 t \circ \map(f) = \map(f) \circ tと略記できます。

Functorに限定した場合、つまり\Haskから\Haskへの関手F,Gについての場合、次のようになります。

自然変換tとは、すべての型aについて定義されている関数t :: forall a. F a -> G aであって、次の条件を満たすものである。
- 任意の関数f :: a -> bに対して、t . fmap f = fmap f . tが成り立つ

ストリング図の解説をしたときは、自然変換を次のように説明していました。

ストリング図が表すものは、Functorの間の自然変換です。改めて明示的に定義するなら、 Functor fとFunctor gに対して、型∀a. f a -> g aが付くような関数が、fからgへの自然変換です。

この説明には、「任意の関数f :: a -> bに対して、t . fmap f = fmap f . tが成り立つ」の部分がありません。しかし、これは間違っていません。Haskellの特殊な事情³によって、あらゆるt :: forall a. f a -> g aは、t . fmap f = fmap f . tを満たします⁴。

これはあくまでHaskellの特殊な事情で、しかもFunctorに限ったことなので、 Functor以外の関手についてはきちんと確認する必要があります。 \Monといった代数的構造の圏が関係する場合はもちろん、 Haskellでプログラムとして定義した圏でも、Functor以外でこれが成り立たないことがあります。特に、Partialから\Haskへの関手Filterableについては成り立ちません。

instance Filterable [] where
    mapMaybe = Data.List.mapMaybe

instance Filterable Maybe where
    mapMaybe f = (>>= f)

instance Filterable (Const c) where
    mapMaybe _ (Const c) = Const c

-- reverseは、[]をPartialからHaskへの関手と見たとき自然変換である。
-- つまり、
--   mapMaybe f . reverse = reverse . mapMaybe f
-- が成り立つ。
reverse :: [a] -> [a]
reverse = Data.List.reverse

-- Functorのように、`forall a.`が付いているだけで自然変換になるだろうか？
-- それは、任意の (t :: forall a. f a -> g a) について以下の式が成り立つ
-- という主張である。
--   mapMaybe f . t = t . mapMaybe f
-- 
-- しかし明らかに以下の式は成り立たない。
--   mapMaybe f . length' = length' . mapMaybe f
length' :: [a] -> Const Int a
length' as = Const (length as)

Functorとは限らない関手の話題では、自然変換と思っていた関数が length'のような”ジェネリックだけど自然じゃない変換”になっていないか、注意を払う必要があります。

つづく

実はならないのだけれど、無限ループやundefinedのような停止しないことがある式に関係してのことなので、多目に見てください↩︎
残念ながらFilterableや同等の型クラスを提供するライブラリは統一されずに複数あって、これは私が好きなやつです↩︎
Theorems for free!, Wadler 1989

単純型付きラムダ計算で”任意の型aについて・・・という型が付く項はこんな性質を満たして・・・” という類の定理があって、Haskellの型システムはこの性質(parametricity)を崩さないように設計されています。↩︎
ただし、Functor f, Functor gがきちんとFunctor則を満たしている場合に限ります↩︎