Haskell/圏論のソースを表示

{{Haskell minitoc|chapter=Wider Theory}}

この項目では Haskell に関連する内容に限って圏論の概観を与えることを試みる。そのために、数学的な定義に併せて Haskell コードも示す。絶対的な厳密さは求めない。そのかわり、圏論の概念とはどんなものか、どのように Haskell に関連するかの直感的な理解を読者に与えることを追求する。<!-- This article attempts to give an overview of category theory, in so far as it applies to Haskell. To this end, Haskell code will be given alongside the mathematical definitions. Absolute rigour is not followed; in its place, we seek to give the reader an intuitive feel for what the concepts of category theory are and how they relate to Haskell. -->

== 圏の導入 <!-- Introduction to categories --> ==
[[Image:Simple-cat.png|left|frame|３つの対象''A'', ''B'', ''C''、３つの恒等射<math>\mathit{id}_A</math>, <math>\mathit{id}_B</math>, <math>\mathit{id}_C</math>と、さらに別の射<math>f : C \to B</math>, <math>g : A \to B</math>からなる単純な圏。３つめの要素(どのように射を合成するかの定義)は示していない。]]
<!-- [[Image:Simple-cat.png|left|frame|A simple category, with three objects ''A'', ''B'' and ''C'', three identity morphisms <math>\mathit{id}_A</math>, <math>\mathit{id}_B</math> and <math>\mathit{id}_C</math>, and two other morphisms <math>f : C \to B</math> and <math>g : A \to B</math>. The third element (the specification of how to compose the morphisms) is not shown.]] -->

本質的に、圏とは単純な集まりである。これは次の３つの要素からなる。
<!-- A category is, in essence, a simple collection. It has three components: -->

* '''対象'''(Object)の集まり。
* ふたつの対象('''source object'''と'''target object''')をひとつに結びつける'''射'''の集まり。(これらは'''arrow'''と呼ばれることもあるが、Haskellではこれは別の意味を持つ用語なので、ここではこの用語を避けることにする。) ''f'' がソースオブジェクト ''A'' からターゲットオブジェクト ''B'' への射であるとき、これを <math>f : A \to B</math> と書く。
* これらの射の'''合成'''の概念。 ''h'' が射 ''f'', ''g'' の合成であるとき、これを <math>h = f \circ g</math> と書く。
<!-- 
* A collection of '''objects'''.
* A collection of '''morphisms''', each of which ties two objects (a ''source object'' and a ''target object'') together. (These are sometimes called '''arrows''', but we avoid that term here as it has other connotations in Haskell.) If ''f'' is a morphism with source object ''A'' and target object ''B'', we write <math>f : A \to B</math>.
* A notion of '''composition''' of these morphisms. If ''h'' is the composition of morphisms ''f'' and ''g'', we write <math>h = f \circ g</math>. -->
様々なものが圏をつくる。例えば、'''Set''' は全ての集合を対象とし、射として標準的な関数、合成として通常の関数合成を持つ圏である。(圏の名前はしばしば太字で表される。)'''Grp'''は全ての群を対象とし、射として群の演算を保存する関数(群準同型)を持つ圏である。つまり、任意の2つの群 ''G'', ''H'' (それぞれ演算<math>*</math>, <math> \cdot </math>をもつ)について、
<math>f(u * v) = f(u) \cdot f(v)</math>ならば、かつそのときに限り、<math>f : G \to H</math> は '''Grp''' 内の射である。
<!-- Lots of things form categories. For example, '''Set''' is the category of all sets with morphisms as standard functions and composition being standard function composition. (Category names are often typeset in bold face.) '''Grp''' is the category of all groups with morphisms as functions that preserve group operations (the group homomorphisms), i.e. for any two groups ''G'' with operation ''*'' and ''H'' with operation ''·'', a function <math>f : G \to H</math> is a morphism in '''Grp''' iff:

: <math>f(u * v) = f(u) \cdot f(v)</math> -->

射はいつも関数のようにも思えるが、そうである必要はない。例えば、いかなる半順序 (''P'', <math>\leq</math>)も圏を定義する。ここで対象は''P''の要素であり、任意の2つの対象''A'', ''B''について<math>A \leq B</math>であるときかつそのときに限り''A''と''B''の間に射が存在する。また、複数の異なる射が同じソースオブジェクトとターゲットオブジェクトを持つことができる。'''Set'''の例でいえば、<math>\sin</math> と <math>\cos</math> はいずれもソースオブジェクト<math>\mathbb{R}</math> と ターゲットオブジェクト <math>[-1,1]</math>をもつが、もちろんこれらは同じ射ではない！

<!-- It may seem that morphisms are always functions, but this needn't be the case. For example, any partial order (''P'', <math>\leq</math>) defines a category where the objects are the elements of ''P'', and there is a morphism between any two objects ''A'' and ''B'' iff <math>A \leq B</math>. Moreover, there are allowed to be multiple morphisms with the same source and target objects; using the '''Set''' example, <math>\sin</math> and <math>\cos</math> are both functions with source object <math>\mathbb{R}</math> and target object <math>[-1,1]</math>, but they’re most certainly not the same morphism! -->

=== カテゴリ則 <!-- Category laws --> ===

圏が従わなければならない規則が３つ存在する。最初に、非常に単純だが、射の合成は'''''結合的'''''である必要がある。つまり、

: <math>f \circ (g \circ h) = (f \circ g) \circ h</math>

次に、圏は合成演算において'''閉じて'''いなければならない。すなわち、もし<math>f : B \to C</math> かつ <math>g : A \to B</math>ならば、<math>h = f \circ g</math>のような射<math>h : A \to C</math>がその圏に存在しなければならない。次の圏を使えば、これがどのように働くかを見ることができる。

[[Image:Composition-ex.png|center]]

''f'' と ''g'' はどちらも射であるので、これらを合成したらこの圏にあるいずれかの射を得るはずである。では、どれが射<math>f \circ g</math>だろうか？唯一の答えは<math>\mathit{id}_A</math>である。同様に<math>g \circ f = \mathit{id}_B</math>もわかる。

最後に、いかなる対象 ''A'' についても'''''恒等'''''射<math>\mathit{id}_A : A \to A</math>、すなわちその射との合成が恒等であるような射が圏 ''C'' に存在しなければならない。正確に言えば、任意の射 <math>g : A \to B</math> に対して 

: <math>g \circ \mathit{id}_A = \mathit{id}_B \circ g = g</math>

である。

<!-- There are three laws that categories need to follow. Firstly, and most simply, the composition of morphisms needs to be '''''associative'''''. Symbolically,

: <math>f \circ (g \circ h) = (f \circ g) \circ h</math>

Secondly, the category needs to be '''''closed''''' under the composition operation. So if <math>f : B \to C</math> and <math>g : A \to B</math>, then there must be some morphism <math>h : A \to C</math> in the category such that <math>h = f \circ g</math>. We can see how this works using the following category:

[[Image:Composition-ex.png|center]]

''f'' and ''g'' are both morphisms so we must be able to compose them and get another morphism in the category. So which is the morphism <math>f \circ g</math>? The only option is <math>\mathit{id}_A</math>. Similarly, we see that <math>g \circ f = \mathit{id}_B</math>.

Lastly, given a category ''C'' there needs to be for every object <code>A</code> an '''''identity''' morphism'', <math>\mathit{id}_A : A \to A</math> that is an identity of composition with other morphisms. Put precisely, for every morphism <math>g : A \to B</math>:

: <math>g \circ \mathit{id}_A = \mathit{id}_B \circ g = g</math> -->

=== Haskell の圏 '''Hask''' <!-- '''Hask''', the Haskell category --> ===

この項目で我々が考えようとしている主な圏は、Haskellの型を対象とし、Haskell の関数を射とし、合成として<code>(.)</code>を使う圏 '''Hask''' である。型 <code>A</code> から <code>B</code>の関数 <code>f :: A -> B</code> は '''Hask''' の射である。
この定義が最初の2つの規則を満たすことは容易に確認できる。
すなわち<code>(.)</code> は結合的であり、また任意の <code>f</code> と <code>g</code>について <code>f . g</code> は明らかに何らかの関数である。'''Hask''' における恒等射は <code>id</code> であり、次は自明である。
<ref>実はここには微妙な部分が存在する。<code>(.)</code>は遅延評価関数であるため、もし<code>f</code> が <code>undefined</code>であると<code>id . f = \_ -> _|_</code>となる。さて、全ての意図と目的においてこれは<code>_|_</code>と等しいように見えるかもしれないが、実は正格化関数<code>seq</code>を使うことでこれらを区別することができる。これは圏の最後の規則が破られることを意味する。新たに正格な合成関数<code>f .! g = ((.) $! f) $! g</code>を定義すれば'''Hask'''を正しく圏にすることもできる。しかしここでは普通の<code>(.)</code>を使って進めていくことにする。全ての矛盾は
<code>seq</code>が良い言語の性質をひどく破壊するということのせいにしておく。</ref>

<!-- The main category we’ll be concerning ourselves with in this article is '''Hask''', the category of Haskell types and Haskell functions as morphisms, using <code>(.)</code> for composition: a function <code>f :: A -> B</code> for types <code>A</code> and <code>B</code> is a morphism in '''Hask'''. We can check the first and second law easily: we know <code>(.)</code> is an associative function, and clearly, for any <code>f</code> and <code>g</code>, <code>f . g</code> is another function. In '''Hask''', the identity morphism is <code>id</code>, and we have trivially: -->

: <code>id . f = f . id = f</code>

<!-- <ref>Actually, there is a subtlety here: because <code>(.)</code> is a lazy function, if <code>f</code> is <code>undefined</code>, we have that <code>id . f = \_ -> _|_</code>. Now, while this may seem equivalent to <code>_|_</code> for all intents and purposes, you can actually tell them apart using the strictifying function <code>seq</code>, meaning that the last category law is broken. We can define a new strict composition function, <code>f .! g = ((.) $! f) $! g</code>, that makes '''Hask''' a category. We proceed by using the normal <code>(.)</code>, though, and attribute any discrepancies to the fact that <code>seq</code> breaks an awful lot of the nice language properties anyway.</ref> -->

ただし、これは添え字を欠いてしまっており、上記の規則の厳密な翻訳ではない。Haskell の関数 <code>id</code> は ''多相的''である。すなわちその定義域や値域に異なる様々な型をとることができる、もしくは圏で言い換えれば、異なるソース及びターゲットオブジェクトをとることができる。しかし圏論における射は''単相的''である。すなわちどんな射もソースオブジェクトとターゲットオブジェクトを1つずつ指定して定義される。多相な Haskell 関数はその型を明示することによって単相化することができる(単相型による''インスタンス化'')ため、『'''Hask'''圏の型<code>A</code>に対する恒等射は<code>(id :: A -> A)</code>である』と書けばより正確になる。これを考慮すると、先程の則は次のように書き直せる。

<!-- This isn't an exact translation of the law above, though; we’re missing subscripts. The function <code>id</code> in Haskell is ''polymorphic'' - it can take many different types for its domain and range, or, in category-speak, can have many different source and target objects. But morphisms in category theory are by definition ''monomorphic'' - each morphism has one specific source object and one specific target object. A polymorphic Haskell function can be made monomorphic by specifying its type (''instantiating'' with a monomorphic type), so it would be more precise if we said that the identity morphism from '''Hask''' on a type <code>A</code> is <code>(id :: A -> A)</code>. With this in mind, the above law would be rewritten as: -->

: <code>(id :: B -> B) . f = f . (id :: A -> A) = f</code>

しかしながら議論を単純にするため、意味が明らかであるときはこの違いを無視することにする。
<!-- However, for simplicity, we will ignore this distinction when the meaning is clear. -->

{{Exercises|
*さきほど触れたとおり、任意の半順序 (''P'', <math>\leq</math>) は''P''の要素を対象、要素 ''a'' と ''b'' について a <math>\leq</math> b であるときかつそのときに限り''a, b''間に射をもつ圏である。上記の規則のどれがこの<math>\leq</math>の推移性を保証しているか？
*(難しい) もし上記の例に別の射を付け足すとこれは圏ではなくなる。なぜか？ヒント：合成演算の結合性を考えてみよ。[[Image:Not-a-cat.png|center]]}}

<!-- {{Exercises|
* As was mentioned, any partial order (''P'', <math>\leq</math>) is a category with objects as the elements of ''P'' and a morphism between elements ''a'' and ''b'' iff a <math>\leq</math> b. Which of the above laws guarantees the transitivity of <math>\leq</math>?
* (Harder.) If we add another morphism to the above example, it fails to be a category. Why? Hint: think about associativity of the composition operation.
[[Image:Not-a-cat.png|center]]}} -->

== 関手 <!-- Functors --> ==

[[Image:Functor.png|frame|right|ふたつの圏<math>\mathbf{C}</math> と <math>\mathbf{D}</math> の間の関手。対象の対応は黄色の、射の対応は青色の破線矢印で示した。注目すべきは対象 ''A'' と対象 ''B''の両方が <math>\mathbf{D}</math> の同じ対象に対応付けられていることである。それゆえ ''g'' はソースとターゲットが同じ対象である射に変換され(これは恒等射である必要はない)、<math>id_A</math> と <math>id_B</math>は同じ射となる。]]

<!-- 
[[Image:Functor.png|frame|right|A functor between two categories, <math>\mathbf{C}</math> and <math>\mathbf{D}</math>. Of note is that the objects ''A'' and ''B'' both get mapped to the same object in <math>\mathbf{D}</math>, and that therefore ''g'' becomes a morphism with the same source and target object (but isn't necessarily an identity), and <math>id_A</math> and <math>id_B</math> become the same morphism. The arrows showing the mapping of objects are shown in a dotted, pale olive. The arrows showing the mapping of morphisms are shown in a dotted, pale blue.]] -->

対象と対象を関連付ける射を持つ幾つかの圏を見てきた。圏論の次の大きな話題は圏どうしを関連づける'''関手'''(functor、ファンクタ)である。関手の本質は圏の間の変換である。つまり圏''C'' と ''D''が与えられたとき、関手 <math>F : C \to D</math>は次のことをする。
<!-- So we have some categories which have objects and morphisms that relate our objects together. The next Big Topic in category theory is the '''functor''', which relates categories together. A functor is essentially a transformation between categories, so given categories ''C'' and ''D'', a functor <math>F : C \to D</math>: -->

* ''C'' 内のあらゆる対象 ''A''を、''D''内の<math>F(A)</math>に対応付ける
* ''C'' 内の射 <math>f : A \to B</math> を ''D'' 内の <math>F(f) : F(A) \to F(B)</math> に対応付ける
<!-- * Maps any object ''A'' in ''C'' to <math>F(A)</math>, in ''D''.
* Maps morphisms <math>f : A \to B</math> in ''C'' to <math>F(f) : F(A) \to F(B)</math> in ''D''. -->

関手の好例のひとつは忘却関手(forgetful functor) <math>\mathbf{Grp} \to \mathbf{Set}</math> である。これは群をその内在する集合に対応付け、群の射を同様に振る舞うがしかし群の代わりに集合の上で定義される関数に対応付ける。他の例としては冪集合関手 <math>\mathbf{Set} \to \mathbf{Set}</math> がある。これは集合をその冪集合に対応付け、関数 <math>f : X \to Y</math> を関数 <math>\mathcal{P}(X) \to \mathcal{P}(Y)</math>、つまり <math>U \subset X</math> をとり <math>f(U) = \{ \, f(u) | u \in U \, \}</math> と定義される、 ''f'' の下の ''U'' の像を返す関数にそれぞれ対応付ける。あらゆる圏 ''C'' について、''C''上の恒等関手として知られる関手、すなわち対象や射をそれ自身に対応付ける、<math>1_C : C \to C</math>を定義できる。これは後の[[#モナド則とその重要性|モナド則]]の節で便利であることがじきにわかるであろう。　

<!-- One of the canonical examples of a functor is the forgetful functor <math>\mathbf{Grp} \to \mathbf{Set}</math> which maps groups to their underlying sets and group morphisms to the functions which behave the same but are defined on sets instead of groups. Another example is the power set functor <math>\mathbf{Set} \to \mathbf{Set}</math> which maps sets to their power sets and maps functions <math>f : X \to Y</math> to functions <math>\mathcal{P}(X) \to \mathcal{P}(Y)</math> which take inputs <math>U \subset X</math> and return <math>f(U)</math>, the image of ''U'' under ''f'', defined by <math>f(U) = \{ \, f(u) : u \in U \, \}</math>. For any category ''C'', we can define a functor known as the identity functor on ''C'', or <math>1_C : C \to C</math>, that just maps objects to themselves and morphisms to themselves. This will turn out to be useful in the [[#The monad laws and their importance|monad laws]] section later on. -->

関手が従わなければならない幾つかの公理を挙げておこう。最初に、任意の対象 ''A'' 上の恒等射 <math>id_A</math> について、<math>F(id_A)</math> は恒等射でなければならない。

<!-- Once again there are a few axioms that functors have to obey. Firstly, given an identity morphism <math>id_A</math> on an object ''A'', <math>F(id_A)</math> must be the identity morphism on <math>F(A)</math>, i.e.: -->

: <math>F(id_A) = id_{F(A)}</math>

ふたつめに、関手は射の合成を分配しなければならない。
<!-- Secondly functors must distribute over morphism composition, i.e. -->

: <math>F(f \circ g) = F(f) \circ F(g)</math>

{{Exercises|右の図において、関手の規則が成り立ってることを確かめよ。}}
<!-- {{Exercises|For the diagram given on the right, check these functor laws.}} -->

=== '''Hask'''における関手 <!-- Functors on '''Hask''' --> ===
Haskellでお目にかかったことがあるかもしれない型クラス Functor は、実際に圏論における関手の概念と一致する。関手がふたつの構成要素からなることを思い出そう。関手はある圏の対象を別の圏の対象に対応付け、最初の圏の射をふたつめの圏の射に対応付ける。Haskell の関手は '''Hask''' から ''func''である。ここで ''func'' は関手の型の上でちょうど定義される''Hask''の部分圏である。例えばリスト関手は '''Hask''' から '''Lst'''である。ここで'''Lst'''は''リスト型''、すなわち任意の型<code>T</code>に対するリスト型<code>[T]</code>のみを含む圏である。'''Lst'''における射はリスト型の上で定義される関数であり、これは任意の型<code>T</code>, <code>U</code>に関して <code>[T] -> [U]</code>の関数である。どのようにこれを Haskell のFunctor型クラスへと結びつけたらよいのであろうか？定義を思い出そう。 
<!-- The Functor typeclass you will probably have seen in Haskell does in fact tie in with the categorical notion of a functor. Remember that a functor has two parts: it maps objects in one category to objects in another and morphisms in the first category to morphisms in the second. Functors in Haskell are from '''Hask''' to ''func'', where ''func'' is the subcategory of '''Hask''' defined on just that functor's types. E.g. the list functor goes from '''Hask''' to '''Lst''', where '''Lst''' is the category containing only ''list types'', that is, <code>[T]</code> for any type <code>T</code>. The morphisms in '''Lst''' are functions defined on list types, that is, functions <code>[T] -> [U]</code> for types <code>T</code>, <code>U</code>. How does this tie into the Haskell typeclass Functor? Recall its definition: -->

 class Functor (f :: * -> *) where
   fmap :: (a -> b) -> (f a -> f b)

インスタンスの例も示しておこう。
<!-- Let's have a sample instance, too: -->

 instance Functor Maybe where
   fmap f (Just x) = Just (f x)
   fmap _ Nothing  = Nothing

ここが鍵となる部分である。''型構築子'' Maybe は任意の型 <code>T</code> をとり新たな型<code>Maybe T</code>となる。また、Maybe 型へと狭められた <code>fmap</code> は関数 <code>a -> b</code> をとり関数 <code>Maybe a -> Maybe b</code> を返す。まさにこれがまさにそうではないか！ふたつの構成要素を定義した。ひとつは'''Hask'''の対象をとり別の圏(これはMaybe型を対象、Maybe型上の関数を射とする)の対象を返す何か、もうひとつは'''Hask''' の射をとりこの圏の射を返す何か。ゆえに Maybe は関手である。
<!-- Here's the key part: the ''type constructor'' Maybe takes any type <code>T</code> to a new type, <code>Maybe T</code>. Also, <code>fmap</code> restricted to Maybe types takes a function <code>a -> b</code> to a function <code>Maybe a -> Maybe b</code>. But that's it! We've defined two parts, something that takes objects in '''Hask''' to objects in another category (that of Maybe types and functions defined on Maybe types), and something that takes morphisms in '''Hask''' to morphisms in this category. So Maybe is a functor. -->

Haskellの関手が内容に関してmapできるような型を表すということは有用な直観である。これはリストや Maybeだけでなく、木のようなより複雑な構造もそうである。構造の内容にmapを行う関数は<code>fmap</code>を使って書くことができ、どんな関手構造もこの関数に渡すことができる。例えば、Data.List.map, Data.Map.map, Data.Array.IArray.amap などをすべてをカバーするジェネリックな関数を書くことができる。
<!-- A useful intuition regarding Haskell functors is that they represent types that can be mapped over. This could be a list or a Maybe, but also more complicated structures like trees. A function that does some mapping could be written using <code>fmap</code>, then any functor structure could be passed into this function. E.g. you could write a generic function that covers all of Data.List.map, Data.Map.map, Data.Array.IArray.amap, and so on. -->

関手の公理はどうだろうか？任意の''A''に対する<math>id_A</math> として多相的な関数 <code>id</code> を使い、最初の則は次のように書ける。  
<!-- What about the functor axioms? The polymorphic function <code>id</code> takes the place of <math>id_A</math> for any ''A'', so the first law states: -->

 fmap id = id

先程の直観によると、この式は『構造を辿ってしかし各要素に何もしないmapと、全く何もしないことは等しい」と解釈できる。次に、射の合成は単に <code>(.)</code> であり、つまり、
<!-- With our above intuition in mind, this states that mapping over a structure doing nothing to each element is equivalent to doing nothing overall. Secondly, morphism composition is just <code>(.)</code>, so -->

 fmap (f . g) = fmap f . fmap g

このふたつめの則は実用的に極めて役に立つ。関手をリストか何かのコンテナと考えると、右辺は２パスのアルゴリズムを表す。つまり構造についてまず<code>g</code>をmapし、さらに<code>f</code>をmapする。この関手の公理はこのような2パスのアルゴリズムを<code>f . g</code>を行う１パスのアルゴリズムへと変換できることを保証する。この処理は ''融合''(fusion)として知られている。
<!-- This second law is very useful in practice. Picturing the functor as a list or similar container, the right-hand side is a two-pass algorithm: we map over the structure, performing <code>g</code>, then map over it again, performing <code>f</code>. The functor axioms guarantee we can transform this into a single-pass algorithm that performs <code>f . g</code>. This is a process known as ''fusion''. -->

{{Exercises|リスト関手と Maybe 関手について、これらの規則を確かめよ。}}
<!-- {{Exercises|Check the laws for the Maybe and list functors.}} -->

=== 圏論の概念から Haskellへの変換 <!-- Translating categorical concepts into Haskell --> ===

関手はどのように圏論が Haskell へと変換されるかの良い例を提供する。次が理解の鍵となる。

<!-- Functors provide a good example of how category theory gets translated into Haskell. The key points to remember are that: -->

* 圏 '''Hask''' とその部分圏を扱う。
* 対象は型である。
* 射は関数である。
* 型を取り別の型を返すものが型構成子である。
* 関数をとり別の関数を返すものが高階関数である。
* 圏論ではしばしば一度に多くの対象にわたって物事が定義されるという事実を、型クラスとそれが同時に提供する多相性はうまく捉えている。

<!-- 
* We work in the category '''Hask''' and its subcategories.
* Objects are types.
* Morphisms are functions.
* Things that take a type and return another type are type constructors.
* Things that take a function and return another function are higher-order functions.
* Typeclasses, along with the polymorphism they provide, make a nice way of capturing the fact that in category theory things are often defined over a number of objects at once.
-->

== モナド <!-- Monads --> ==

[[Image:Unit-join.png|frame|right|モナドの全ての対象について''unit'' と ''join''のふたつの射が存在しなくてはならない。]]

<!-- [[Image:Unit-join.png|frame|right|''unit'' and ''join'', the two morphisms that must exist for every object for a given monad.]] -->

モナドは言うまでもなく Haskell の極めて重要な概念であるが、実はこれらは本来圏論に由来するものである。''モナド'' は圏から同じ圏への関手であり、さらにいくつかの追加の構造を提供する。では定義を見てみよう。モナドは''C''内のすべての対象 ''X''に対してふたつの射をともなう関手 <math>M : C \to C</math> である<ref>熟達した圏論の理論家は、ここで少し単純化していることに気付くだろう。''unit''と''join''を自然変換(natural transformations)として導入する代わりに、これらを明示的に射として扱った。そしてnaturalityをモナド則の[[#３番目と４番目の規則|規則３と規則４]]として追加した。ここでは圏論全体を教えようとしているわけではなく、Haskellのある構造に対する理論的裏付けとしての圏論だけを示したいために、このような単純化を行った。これらの射にHaskellで対応するものを連想させる名前を与えていることに気付く読者もいるかも知れない。これは名前<math>\eta</math> と <math>\mu</math>が直感的でないためである。</ref>。
<!-- Monads are obviously an extremely important concept in Haskell, and in fact they originally came from category theory. A ''monad'' is a special type of functor, from a category to that same category, that supports some additional structure. So, down to definitions. A monad is a functor <math>M : C \to C</math>, along with two morphisms<ref>Experienced category theorists will notice that we're simplifying things a bit here; instead of presenting ''unit'' and ''join'' as natural transformations, we treat them explicitly as morphisms, and require naturality as extra axioms alongside the [[#The monad laws|the standard monad laws]] (laws 3 and 4). The reasoning is simplicity; we are not trying to teach category theory as a whole, simply give a categorical background to some of the structures in Haskell. You may also notice that we are giving these morphisms names suggestive of their Haskell analogues, because the names <math>\eta</math> and <math>\mu</math> don’t provide much intuition.</ref> for every object ''X'' in ''C'': -->

* <math>\mathit{unit}^M_X : X \to M(X)</math>
* <math>\mathit{join}^M_X : M(M(X)) \to M(X)</math>

議論されているモナドが明らかなとき、これらの関数について上添字 ''M'' を省略することにし、単に何らかの ''X'' に対する<math>\mathit{unit}_X</math>と <math>\mathit{join}_X</math>について述べることにする。
<!-- When the monad under discussion is obvious, we’ll leave out the ''M'' superscript for these functions and just talk about <math>\mathit{unit}_X</math> and <math>\mathit{join}_X</math> for some ''X''. -->


では、どのようにこれを Haskell の型クラス Monad に翻訳されるかをみよう。
<!-- Let’s see how this translates to the Haskell typeclass Monad, then. -->

 class Functor m => Monad m where
   return :: a -> m a
   (>>=)  :: m a -> (a -> m b) -> m b

このクラス制約<code>Functor m</code>は<code>m</code>があらかじめ関手の構造、つまり対象と射の対応付けを持っていることを保証する。<code>return</code> は全ての ''X'' に対する<math>\mathit{unit}_X</math> の(多相的な)類義語である。しかしここには問題がある。<code>return</code>の型は''unit''に非常に似ているけれども、もう一方の関数、しばしば''bind''とも呼ばれる <code>(>>=)</code>の型は''join''に似ていない。ここでさらに別のモナド関数<code>join :: Monad m => m (m a) -> m a</code>があり、これは非常によく似ている。実際に、<code>join</code> と <code>(>>=)</code>は次のように互いに表すことができる。

<!-- The class constraint of <code>Functor m</code> ensures that we already have the functor structure: a mapping of objects and of morphisms. <code>return</code> is the (polymorphic) analogue to <math>\mathit{unit}_X</math> for any ''X''. But we have a problem. Although <code>return</code>’s type looks quite similar to that of ''unit''; the other function, <code>(>>=)</code>, often called ''bind'', bears no resemblance to ''join''. There is however another monad function, <code>join :: Monad m => m (m a) -> m a</code>, that looks quite similar. Indeed, we can recover <code>join</code> and <code>(>>=)</code> from each other: -->

 join :: Monad m => m (m a) -> m a
 join x = x >>= id
 
 (>>=) :: Monad m => m a -> (a -> m b) -> m b
 x >>= f = join (fmap f x)

つまり、モナドの <code>return</code>, <code>fmap</code>, <code>join</code>を定義することは、<code>return</code> と <code>(>>=)</code>を定義することと同等である。圏論でモナドの定義をする典型的な方法が''unit'' と ''join''を与えることであるのに対して、Haskell プログラマは<code>return</code> と <code>(>>=)</code>を与えることを好むことがわかる。<ref>これはおそらく、圏論では様々な構造のコンテナとしての側面に重点が置かれるのに対して、Haskellプログラマはモナドを共通する機能を持つ計算を連鎖させる方法と考えることを好むことが原因であろう。<code>join</code>はコンテナのふたつの層をひとつに潰すという意味でコンテナと自然に関連し、対して<code>(>>=)</code>は何かを行い、その結果を何かに与えるという意味で計算を連鎖させる自然な演算子である。</ref><!--  <ref>This is perhaps due to the fact that Haskell programmers like to think of monads as a way of sequencing computations with a common feature, whereas in category theory the container aspect of the various structures is emphasised. <code>join</code> pertains naturally to containers (squashing two layers of a container down into one), but <code>(>>=)</code> is the natural sequencing operation (do something, feeding its results into something else).</ref> -->多くの場合、圏論の方法のほうが理にかなっている。
何らかの構造<math>M</math>があり、任意の対象''X''を<math>M(X)</math>としたり、<math>M(M(X))</math>を<math>M(X)</math>とできる自然な方法があるとき、それはしばしばモナドである。次の節で例を示す。
 
<!-- So specifying a monad’s <code>return</code>, <code>fmap</code>, and <code>join</code> is equivalent to specifying its <code>return</code> and <code>(>>=)</code>. It just turns out that the normal way of defining a monad in category theory is to give ''unit'' and ''join'', whereas Haskell programmers like to give <code>return</code> and <code>(>>=)</code>.<ref>This is perhaps due to the fact that Haskell programmers like to think of monads as a way of sequencing computations with a common feature, whereas in category theory the container aspect of the various structures is emphasised. <code>join</code> pertains naturally to containers (squashing two layers of a container down into one), but <code>(>>=)</code> is the natural sequencing operation (do something, feeding its results into something else).</ref> Often, the categorical way makes more sense. Any time you have some kind of structure ''M'' and a natural way of taking any object ''X'' into <math>M(X)</math>, as well as a way of taking <math>M(M(X))</math> into <math>M(X)</math>, you probably have a monad. We can see this in the following example section. -->

=== 例: 冪集合関手もモナドである <!-- Example: the powerset functor is also a monad --> ===

先ほど述べた冪集合関手 <math>P : \mathbf{Set} \to \mathbf{Set}</math> はモナドをなす。任意の集合''S''について、要素をその単集合へ写す<math>\mathit{unit}_S(x) = \{x\}</math> がある。これらの単集合のそれぞれは明らかに ''S'' の部分集合であり、よって<math>\mathit{unit}_S</math>は''S''の冪集合の要素を返す、つまりモナドの要求を満たしている。同様に関数 <math>\mathit{join}_S</math> を次のように定義できる。引数として<math>L \in \mathcal{P}(\mathcal{P}(S))</math>をとる。これは、
<!-- The power set functor <math>P : \mathbf{Set} \to \mathbf{Set}</math> described above forms a monad. For any set ''S'' you have a <math>\mathit{unit}_S(x) = \{x\}</math>, mapping elements to their singleton set. Note that each of these singleton sets are trivially a subset of ''S'', so <math>\mathit{unit}_S</math> returns elements of the powerset of ''S'', as is required. Also, you can define a function <math>\mathit{join}_S</math> as follows: we receive an input <math>L \in \mathcal{P}(\mathcal{P}(S))</math>. This is: -->

* 冪集合の要素はもとの集合の部分集合、すなわち<math>X \in \mathcal{P}(S) \leftrightarrow X \subseteq S</math>
* つまり<math>L \subseteq \mathcal{P}(S)</math>
* つまり<math>L</math>は<math>S</math>の部分集合の集合。
<!--
直訳せず説明をスマートに書きなおした。
* ''S''の冪集合の冪集合の要素。
* つまり、''S''のすべての部分集合の集合のすべての部分集合の集合の要素。
* つまり、''S''の部分集合の集合。
-->
<!-- 
* A member of the powerset of the powerset of ''S''.
* So a member of the set of all subsets of the set of all subsets of ''S''.
* So a set of subsets of ''S''
-->

よって<math>\mathit{join}_S</math>はこれらの部分集合の和を返すことで、''S''のまた別の部分集合を与えるようにする。式で表せば、
<!-- We then return the union of these subsets, giving another subset of ''S''. Symbolically, -->

: <math>\mathit{join}_S(L) = \bigcup L</math>. 

従って、(次の節で探求する規則を満たすことが証明できれば)''P'' はモナドである。
<!-- Hence ''P'' is a monad <ref>If you can prove that certain laws hold, which we'll explore in the next section.</ref>. -->

実際のところ、議論の対象が集合の代わりにリストになるという違いを除けば、''P''はほとんどリストモナドと等しい。これらはほぼ同じものである。比較してみよう。
<!-- In fact, ''P'' is almost equivalent to the list monad; with the exception that we're talking lists instead of sets, they're almost the same. Compare: -->

{| class="wikitable" width="100%"

! colspan="2" width="50%" | '''Set'''に対する冪集合関手
! colspan="2" width="50%" | Haskellのリストモナド
|-
! 関数の型
! 定義
! 関数の型
! 定義

|-

| colspan="2" | 集合を ''S'' 、射を <math>f : A \to B</math>とする
| colspan="2" | 型を <code>T</code> 、関数を <code>f :: A -> B</code>とする

|-

| <math>P(f) : \mathcal{P}(A) \to \mathcal{P}(B)</math>
| <math>(P(f))(S) = \{ f(a) : a \in S \}</math>

| <code>fmap f :: [A] -> [B]</code>
| <code>fmap f xs = <nowiki>[ f a | a <- xs ]</nowiki></code>

|-

| <math>\mathit{unit}_S : S \to \mathcal{P}(S)</math>
| <math>\mathit{unit}_S(x) = \{ x \}</math>

| <code>return :: T -> [T]</code>
| <code>return x = [x]</code>

|-

| <math>\mathit{join}_S : \mathcal{P}(\mathcal{P}(S)) \to \mathcal{P}(S)</math>
| <math>\mathit{join}_S(L) = \bigcup L</math>

| <code>join :: <nowiki>[[T]]</nowiki> -> [T]</code>
| <code>join xs = concat xs</code>

|}

<!--
{| class="wikitable" width="100%"

! colspan="2" width="50%" | Power set functor on '''Set'''
! colspan="2" width="50%" | List monad from Haskell
|-
! Function type
! Definition
! Function type
! Definition

|-

| colspan="2" | Given a set ''S'' and a morphism <math>f : A \to B</math>:
| colspan="2" | Given a type <code>T</code> and a function <code>f :: A -> B</code>

|-

| <math>P(f) : \mathcal{P}(A) \to \mathcal{P}(B)</math>
| <math>(P(f))(S) = \{ f(a) : a \in S \}</math>

| <code>fmap f :: [A] -> [B]</code>
| <code>fmap f xs = <nowiki>[ f a | a <- xs ]</nowiki></code>

|-

| <math>\mathit{unit}_S : S \to \mathcal{P}(S)</math>
| <math>\mathit{unit}_S(x) = \{ x \}</math>

| <code>return :: T -> [T]</code>
| <code>return x = [x]</code>

|-

| <math>\mathit{join}_S : \mathcal{P}(\mathcal{P}(S)) \to \mathcal{P}(S)</math>
| <math>\mathit{join}_S(L) = \bigcup L</math>

| <code>join :: <nowiki>[[T]]</nowiki> -> [T]</code>
| <code>join xs = concat xs</code>

|}
-->

== モナド則とその重要性 <!-- The monad laws and their importance --> ==

関手がそう呼ばれるためには従わなければならない公理があるように、モナドにも幾つかそのような公理が存在する。まずはそれらを一覧し、次に Haskell へと翻訳し、なぜそれが重要なのかをみていくことにしよう。
<!-- Just as functors had to obey certain axioms in order to be called functors, monads have a few of their own. We'll first list them, then translate to Haskell, then see why they’re important. -->

モナド <math>M : C \to C</math> と、<math>A, B \in C</math>に射 <math>f : A \to B</math> があるとする。
このとき次が成り立たなくてはならない。
<!-- Given a monad <math>M : C \to C</math> and a morphism <math>f : A \to B</math> for <math>A, B \in C</math>, -->

# <math>\mathit{join} \circ M(\mathit{join}) = \mathit{join} \circ \mathit{join}</math>
# <math>\mathit{join} \circ M(\mathit{unit}) = \mathit{join} \circ \mathit{unit} = \mathit{id}</math>
# <math>\mathit{unit} \circ f = M(f) \circ \mathit{unit}</math>
# <math>\mathit{join} \circ M(M(f)) = M(f) \circ \mathit{join}</math>


Haskell への翻訳はなるべく自明であってほしい。
<!-- By now, the Haskell translations should be hopefully self-explanatory: -->

# <code>join . fmap join     = join . join</code>
# <code>join . fmap return   = join . return = id</code>
# <code>return . f           = fmap f . return</code>
# <code>join . fmap (fmap f) =  fmap f . join</code>

(<code>fmap</code> が関手の構成要素のひとつで、射に作用するものであることを思い出そう。)これらの則は最初は少し不可解にも思える。いったいこれらの則はどういう意味で、なぜモナドはこれを満たすべきなのだろうか？ではこれらの法則について調べていこう。
<!-- (Remember that <code>fmap</code> is the part of a functor that acts on morphisms.) These laws seem a bit impenetrable at first, though. What on earth do these laws mean, and why should they be true for monads? Let’s explore the laws. -->

=== 最初の規則 <!-- The first law --> ===
<code>join . fmap join = join . join</code>
[[Image:Monad-law-1-lists.png|frame|right|最初の規則のリスト版の説明。リストモナドでは  <code>join</code> は <code>concat</code> で、<code>fmap</code> は <code>map</code> であることを思い出そう。]]
<!-- [[Image:Monad-law-1-lists.png|frame|right|A demonstration of the first law for lists. Remember that <code>join</code> is <code>concat</code> and <code>fmap</code> is <code>map</code> in the list monad.]] -->

この規則を理解するために、まずはリストの例を使っていこう。最初の規則は<code>join . fmap join</code> (左辺) と <code>join . join</code> (右辺)のふたつの関数について述べている。これらの型はどうなるだろうか？(今はリストモナドについて議論しているので)<code>join</code>の型は<code><nowiki>[[a]]</nowiki> -> [a]</code>であることを思い出そう。つまり両辺の型はどちらも<code>[[[a]]] -> [a]</code>である。(これが同じであるという事実は役に立つ。最終的には、両辺が全く同じ関数であることを示そうとしているのだ。)では、リストのリストのリストがあるとしよう。左辺はこの三重のリストに <code>fmap join</code>を作用させ(1)、その結果に <code>join</code> を適用する(2)。  <code>fmap</code> はリストに対しては <code>map</code> と同じであるので、(1)の計算はまずいちばん外側のリストの要素に対して<code>join</code>を<code>map</code>で施す。各要素に対して、<code>join</code>はリストのリストそれぞれを連結する。結果としてリストのリストが得られたら、(2)によりこれ全体に<code>join</code>を適用する。手短に言えば、トップレベルに'入り込み'、二番目と三番目のレベルを潰してひとつにして、次いでトップレベルとこの新しいレベルを潰してひとつにする。
<!-- In order to understand this law, we'll first use the example of lists. The first law mentions two functions, <code>join . fmap join</code> (the left-hand side) and <code>join . join</code> (the right-hand side). What will the types of these functions be? Remembering that <code>join</code>’s type is <code><nowiki>[[a]]</nowiki> -> [a]</code> (we’re talking just about lists for now), the types are both <code>[[[a]]] -> [a]</code> (the fact that they’re the same is handy; after all, we’re trying to show they’re completely the same function!). So we have a list of list of lists. The left-hand side, then, performs <code>fmap join</code> on this 3-layered list, then uses <code>join</code> on the result. <code>fmap</code> is just the familiar <code>map</code> for lists, so we first map across each of the list of lists inside the top-level list, concatenating them down into a list each. So afterward, we have a list of lists, which we then run through <code>join</code>. In summary, we 'enter' the top level, collapse the second and third levels down, then collapse this new level with the top level. -->

では右辺についてはどうだろうか？最初にリストのリストのリストに対して <code>join</code>
を実行する。普通<code>join</code>は二重のリストに適用するものであるが、三重のリストにも適用できる。なぜなら、<code>[[[a]]]</code>は<code>b = [a]</code>とおけば<code><nowiki>[[b]]</nowiki></code>と書けるからである。つまり三重のリストはある意味で二重のリストにすぎない、ただし最深部は'フラット'な値でなく別のリストからなっている。だからもしリストのリスト(のリスト)に<code>join</code>を適用すると、外側のふたつのリストがひとつに平坦化される。外から二番目の深さのリストの要素はフラットではなく三番目の層のリストが含まれているので、この結果はリストのリストであり、次にもう一方の<code>join</code> がこの構造を平坦化する。要約すると、左辺は内側のふたつの層を新しい層へと平坦化し、それから最も外側と新しい層を平坦化する。右辺は外側のふたつの層をまず平坦化し、それから新しい層と最も内側の層を平坦化する。これらの二つの操作は等しい。これはいわば<code>join</code>に関する結合則のようなものである。
<!-- What about the right-hand side? We first run <code>join</code> on our list of list of lists. Although this is three layers, and you normally apply a two-layered list to <code>join</code>, this will still work, because a <code>[[[a]]]</code> is just <code><nowiki>[[b]]</nowiki></code>, where <code>b = [a]</code>, so in a sense, a three-layered list is just a two layered list, but rather than the last layer being 'flat', it is composed of another list. So if we apply our list of lists (of lists) to <code>join</code>, it will flatten those outer two layers into one. As the second layer wasn't flat but instead contained a third layer, we will still end up with a list of lists, which the other <code>join</code> flattens. Summing up, the left-hand side will flatten the inner two layers into a new layer, then flatten this with the outermost layer. The right-hand side will flatten the outer two layers, then flatten this with the innermost layer. These two operations should be equivalent. It’s sort of like a law of associativity for <code>join</code>. -->

次のようにした<code>Maybe</code> もまたモナドである。
<!-- <code>Maybe</code> is also a monad, with -->

 return :: a -> Maybe a
 return x = Just x
 
 join :: Maybe (Maybe a) -> Maybe a
 join Nothing         = Nothing
 join (Just Nothing)  = Nothing
 join (Just (Just x)) = Just x

''三重の'' Maybe (これは<code>Nothing</code>, <code>Just Nothing</code>, <code>Just (Just Nothing)</code>, <code>Just (Just (Just x))</code>といった値をとる)を考えて、一つめの規則は内側のふたつの層を先に潰し、それから外側の層を潰すことは、外側の層が先に潰し、それから最も内側の層を潰すことと全く同じであると述べている。
<!-- So if we had a ''three''-layered Maybe (i.e., it could be <code>Nothing</code>, <code>Just Nothing</code>, <code>Just (Just Nothing)</code> or <code>Just (Just (Just x))</code>), the first law says that collapsing the inner two layers first, then that with the outer layer is exactly the same as collapsing the outer layers first, then that with the innermost layer. -->

{{Exercises| 層の平坦化がどのように働くかを見るために、リストモナドと Maybe モナドがこの規則に確かに従うことを、幾つかの例について確認せよ。}}
<!-- {{Exercises|Verify that the list and Maybe monads do in fact obey this law with some examples to see precisely how the layer flattening works.}} -->

=== 二番目の規則 <!-- The second law --> ===
<code>join . fmap return = join . return = id</code>

それでは、二番目の法則はどうだろうか？再び、リストの例で始めよう。二番目の法則で述べられている両辺は <code>[a] -> [a]</code>の関数である。左辺はまずリストのそれぞれの要素<code>x</code>を要素がそれひとつだけのリスト<code>[x]</code>へと変え、シングルトンリストのリストを得る。この二重のリストは再び<code>join</code>を使って一重のリストへと平坦化される。以上が左辺の表す関数である。一方右辺では、リスト全体<code>[x, y, z, ...]</code>をとり、これをリストのシングルトンリスト<code><nowiki>[[x, y, z, ...]]</nowiki></code>にし、それから再びこのふたつの層をひとつに平坦化する。この規則は一言で説明できるほどの自明さはないが、<code>return</code>をモナドの値に適用しその結果を<code>join</code>することは、<code>return</code>を最上位の層の内側で実行しても外側で実行しても同じ結果になるべきであるということを本質的に述べている。

<!-- What about the second law, then? Again, we'll start with the example of lists. Both functions mentioned in the second law are functions <code>[a] -> [a]</code>. The left-hand side expresses a function that maps over the list, turning each element <code>x</code> into its singleton list <code>[x]</code>, so that at the end we’re left with a list of singleton lists. This two-layered list is flattened down into a single-layer list again using the <code>join</code>. The right hand side, however, takes the entire list <code>[x, y, z, ...]</code>, turns it into the singleton list of lists <code><nowiki>[[x, y, z, ...]]</nowiki></code>, then flattens the two layers down into one again. This law is less obvious to state quickly, but it essentially says that applying <code>return</code> to a monadic value, then <code>join</code>ing the result should have the same effect whether you perform the <code>return</code> from inside the top layer or from outside it. -->

{{Exercises| Maybe モナドについて、二番目の規則を証明せよ。}}
<!-- {{Exercises|Prove this second law for the Maybe monad.}} -->

=== ３番目と４番目の規則 <!-- The third and fourth laws --> ===
<code>return . f = fmap f . return</code>

<code>join . fmap (fmap f) = fmap f . join</code>

最後のふたつの法則は、どのようにモナドが振舞うべきかに関するもっと自明な事実を示す。これがどう真であるかを調べる最も簡単な方法は、展開した形式を使うためにこれらを展開することである。
<!-- The last two laws express more self evident fact about how we expect monads to behave. The easiest way to see how they are true is to expand them to use the expanded form: -->

# <code>\x -> return (f x)  =  \x -> fmap f (return x)</code>
# <code>\x -> join (fmap (fmap f) x)  =  \x -> fmap f (join x)</code>

{{Exercises|最初と二番目の規則を説明したのと同様の方法で、それらがどのような意味を持つかを探り、これらの規則がどんなモナドについても成り立つべきであることを確かめよ。}}
<!-- {{Exercises|Convince yourself that these laws should hold true for any monad by exploring what they mean, in a similar style to how we explained the first and second laws.}} -->

=== doブロックへの適用 <!-- Application to do-blocks --> ===
モナドが従わなければならない規則について直観的に説明した。ではなぜこれは重要なのか？その答えは do ブロックについて考えたときに明らかになる。次のお決まりの変換が示しているように、do ブロックが文の組み合わせを<code>(>>=)</code>を使わずに表すためのただの構文糖衣であることを思い出そう。
<!-- Well, we have intuitive statements about the laws that a monad must support, but why is that important? The answer becomes obvious when we consider do-blocks. Recall that a do-block is just syntactic sugar for a combination of statements involving <code>(>>=)</code> as witnessed by the usual translation: -->

 do { x }                 -->  x
 do { let { y = v }; x }  -->  let y = v in do { x }
 do { v <- y; x }         -->  y >>= \v -> do { x }
 do { y; x }              -->  y >>= \_ -> do { x }

ここで用いている4つの規則から、通常の <code>return</code> と<code>(>>=)</code>を使ったモナド則を証明できることに注意したい。(非常に大掛かりな証明もあるので、ここは飛ばしてしまっても構わない。)
 
<!-- Also notice that we can prove what are normally quoted as the monad laws using <code>return</code> and <code>(>>=)</code> from our above laws (the proofs are a little heavy in some cases, feel free to skip them if you want to): -->

<ol><li>

<code>return x >>= f  =  f x</code>. 証明:
<!-- <<code>return x >>= f  =  f x</code>. Proof: -->
<pre>   return x >>= f
 = join (fmap f (return x)) -- (>>=)の定義より
 = join (return (f x))      -- 規則3より
 = (join . return) (f x)
 = id (f x)                 -- 規則2より
 = f x
</pre>

</li><li>

<code>m >>= return  =  m</code>. 証明:
<!-- <code>m >>= return  =  m</code>. Proof: -->
<pre>
   m >>= return
 = join (fmap return m)    -- (>>=)の定義より
 = (join . fmap return) m
 = id m                    -- 規則2より
 = m
</pre>
</li><li>

<code>(m >>= f) >>= g  =  m >>= (\x -> f x >>= g)</code>. 証明 (<code>fmap f . fmap g = fmap (f . g)</code>を思い出そう):
<!-- <code>(m >>= f) >>= g  =  m >>= (\x -> f x >>= g)</code>. Proof (recall that <code>fmap f . fmap g = fmap (f . g)</code>): -->
<pre>
   (m >>= f) >>= g
 = (join (fmap f m)) >>= g                          -- (>>=)の定義より
 = join (fmap g (join (fmap f m)))                  -- (>>=)の定義より
 = (join . fmap g) (join (fmap f m))
 = (join . fmap g . join) (fmap f m)
 = (join . join . fmap (fmap g)) (fmap f m)         -- 規則4より
 = (join . join . fmap (fmap g) . fmap f) m
 = (join . join . fmap (fmap g . f)) m              -- 関手の分配則より
 = (join . join . fmap (\x -> fmap g (f x))) m
 = (join . fmap join . fmap (\x -> fmap g (f x))) m -- 規則1より
 = (join . fmap (join . (\x -> fmap g (f x)))) m    -- 関手の分配則より
 = (join . fmap (\x -> join (fmap g (f x)))) m
 = (join . fmap (\x -> f x >>= g)) m                -- (>>=)の定義より
 = join (fmap (\x -> f x >>= g) m)
 = m >>= (\x -> f x >>= g)                          -- (>>=)の定義より
</pre>

</li></ol>

<code>return</code>と<code>(>>=)</code>を使うこの新たなモナド則は、これをdo記法へと変換できる。

<!-- These new monad laws, using <code>return</code> and <code>(>>=)</code>, can be translated into do-block notation. -->

{| class="wikitable" style="margin: 1em auto"

! ポイントフリースタイル
! do記法

|-

| <code>return x >>= f = f x</code>
| <code>do { v <- return x; f v } = do { f x }</code>

|-

| <code>m >>= return = m</code>
| <code>do { v <- m; return v } = do { m }</code>

|-

| <code>(m >>= f) >>= g = m >>= (\x -> f x >>= g)</code>
| 
<pre>   do { y <- do { x <- m; f x };
        g y }
 =
   do { x <- m;
        y <- f x;
        g y }
</pre>

|}

モナド則はいまやdoブロックがどのように機能すべきかという常識を述べた文である。もしこれらの規則がひとつでも無効であれば、doブロックを期待したとおりに操作できなくなるのでユーザが混乱する。要するに、モナド則はユーザビリティガイドラインなのである。

<!-- The monad laws are now common-sense statements about how do-blocks should function. If one of these laws were invalidated, users would become confused, as you couldn't be able to manipulate things within the do-blocks as would be expected. The monad laws are, in essence, usability guidelines. -->

{{Exercises|1=
規則をここでは２バージョン示した。
 -- 圏論的:
 join . fmap join = join . join
 join . fmap return = join . return = id
 return . f = fmap f . return
 join . fmap (fmap f) = fmap f . join
 
 -- 関数的:
 m >>= return = m
 return m >>= f = f m
 (m >>= f) >>= g = m >>= (\x -> f x >>= g)

これらは全く同等である。圏論的な規則から関数的な規則を作る方法は示した。逆をやってみよう。関数的な規則から始めて、圏論の規則が満たされることを示せ。以下の定義を思い出すと役に立つ。
 join m = m >>= id
 fmap f m = m >>= return . f
この問題を薦めてくれた Yitzchak Gale に感謝する。
}}
<!-- {{Exercises|1=
In fact, the two versions of the laws we gave:
 -- Categorical:
 join . fmap join = join . join
 join . fmap return = join . return = id
 return . f = fmap f . return
 join . fmap (fmap f) = fmap f . join
 
 -- Functional:
 m >>= return = m
 return m >>= f = f m
 (m >>= f) >>= g = m >>= (\x -> f x >>= g)
are entirely equivalent. We showed that we can recover the functional laws from the categorical ones. Go the other way; show that starting from the functional laws, the categorical laws hold. It may be useful to remember the following definitions:
 join m = m >>= id
 fmap f m = m >>= return . f
Thanks to Yitzchak Gale for suggesting this exercise.
}} -->

== まとめ <!-- Summary --> ==
この章で長い道のりを辿ってきた。圏とは何か、どうやってHaskellに応用されるのかを見てきた。関手をはじめとする圏論の基本的な概念から、モナドのようなより発展的な内容まで、それらがいかにHaskellらしさに必要不可欠であるかについても紹介してきた。自然変換(natural transformations)など、我々の目的に必要なかった幾つかの圏論の基本的事項については触れなかったが、代わりにHaskellの構造の背後に根付く圏論の直観的な理解を提供した。

<!-- We've come a long way in this chapter. We've looked at what categories are and how they apply to Haskell. We've introduced the basic concepts of category theory including functors, as well as some more advanced topics like monads, and seen how they're crucial to idiomatic Haskell. We haven't covered some of the basic category theory that wasn't needed for our aims, like natural transformations, but have instead provided an intuitive feel for the categorical grounding behind Haskell's structures. -->

== 注釈 ==
<references />

{{Haskell navigation|chapter=Wider Theory}}
[[Category:Haskell|Category theory]]

[[en:Haskell/Category theory]]