クライスリ圏とプログラムの関係
はじめに
これは何の記事？
本記事は、クライスリ圏という圏と、プログラムの関係を書いた記事になります。
主に内容は次になります。
- 圏の定義
- 定義の解説
- プログラムとの関係
この記事では実際のプログラミング言語として個人的な嗜好で関数型言語PureScriptを用いますが、Haskellにも読み替えられるはずです。
クライスリ圏とは？の前に
では、まずクライスリ圏の定義を、、、といきたいところなのですが、いきなり圏の話をするよりは、プログラムにクライスリ圏の概念が登場する例を見たほうがよいかなと思います。
ということで圏の話の前に、応用の話を一部先取りして書いてしまいます。
>=>
HaskellやPureScriptなどには>=>という中置演算子があります。
見たことがある、あるいは使ったことがあるかもしれませんね。
関数の定義としては
forall a b c m. Bind m => (a -> m b) -> (b -> m c) -> a -> m c
のようになっています。
詳しくは後述しますが、これはクライスリ圏でいうと「射の合成」にあたります。
クライスリ圏の射はa -> m bという形をしているので、2つの射(a -> m b),(b -> m c)を合成するというわけです。
=<<
>>= (bind)の引数の順序を入れ替えた=<< (bindFlipped)もクライスリ圏と関係があります。
bind :: m a -> a -> m b -> m b
bindFlipped :: a -> m b -> m a -> m b
クライスリ圏を構成する要素として拡張演算子と呼ばれるものがあるのですが、a -> m bという射にこの拡張演算子を適用するとm a -> m bという射になります。
a -> m bを関数fと呼び、拡張演算子を*とするならf*はbindFlippedと一致します。
詳しくは後ほど説明しましょう。
二つ例を挙げましたが、bindなんかはかなり身近な関数ですよね。
というところで、そろそろ本格的にクライスリ圏の話に突入したいと思います。
クライスリ圏
まず、クライスリ圏ですが、定義の仕方がいくつか存在します。
例えばnLabに記載されている定義は、モナドを前提とした定義になっています。
この記事では、クライスリトリプルを用いた定義を使います。
【定義】クライスリトリプル
圏
- 関手
{\footnotesize T:\mathcal{C}\rightarrow\mathcal{C}} - 自然変換
{\footnotesize \eta_{A}:A\rightarrow T(A)} {\footnotesize A\in\mathrm{ob}(\mathcal{C})} - 射
{\footnotesize f:A\rightarrow T(B)} {\footnotesize f^{*}:T(A)\rightarrow T(B)} {\footnotesize -^{*}}
からなる3つ組
-
{\footnotesize f^{*} \circ \eta _{A}=f} {\footnotesize f:A\rightarrow T(B)} {\footnotesize \eta {_{A}^{*}} =1_{T(A)}} -
{\footnotesize g^{*} \circ f^{*} =\left( g^{*} \circ f\right)^{*}} {\footnotesize f:A\rightarrow T(B)} {\footnotesize g:B\rightarrow T(C)}
【解説】クライスリトリプル
自己関手
そうモナドの定義にも出てきたものです。
2つの定義を比べてみましょう。
モナドには自然変換
というかモナドとクライスリトリプルはお互いに構成可能なのですが、それは置いておいてモナドとの違いを生んでいる拡張演算子について説明します。
拡張演算子の定義の
拡張演算子が適用された射は、元の射のdomain
これを踏まえて、定義にあるクライスリトリプルの3つの条件を図解します。
-
{\footnotesize f^{*} \circ \eta _{A}=f} {\footnotesize f:A\rightarrow T(B)}
-
{\footnotesize \eta {_{A}^{*}} =1_{T(A)}}
-
{\footnotesize g^{*} \circ f^{*} =\left( g^{*} \circ f\right)^{*}} {\footnotesize f:A\rightarrow T(B)} {\footnotesize g:B\rightarrow T(C)}
また、この拡張演算子において射のdomainが既に関手
ということは
これまたどこかで見たことありませんか？
そう、モナドの3つ組の
ということはこれを利用してクライスリトリプルからモナドを構成することができそうですし、実際できます（趣旨から外れるため証明は省略します）。
【定義】クライスリ圏
圏
そして圏として成り立つための条件である対象・射・射の合成について次のように定めた圏
-
【対象】
{\footnotesize \mathrm{ob}(\mathcal{C_T})=\mathrm{ob}(\mathcal{C})} -
【射】
{\footnotesize \mathrm{Hom}_{\mathcal{C_T}}(A,B)=\mathrm{Hom}_{\mathcal{C}}(A,T(B))} -
【射の合成】
{\footnotesize f\in \mathrm{Hom}_{\mathcal{C_T}}(A,B),\,\, g\in \mathrm{Hom}_{\mathcal{C_T}}(B,C)} {\footnotesize g\circ f:A\rightarrow C}
{\footnotesize f\in \mathrm{Hom}_{\mathcal{C}}(A,T(B)),\,\, g\in \mathrm{Hom}_{\mathcal{C}}(B,T(C))} {\footnotesize g^{*}\circ f:A\rightarrow T(C)} -
【恒等射】
{\footnotesize A\in \mathrm{\mathcal{C_T}}} {\footnotesize 1_{A}=\eta_A}
圏
【解説】クライスリ圏
対象について
対象についての規則は、『
これは、圏
射について
次に射についての規則は、『
これは、圏
圏
雰囲気を掴むための図
表面の世界と、その世界につながる裏の世界みたいに捉えてみるといいかもしれません。
射の合成について
最後に射の合成についての規則は、
というものでした。
なぜこのような規則が定められているのでしょうか？
それは、クライスリ射をそのまま合成することができないからです。
例えば
これは
と
の
合成になるわけですが、
そこで拡張演算子が出てくるわけで、クライスリ射
恒等射について
プログラムの世界での話
クライスリ圏の概念を踏まえつつ、今一度>=>や>>=を見ていきます。
>=>
>=>の定義は
forall a b c m. Bind m => (a -> m b) -> (b -> m c) -> a -> m c
でした。
a -> m bやb -> m cという形は、クライスリ射
クライスリ射を合成するとa -> m cとも一致します。
ということで最初の方に書いた通り、>=>はクライスリ射の合成というわけです。
PureScriptでは>=>はcomposedKleisliという関数名になっていますが、元ネタの通りの意味を持つ関数だったんですね。
>>=, =<<
次に>>=(bind)や=<<(bindFlipped)の定義を見てみましょう。
bind :: m a -> a -> m b -> m b
bindFlipped :: a -> m b -> m a -> m b
ここでもa -> m bというクライスリ射にあたるものが出てきましたね。
そしてbindFlippedの方は括弧をつけて(a -> m b) -> (m a -> m b)としてみると、a -> m bをクライスリトリプルの拡張演算子でm a -> m bに写してやっているものと一致しており、拡張演算子*=bindFlippedと解釈できるかと思います。
そして拡張演算子によってクライスリ射の合成を実現できたことを思い出しつつ、PureScriptにおいてのbindFlippedの定義を見てみましょう。
composeKleisli :: forall a b c m. Bind m => (a -> m b) -> (b -> m c) -> a -> m c
composeKleisli f g a = f a >>= g
実装に、>>=が出てきました。これはbindですが、bindFlippedの引数を入れ替えればbindになるので、bindFlippedでも実装可能です。
プログラムの圏としてのクライスリ圏と、モナドへの影響
この節では、「プログラムの圏をモデル化するためのクライスリ圏」の話と、関数型プログラムの構造化におけるモナドの応用の歴史に登場するクライスリ圏の話をします。
まずHaskellの設計者の一人であるPhilip Wadlerが、論文『The essence of functional programming』で、モナドの過去について言及している部分を見てみます（翻訳はDeepLです。参照の部分はリンクなどを追記しています。誤りがあったらご指摘いただけると幸いです）。
5.2 過去
最後に、これらの考え方の起源について述べておこう。
モナドの概念は圏論 [マックレーンの『圏論の基礎』] に由来する。
最初はホモロジー代数の分野で生まれたが、後に（KleisliやEilenbergとMooreの研究によって）もっと広い応用があることが認識された。その重要性は徐々に現れたが、初期には正式な名前すら与えられず、単に「標準構成」や「トリプル」と呼ばれていた。ここで使われている定式化はKleisliによるものである。
Eugenio Moggiは、モナドが意味論に有用な構造化ツールを提供することを提案した[Mog89a, Mog89b]。彼は、ラムダ計算が任意のモナドにおいて、値による呼出しと名前による呼出しのセマンティクスをどのように与えられるか、また、モナドが状態、例外処理、継続などのプログラミング言語のさまざまな機能をどのようにカプセル化できるかを示した。
原文
5.2 The past
Finally, something should be said about the origin of these ideas.
The notion of monad comes from category theory [Mac71, LS86].
It first arose in the area of homological algebra, but later was recognised (due to the work of Kleisli and of Eilenberg and Moore) to have much wider applications.
Its importance emerged slowly: in early days, it was not even given a proper name, but called simply a “standard construction” or a “triple”.
The formulation used here is due to Kleisli.
Eugenio Moggi proposed that monads provide a useful structuring tool for denotational semantics [Mog89a, Mog89b].
更にWadlerはこう書いています。
MoggiとSpiveyに触発されて、私は関数型プログラムを構造化する一般的な手法としてモナドを提案した。
原文:Inspired by Moggi and Spivey, I proposed monads as a general technique for structuring functional programs.
どうやら、WadlerはモナドにおいてMoggi（などの人物）の考え方に影響を受けているようです。
(計算機科学者MoggiについてはWikipediaを参照)
ということで、次はMoggiの『Notions of Computation and Monads』を見てみます。
Moggiはこの「1. A CATEGORICAL SEMANTICS OF COMPUTATIONS」で「プログラムの圏」について言及しています。
以下の圏論的意味論の基本的な考え方は、プログラミング言語を圏
で解釈するために、 {\footnotesize \mathcal{C}} 型の値の対象 {\footnotesize A} と {\footnotesize A} 型の計算の対象 {\footnotesize A} を区別し、 {\footnotesize TA} 型のプログラムの表記を {\footnotesize A} の要素とする、というものである。 {\footnotesize TA}
特に、型と {\footnotesize A} 型の値の対象を識別し、 {\footnotesize A} 型に単項の型構成子 {\footnotesize A} を適用することで、 {\footnotesize T} 型の計算の対象を得る。 {\footnotesize A}
私たちはを計算の概念と呼ぶ。これは、計算が生み出す可能性のある値の型を抽象化したものだからである。 {\footnotesize TA}
には、さまざまな計算概念に対応する多くの選択肢がある。 {\footnotesize TA}
原文
The basic idea behind the categorical semantics below is that, in order to interpret a programming language in a category
, we distinguish the object {\footnotesize \mathcal{C}} of values (of type {\footnotesize A} ) from the object {\footnotesize A} of computations (of type {\footnotesize TA} ), and take as denotations of programs (of type {\footnotesize TA} ) the elements of {\footnotesize A} . {\footnotesize TA}
In particular, we identify the typewith the object of values (of type {\footnotesize A} ) and obtain the object of computations (of type {\footnotesize A} ) by applying an unary type-constructor {\footnotesize A} to {\footnotesize T} . {\footnotesize A}
We calla notion of computation, since it abstracts away from the type of values computations may produce. {\footnotesize T}
There are many choices forcorresponding to different notions of computations. {\footnotesize TA}
次に計算の概念の例示があります。
EXAMPLE 1.1. We give few notions of computation in the category of sets:
ここでは部分性、非決定性、副作用、例外、継続などが計算概念として示されます。
（詳細は後述しますが、具体的にはListモナドやStateモナドなどが計算概念にあたります。）
そして次に続きます。
さらに（cposの圏で）様々なプログラミング言語の意味論に基づいた例を挙げることができる（Schmidt (1986), Gunter and Scott (1989), Mosses (1989)を参照）。
我々は、特定のに焦点を当てるのではなく、計算のすべての概念に共通する一般的な性質を見出したい。 {\footnotesize T}
本節の目的は、このような要件が、がクライスリトリプル {\footnotesize T} の一部であり、プログラムの圏がこのようなトリプルに対するクライスリ圏であることを、一連の非公式な論証によって読者に納得させることである。 {\footnotesize (T,\mu,-^*)}
原文
Further examples (in a category of cpos) could be given based on the denotational semantics for various programming languages (see Schmidt (1986), Gunter and Scott (1989), and Mosses (1989)).
Rather than focusing on a specific, we want to find the general properties common to all notions of computation; therefore we impose as the only requirement that programs should form a category. {\footnotesize T}
The aim of this section is to convince the reader, with a sequence of informal argumentations, that such a requirement amounts to saying thatis part of a Kleisli triple {\footnotesize T} and that the category of programs is the Kleisli category for such a triple. {\footnotesize (T,\mu,-^*)}
Moggiは「プログラムの圏」は（このようなクライスリトリプルに対する）「クライスリ圏」であると言っているようです。
ではここでいう「プログラム」とは何でしょうか？
MoggiのAn Abstract View of Programming Languagesの「3.2.1 A justification for monad」では、次のように説明されています。
計算の概念をモデル化するためのモナドの使用を正当化するために、我々はプログラムについて次のような直感的な理解を採用する。 プログラムとは値から計算への関数である。
- まず、関数のモデルとして圏
を取り上げ、その上に値と計算の一般的な理解を展開する。 {\footnotesize \mathcal{C}}
より正確には、の対象に単項演算 {\footnotesize \mathcal{C}} を導入し、 {\footnotesize T} 型の値の集合として見た対象 {\footnotesize \tau} を、 {\footnotesize A} 型の計算の集合に対応する対象 {\footnotesize \tau} に写す。 {\footnotesize T A} - そして、
から {\footnotesize A} へのプログラム、つまり {\footnotesize B} 型の値を入力とし、ある計算を実行した後に {\footnotesize A} 型の値を返すプログラムは、 {\footnotesize B} における {\footnotesize \mathcal{C}} から {\footnotesize A} への射とみなすことができる。 {\footnotesize T B} - 最後に、プログラムが適切な圏の射となるように、値と計算に関する最小限の要件を特定する。
これらの3つのステップにより、計算の概念をモデル化するためのクライスリトリプルと、プログラムの圏をモデル化するためのクライスリ圏が導かれる。
原文
In order to justify the use of monads for modelling notions of computations we adopt the following intuitive understanding of programs a program is a function from values to computations.
- First we take a category
as a model for functions and develop on top a general understanding of values and computations. {\footnotesize \mathcal{C}}
More precisely we introduce a unary operationon the objects of {\footnotesize T} , which map an object {\footnotesize \mathcal{C}} viewed as the set of values of type {\footnotesize A} to an object {\footnotesize \tau} corresponding to the set of computations of type {\footnotesize T A} . {\footnotesize \tau} - Then a program from
to {\footnotesize A} , i.e. which takes as input a value of type {\footnotesize B} {\footnotesize A}
and after performing a certain computation will return a value of type{\footnotesize B}
can be identified with a morphism fromto {\footnotesize A} in {\footnotesize T B} {\footnotesize \mathcal{C}} - Finally we identify a minimum set of requirements on values and computations so that programs are the morphisms of a suitable category.
These three steps lead to Kleisli triples for modelling notions of computation and Kleisli categories for modelling categories of programs.
どうやらこの文脈での「プログラム」とは「値から計算への関数」のことを指すようです。
具体的には「A型の値を引数とし、計算(何らかの処理)を実行した後B型の値を返すもの」と書かれていますね。
射としては
そして、この射はクライスリ射と同じ形の射です。
更に「プログラムの圏をモデル化するためのクライスリ圏」とも書かれています。
これがこの節の冒頭に書いた「プログラムの圏をモデル化するためのクライスリ圏」です。
プログラムが、単なる
更に重要なのが、これが圏であるということです。
当たり前のことをいうようですが圏であるということは射（この場合はプログラム）を合成できるわけですから、この射（＝プログラム）の合成により、より大きなプログラムを構成できます。
プログラマーのための圏論(Bartosz Milewski著)(原文)に「合成はプログラミングの本質」と書かれていましたが、納得です。
合成は圏論の根本にあり、圏そのものの定義の一部だ。そして私は、合成こそプログラミングの本質であると強く主張したい。我々は、偉大なエンジニアがサブルーチンのアイデアを思いつく遥か前から、ずっとものを合成してきた。かつて構造化プログラミングはプログラミングに革命をもたらした。コードのブロックを合成可能にしたからだ。続いてオブジェクト指向プログラミングが登場した。これはオブジェクトを合成することこそすべてだ。関数プログラミングは、関数や代数的データ構造を合成するだけでなく、並行性を合成可能にする。これは他のプログラミングパラダイムでは事実上不可能だ。
以上で、この節は終わりなのですが、関数型プログラムの構造化におけるモナドの応用の歴史においてクライスリ圏が関わっているということが多少なりともおわかりいただけたのではないかと思います。
最後に話の流れに影響しないため「詳細は後述します」としていた計算概念の例の話を書きます。
様々な計算概念
ここでは計算概念として様々な
簡素・簡潔に書かれているため最初読んだとき自分はよくわからなかったので、調べてわかったことなどを解説として加えています。
また、計算概念が実際のプログラムではどうなるかを、プログラミング言語PureScriptを用いて説明していきたいと思います。
計算概念については、それぞれ次の3つについて定義が行われます。
\footnotesize T(A) \footnotesize \eta:A\rightarrow T(A) -
\footnotesize f \footnotesize f^*
定義では、具体の
PureScriptを用いた説明では、pure関数、bind(>>=)として説明します。
=<<に対応するものでしたが、>>=は=<<の引数の順序が異なるだけで実質同じものとして扱える上、こちらを使うほうがコードとして読みやすいと考えたためです（個人の主観です）。
また、PureScriptのコードとして説明が難しい計算概念については説明を書きません（いきなり↓のPartialityがそれにあたるのですが）。
partiality (部分性)
-
{\footnotesize T(A)=A_{\bot}} {\footnotesize A+\{\bot \}} {\footnotesize \bot} -
{\footnotesize \eta _{A} :A\rightarrow A_{\bot}} {\footnotesize A} {\footnotesize A_{\bot}} - もし
{\footnotesize f:A \rightarrow T(B)} {\footnotesize f^*(\bot)=\bot} {\footnotesize f^*(a)=f(a)} {\footnotesize a\in A}
解説
コンピューター・サイエンスでは、計算が終了しないか、例外的な状態で終了する場合、計算は発散するといわれます。それ以外の場合は収束すると言われます。プロセス計算など、計算が無限であると予想される領域では、生産的ではない (つまり、有限時間内にアクションを生成し続ける) ことができない場合、計算は発散するといわれます。
ちなみにボトムといいます。
この場合は、発散、つまり呼び出し側に結果を返さないことを知らせるために使われます。（これは必ずしもプログラムが終了に失敗することを意味するわけではありません。サブルーチンは呼び出し側へ戻ることなく終了したり、継続のような他の手段によって脱出する可能性があります）
具体的な
となります。
上記の最初の例を見ると、
そして
この
PureScriptではではどうなるか
この定義のまんまに当てはまるようなものは見つけられませんでした。
Wikipediaのボトム型の記事によると、
理論色の強いプログラミング言語で見られる。産業色の強いプログラミング言語では、一般的にオプション型（タグ付きポインタを含む）や例外処理などの他の手法を使う。
ということのようなので、PureScriptはサポートしていないのかも。
（Partiality Monadというモナドがあるらしいので、別の形ではあるが自前で実装はできるかもしれない）
nondeterminism (非決定性)
\footnotesize T( A) =\mathcal{P}_{\mathrm{fin}}( A) -
\footnotesize \eta _{A} :A\rightarrow \mathcal{P}_{\mathrm{fin}}( A) \displaystyle a\mapsto \{a\} - もし
\footnotesize f:A\rightarrow T( B) \footnotesize c\in T( A) \footnotesize f^{*}( c) =\cup _{x\in c} f( x)
解説
【
まず
次に
つまり
次は具体です。
具体的な
という感じになります。
【
singleton map とは、一元集合への写像
singletonは単一集合のことを指し、その射なのでsingleton mapということですね。
そして
上記の例の
【もし
この場合の
ということは、
これも具体的な値を用いて説明してみます。
上記の
すると各
PureScriptではどうなるか
非決定性はPureScriptでいうと、ArrayやListなどになります。
つまりArray AやList Aですね。
pureの動作を見てみましょう。
Array Stringとします。
つまり
replで確認してみると、定義どおりになっていますね。
> import Prelude
> pure@Array "x"
["x"]
次に
つまりこの場合の
=<<は
>>=は
適当なString -> Array Int型の関数を使って、replで確認してみましょう。
> import Prelude
> import Data.String
> ["ab", "c"] >>= \s -> pure $ length s
[2,1]
> [] >>= \s -> pure $ length s
[]
こちらも計算概念に示された通りになってますね。
side-effect (副作用)
\footnotesize T( A) =( A\times S)^{S} -
\footnotesize \eta _{A} \footnotesize a\mapsto ( \lambda s :S.\langle a,s\rangle ) -
\footnotesize f:A\rightarrow T( B) \footnotesize c\in T( A) \footnotesize f^{*}( c) =\lambda s :S.(\mathrm{let} \ \langle a,s'\rangle =c( s) \ \mathrm{in} \ f( a)( s'))
解説
【
まず
次に
ですのでこれは
【
この射を型つきラムダ計算の表記（より正確にはラムダ計算でいうところのラムダ抽象）で、
つまり
なので
【
まず
続いて内容を見ていきましょう。
なので
- まず状態
{\footnotesize s\in S} {\footnotesize c} {\footnotesize \langle a,s'\rangle} - 次に
{\footnotesize \langle a,s'\rangle} \footnotesize a \footnotesize f(a) {\footnotesize s\rightarrow \langle b,s''\rangle} - 最後に
{\footnotesize \langle a,s'\rangle} \footnotesize s' {\footnotesize s\rightarrow \langle b,s''\rangle}
これが
PureScriptではどうなるか
PureScriptだとこれはStateモナドになります。
s -> (Tuple a s)という感じになるでしょう。
型構築子まで含めると次のようになります。
newtype State s a = State (s -> (Tuple a s))
「なるでしょう」というのは、いまのPureScriptのライブラリのStateモナドは、モナド変換子を用いた定義になっており、↑のようなシンプルな定義にはなっていないからです。
newtype StateT s m a = StateT (s -> m (Tuple a s))
説明では、自前のもので恐縮ですが最初のシンプルなコードの方を使っていきます。
では次にpureを見てみましょう。
pureの実装例はこんな感じになります。
instance applicativeState :: Applicative (State s) where
pure :: forall s a. a -> State s a
pure a = State $ \s -> (Tuple a s)
Stateで包まれてはいますが、
続いて
を見つつbindの実装例を見てみます。
instance bindState :: Bind (State s) where
bind :: forall s a b. State s a -> (a -> State s b) -> State s b
bind m f = State $ \s -> let
(Tuple a s') = runState m s
in runState (f a) s'
runState :: forall s a. State s a -> (s -> (Tuple a s))
runState (State f) = f
runStateはunwrapsして関数を取り出す関数ですが、ここを除いて見ると
exceptions (例外)
-
\footnotesize T( A) =( A+E)
ここで\footnotesize E -
\footnotesize \eta _{A} \footnotesize a\mapsto \mathrm{inl}( a) -
\footnotesize f:A\rightarrow T( B)
\footnotesize e\in E \footnotesize f^{*}(\mathrm{inr}( e)) =e
かつ
\footnotesize a\in A \footnotesize f^{*}(\mathrm{inl}( a)) =f( a)
解説
ただこれは圏論の文脈なので圏論的直和である余積と考えます。
つまり
ということです。
射を合成したとき、例外ならずっと例外のままってことですね。
PureScriptではどうなるか
Eitherになるでしょう。
このPureScriptの実装例ではE,Aの順に定義しています。したがってinl,inrも逆になっていると考えてください。
newtype Except e a = Except (Either e a)
instance applicativeExcept :: Applicative (Except e) where
pure = Except <<< Right
bindの実装例もみてみます。
instance bindExcept :: Bind (Except e) where
bind (Except x) k =
Except (either Left (\a -> case k a of Except b -> b) x)
continuations (継続)
-
\footnotesize T( A) =R^{(R^{A})}
ここで\footnotesize R -
\footnotesize \eta _{A} \footnotesize a\mapsto ( \lambda k) :R^{A} .( k( a)) -
\footnotesize f:A\rightarrow T( B) \footnotesize c\in T( A) \footnotesize f^{*}( c) =\left( \lambda k:\ R^{B} .c( \lambda a:A.f( a)( k))\right)
解説
ですので継続を取り、結果を返す射の集合ということですね。
【
次に
なので、これは単に
【
まず
だから
です。
また
だから
です。
ここまでを前提として、
ラムダ抽象の部分を見ると、
更に
上記から
-
\footnotesize f(a) \footnotesize (B\rightarrow R)\rightarrow R -
\footnotesize k\in (B\rightarrow R) \footnotesize R
なので
ということは
PureScriptではどうなるか
newtype Cont r a = Cont ((a -> r) -> r)
続いて pureです。定義のまんまですね。
instance applicativeCont :: Applicative (Cont r) where
pure a = Cont (\k -> k a)
最後に「bindです。型注釈を多めにつけてます。これも定義どおりに実装できてますね。
instance bindCont :: Bind (Cont r) where
bind :: forall a b. Cont r a -> (a -> (Cont r b)) -> Cont r b
bind (Cont c) f = Cont
(\(k :: (b -> r)) ->
c (\a -> case f a of
(Cont (x :: ((b -> r) -> r))) -> x k))
後書き
クライスリというキーワードは圏論を知る以前から、モナドについて調べていたり、ライブラリのコードを読んでいたりしたときに見かけていました。
例えばPureScriptでは>=>の関数名はcomposeKleisliなのですが、「何がクライスリなんだ？」「クライスリってどういう意味？」と思っていました。
ググっても、クライスリトリプルなんかが出てきてよくわからかったので最初はスルーしました。
圏論でモナドを学び始めた頃、「そろそろいけるだろ」とWikipediaの記事を読んでみたのですが、正直簡単には定義を理解できませんでした。
Moggiが挙げている計算概念の例も同様で、なんかわかりそうでわからないという状態でした。
そんな状態だったのですが、クライスリ圏はここしばらく強い関心をもっていたモナドとの関わりが深そうだということわかってきて、面白みを感じたんですね。
そこから色々調べたり、図式を書いてみたり、関係しそうなプログラムを動かしたり読んだり書いてみたりしていたのですが、実際これがなかなか面白かったので記事にしてみました。
みなさまも楽しんでいただけたら幸いです。
Discussion