Arrow

1992年、「非常に複雑で習得するのが難しいため、誰にもプログラマ市場をあふれさせることができないような言語があったとしたら、どうだろう。」と、Wadlerは考えました。実際のところは、C++、つまり、Stroustrupからアイディアをいただいたんですが。そして、あらゆる実用的なプログラミングを複雑にするためにMonadを導入しました。ところが、Wadlerの意に反して、Haskellerたちは、Monadを難無く使いこなすようになりました。事態を憂いたHughesは、1998年、Monadが関わる対象の扱いを、もっとずっと複雑で習得が困難なものとするためにArrowを発明しました。Monad lawはたった3つしかないのに、Arrow lawは、20以上もあります。これは、もはや人間に制御しきれるレベルではありません。

というわけはなくて。少しずつArrowが理解できてきたような。基本的っぽい文献
[1]Generalising Monads to Arrows
Arrow導入の動機をパーサー使って説明している
[2]Arrows and computation
Arrow lawをきちんと書き下してあるので珍しい気が。しかし多分あまり役には立たない

Monadと同様、圏論の概念と関係があるらしいけど、よくわからないね。まず、Arrow以前の話で、考察の対象とするのは、型をObjectに持つような圏Typeで、Tupleに対応する積と、関数型に対応するinternal hom(exponential functorとか呼ばれることもある)を持つ。個人的には、型の和(Either)も基本的だと思うんだけど、それはいいとして、Typeはclosed monoidal categoryてことかな。

Typeの対象s,tに対して、積をT(s,t)と書いて、internal homをhom(s,t)と書く。Haskellでは、単にTupleと"s -> t"のこと。あと、普通のHomを、[s,t]と書く。[s,t]は単なる集合で、hom(s,t)はTypeのobjectという違いがあるんだけど、この二つは同一視したいよね〜。enriched-categoryとかいうので説明すればいいのかもしれない。で、関手_->hom(_,t)は関手_->T(_,t)の右随伴;
[T(s,t) , u] `equiv` [s , hom(t,u)]
これは大体Curry化なんだけど、Curry化は本来、
hom(T(s,t) , u) `equiv` hom(s , hom(t,u))
となるべき。このへんどう正当化すればいいのか分からないけど、とりあえず、internal homについても、curry化が成り立っているとする。

で、Arrowはhomに似たbifunctorのようなもの。これを単に、A(s,t)と書く。これは、丁度Kleisli構成で、Monad mから、[s , m t]で新しいHomを導入するのの一般化。internal homの方でいうと、
A[m](s , t) = hom(s, m t)
mはモナド。この場合、(internal homに対するcurry化が成立すれば)
A[m](T(s,t),u) `equiv` hom(s , A[m](t,u))
が成り立つ。実際に、
A[m](T(s,t),u) = hom(T(s,t) , m u) `equiv` hom (s , hom(t, m u)) = hom(s , A[m](t,u))

で、これはA[m]のみならず、一般のArrow Aについて成り立つ(というか、公理と考えるべきなのか)。[2]でcurryingとか書いてるのに相当。んで、Typeと同じObjectと積を持って、HomがAと「同一視」できるような圏Type'を考えると、premonoidal category(ってなに?)になってますよ、とか、そんな感じなのかな？

(>>>)はType'に於ける射の合成で、arr([2]ではpureと書いてる)はTypeからType'への関手と見なせばいい？(&&&)とか謎の演算子はよくわからない。まあ、bind :: (s -> m t) -> (m s -> m t)とかより、arr :: (s -> t) -> (a s t)の方が分かりやすい気はする。ArrowもMonadもない言語では、"getchar :: () -> char"、"putchar :: char -> ()"という型が自然なんだけど、副作用があるから、"getChar::IOArrow () Char" , "putChar::IOArrow Char ()"みたいに書く感じ。IOモナドから、IOArrowみたいなのを作り出すのが、Kleisli(任意のモナドからArrowを作れる)で、Control.Arrowで定義されている。但し、HaskellでのgetCharの型は、"()->IO Char"ではなく、"IO Char"なので、Kleisliで素直に持ち上げれないという欠点が。ショボーン
で、こんな感じ。

import Control.Arrow

type IOArrow a b = Kleisli IO a b

getCharA :: IOArrow () Char
getCharA = Kleisli (\_ -> getChar)
putCharA :: IOArrow Char ()
putCharA = Kleisli putChar

appA proc x = case proc of
 Kleisli f -> f x

main = appA (getCharA>>>putCharA) ()

Kleisliは、多相型名であると同時に、型構成子名でもあるので、ややこしい。というか、多相型名=型構成子名なのって、よく見るけど、みんな混乱しないのか？とりあえず、関数としてのgetCharが復権できてよかったね。んー、monadよりも直感的で扱いは楽かも。

それから、不動点コンビネータのArrow版
fixA :: (Arrow a) => a (a t t) t
が存在するべきです。

(メモ)enriched-caterogyに対する米田の補題みたいなのがあれば、internal homからHom集合を復元できるのかもしれない。で、"Arrow Functor"(造語)からも同様にして、それをinternal homとするようなHomが作れて云々というストーリーに。気が向いたら考える

(2006/10/19追記)
Computational Applications of calculi based on Monads
を眺めていたら、closed monoidal categoryのinternal homとHomの対応はもっと簡単に与えられていた;
[s , t] `equiv` [1 , hom(s,t)]
うーむ。単位元(Haskellの()型。Ocamlとかだと、unit型とか呼ばれてるんだっけ)の存在忘れてたね。
T(1 , t) `equiv` T(t , 1) `equiv` t
なので、上の対応は、Curry化の特殊な場合でもある。

それで、internal homに対するCurry化。
[1 , hom(T(s,t) , u)] `equiv` [T(s,t) , u] `equiv` [s , hom(t,u)] `equiv [1 , hom(s , hom(t,u))]
えーと、[1 , X] `equiv` [1 , Y]から、X `equiv` Y導いていいのかな？ダメな気が･･･

premonoidal categoryというのは、[A,B]の射fと[C,D]の射gから、[T(A,C) , T(B,D)]の射を得る方法が、T(A,C)->T(B,C)->T(B,D)を経由するのと、T(A,C)->T(A,D)->T(B,D)を経由するのと二通りあるけど、それらが一致しないらしい。よくわからないけど。

以下よくわからない点
・Kleisli categoryがpremonoidalになるのは、Strong Monadの時のみなのに、Arrowの方は、Monadに対して、そんな仮定を必要としてない(と思う)
・時々、Kleisli exponentialと呼ばれてる概念は、Arrowのことではないの？元の圏が、closed monoidalなら、Kleisli exponentialはいつでも存在する気がするけど

うーん、まだ色々混乱してる気がする。圏論は嫌いだ。こんなんで悩むのも不毛だけど、すっきりしないなー。