String diagram のすすめ
こちらは Haskell Advent Calendar 2015 - Qiita の 20 日目の記事です。
- 前の日・・・Hakyllでブログを作る(実践編) - Wake up! Good night*
- 次の日・・・「第2期 H本読書会 in 秋葉原」を終えて #readhbon #haskell - セカイノカタチ
String diagram
String diagram というのは 圏論の bicategory というのを、平面上の点と線を使って描くものなんですが、特にややこしい知識が無くても使える(使っている)、と思ったので記事にしました。
以下、圏論の知識は必要ありません。
垂直方向について
型を縦線で表現し、関数は縦線上のノードで表現します:
諸般の事情で四角になってますが、ノートに書くときは丸でも何でもかまいません。
定義域a
が下になっていることに注意。
関数id = \a -> a
のノードは(特に明示したい場合を除いて)省略します:
縦線をつなぐのが composition.
です:
演習問題.1
- 関数
id
が省略されていてもされてなくても矛盾がないことを確認してください。
水平方向について
縦線2本で tuple 型を表現します:
水平に並んだ関数二個について、次のように定義します:
水平方向を先に計算しても垂直方向を先に計算しても等しい:
ので
と括弧なしに描けます。
特に、関数id
を代入すると:
これによって関数は線上を自由に移動できます。
このような移動が直感的であることが string diagram のキモになります。
演習問題.2
- 水平方向を先に計算しても垂直方向を先に計算しても等しいことを確認してください。
Tuple 型について
Unit 型()
は(特に明示したい場合を除いて)描きません:
以上の定義から、縦線が3本以上になると解釈に困ります:
Unit 型は省略できるので、幾通りでも解釈できるのです・・・が、気にしません。ソースコードに落とす時は、
\((a,b),c) -> (a,(b,c))
等々を補完してつなげます。
Value
値は、定義域を unit 型とする関数で表現します:
Point-free 化
定義:
により、同じ変数が下にくっ付いていれば消せます。
Symmetry
次のような交差点を表す関数を symmetry といいます:
(右前の方が縁起が良いらしい。)
交差点を何回も使えば3個以上の tuple も如何様にも並べ替えられます。
関数は交差点も自由に移動できます:
Function type
関数の型のために特別な縦線を定義します:
左右が逆になっていることに注意。
例えばfmap
は:
Currying
右側の足を上げたり下げたりするのが currying です:
curry/uncurry したもの同士は区別しないことにします:
特に、全部の足を上げたら値になります:
関数の composition.
は次にように描きます:
さらに
とすると
線のたるみをピンと張る、みたいな感じ。
これらを使うと、垂直方向と水平方向を直感的に変換できます:
線を束ねたり垂らしたりする感じ。
演習問題.3
- Functor 則 を描いてみてください。
- 足が3本以上の場合の composition の図を定義してください。
関数の箱
以上の定義より、string diagram は単に expression tree を作ってるだけ・・・となり、色んな law を描いてもあまりうれしくなりません。そこで関数に次のような箱を使います:
Functoriality @deprecated
代わりに
- 1-natural transformations in string diagrams - PS
- Monoidal natural transformations in string diagrams - PS
- Applicative functors in string diagrams rev.2 - PS
を参照してください。
<deprecated>
箱を分割しても合体しても等しくなる性質を functoriality と言います。
特に、垂直方向でそれが出来るのがFunctor
です:
さらに、足が分かれていてもそれが出来る*1のがApplicative
です:
箱の底辺で型が合ってない所がありますが、気にしません。詳しくは・・・こちら*2。
</deprecated>
演習問題.4
- 実はすでに functoriality がひとつ出てきていました。どこでしょうか。
- 関数
curry
の functoriality を描いてみてください。
Naturality
ノードが箱に出たり入ったりできる性質を naturality と言います。例えばtraverse
:
箱の型を壊してしまうような移動はできません。
基本的に polymorphic な関数はなんらかの naturality を持ちます。
演習問題.5
- 関数
curry
の naturality を描いてみてください。
箱の鍵
箱に鍵が与えられている場合があります。例えばreturn
:
fst
や snd
も鍵の一種です。鍵を開けたらまた閉じ込められる、なんて箱もあります。
Anonymous function
無名関数を自分は以下のように書いています:
変数x
(のスコープ)が閉じ込められているということを箱の隅に明記しています。
底辺に書いているのは鍵穴の位置が下側だからです。鍵が何かはお分かりですね。
さて、return
も型引数からの関数と考えられるので
と出来ますが、箱の外側はどうなるのでしょうか。
実は新たな string diagram の世界が広がっています。ここから先は圏論で・・・。
まとめ
String diagram を使うと、一見恐ろしい law の数々を視覚的に記憶し適用できます。特に naturality に関して劇的です。何重にもなっている箱を一気に移動できます。
この記事では、expression tree になるような描き方を採用しましたが、この描き方で決まっているというわけではありません。寝かせたり、反転させたり、逆さにする方法もあります。かっこいい図の描き方を考えるのも面白いです。