PS

String diagram のすすめ

こちらは Haskell Advent Calendar 2015 - Qiita の 20 日目の記事です。

String diagram

String diagram というのは 圏論bicategory というのを、平面上の点と線を使って描くものなんですが、特にややこしい知識が無くても使える(使っている)、と思ったので記事にしました。

以下、圏論の知識は必要ありません。

垂直方向について

型を縦線で表現し、関数は縦線上のノードで表現します:

f:id:mbps:20151117072706p:plain

諸般の事情で四角になってますが、ノートに書くときは丸でも何でもかまいません。

定義域aが下になっていることに注意。

関数id = \a -> aのノードは(特に明示したい場合を除いて)省略します:

f:id:mbps:20151117072713p:plain

縦線をつなぐのが composition.です:

f:id:mbps:20151117072943p:plain

演習問題.1

  1. 関数idが省略されていてもされてなくても矛盾がないことを確認してください。

水平方向について

縦線2本で tuple 型を表現します:

f:id:mbps:20151117094152p:plain

水平に並んだ関数二個について、次のように定義します:

f:id:mbps:20151121213039p:plain

水平方向を先に計算しても垂直方向を先に計算しても等しい:

f:id:mbps:20151117074229p:plain

ので

f:id:mbps:20151121213057p:plain

と括弧なしに描けます。

特に、関数idを代入すると:

f:id:mbps:20151121213111p:plain

これによって関数は線上を自由に移動できます。

このような移動が直感的であることが string diagram のキモになります。

演習問題.2

  1. 水平方向を先に計算しても垂直方向を先に計算しても等しいことを確認してください。

Tuple 型について

Unit 型()は(特に明示したい場合を除いて)描きません:

f:id:mbps:20151117075650p:plain

以上の定義から、縦線が3本以上になると解釈に困ります:

f:id:mbps:20151117075713p:plain

Unit 型は省略できるので、幾通りでも解釈できるのです・・・が、気にしません。ソースコードに落とす時は、

\((a,b),c) -> (a,(b,c))

等々を補完してつなげます。

Value

値は、定義域を unit 型とする関数で表現します:

f:id:mbps:20151121212017p:plain

Point-free 化

定義:

f:id:mbps:20151121211334p:plain

により、同じ変数が下にくっ付いていれば消せます。

Symmetry

次のような交差点を表す関数を symmetry といいます:

f:id:mbps:20151126131319p:plain

(右前の方が縁起が良いらしい。)

交差点を何回も使えば3個以上の tuple も如何様にも並べ替えられます。

関数は交差点も自由に移動できます:

f:id:mbps:20151126131324p:plain

Function type

関数の型のために特別な縦線を定義します:

f:id:mbps:20151117091955p:plain

左右が逆になっていることに注意。

例えばfmapは:

f:id:mbps:20151117085841p:plain

Currying

右側の足を上げたり下げたりするのが currying です:

f:id:mbps:20151117181659p:plain

curry/uncurry したもの同士は区別しないことにします:

f:id:mbps:20151121184702p:plain

特に、全部の足を上げたら値になります:

f:id:mbps:20151117181706p:plain

関数の composition.は次にように描きます:

f:id:mbps:20151117090817p:plain

さらに

f:id:mbps:20151117090844p:plain

とすると

f:id:mbps:20151117090849p:plain

線のたるみをピンと張る、みたいな感じ。

これらを使うと、垂直方向と水平方向を直感的に変換できます:

f:id:mbps:20151118081555p:plain

線を束ねたり垂らしたりする感じ。

演習問題.3

  1. Functor 則 を描いてみてください。
  2. 足が3本以上の場合の composition の図を定義してください。

関数の箱

以上の定義より、string diagram は単に expression tree を作ってるだけ・・・となり、色んな law を描いてもあまりうれしくなりません。そこで関数に次のような箱を使います:

f:id:mbps:20151117081127p:plain

Functoriality @deprecated

代わりに

を参照してください。

<deprecated>

箱を分割しても合体しても等しくなる性質を functoriality と言います。

特に、垂直方向でそれが出来るのがFunctorです:

f:id:mbps:20151117081410p:plain

さらに、足が分かれていてもそれが出来る*1のがApplicativeです:

f:id:mbps:20151117081420p:plain

箱の底辺で型が合ってない所がありますが、気にしません。詳しくは・・・こちら*2

</deprecated>

演習問題.4

  1. 実はすでに functoriality がひとつ出てきていました。どこでしょうか。
  2. 関数curry の functoriality を描いてみてください。

Naturality

ノードが箱に出たり入ったりできる性質を naturality と言います。例えばtraverse:

f:id:mbps:20151120002712p:plain

箱の型を壊してしまうような移動はできません。

基本的に polymorphic な関数はなんらかの naturality を持ちます。

演習問題.5

  1. 関数curryの naturality を描いてみてください。

箱の鍵

箱に鍵が与えられている場合があります。例えばreturn:

f:id:mbps:20151209131522p:plain

fstsnd も鍵の一種です。鍵を開けたらまた閉じ込められる、なんて箱もあります。

Anonymous function

無名関数を自分は以下のように書いています:

f:id:mbps:20151209130207p:plain

変数x(のスコープ)が閉じ込められているということを箱の隅に明記しています。
底辺に書いているのは鍵穴の位置が下側だからです。鍵が何かはお分かりですね。

さて、returnも型引数からの関数と考えられるので

f:id:mbps:20151217130126p:plain

と出来ますが、箱の外側はどうなるのでしょうか。
実は新たな string diagram の世界が広がっています。ここから先は圏論で・・・。

まとめ

String diagram を使うと、一見恐ろしい law の数々を視覚的に記憶し適用できます。特に naturality に関して劇的です。何重にもなっている箱を一気に移動できます。

この記事では、expression tree になるような描き方を採用しましたが、この描き方で決まっているというわけではありません。寝かせたり、反転させたり、逆さにする方法もあります。かっこいい図の描き方を考えるのも面白いです。

参考文献

*1:圏論では lax functoriality と言います

*2:リンク先の図は左右が反転されてます