圏論と関数型プログラミング

2014くらいからやってるんですが、そんなに難しい離しでもない。要するに、

　　型を対象、関数を射と呼ぶと圏になる

というだけなので。

関手は型変数a を持つ data F a とaに対する fmap。自然変換はF
aからG bへのdataの変換で、f : a -> b に対して可換なもの。木
をリストに変換する flatten : tree a -> [ a ] とか。

自然変換がfmapに対して可換なdata構造の変換ってのはわかりやすいよね。

何の役に立つかというと、fmap とか可換性とかで、コードが満たしている性質、
要するに invariant が見やすくなるというだけ。

Monad は Maybe a で理解するのが良い。関手であることは fmap があるからすぐにわかる。
mu : Maybe (Maybe a) -> Maybe a
return : a -> Maybe a
は当たり前でしょ。

g : a -> Maybe b
f : b -> Maybe c

で、f (g x) とは書けないけど、mu (fmap f (g x)) で意味が通ると気がつけば良い。

fst x , snd x) が x に等しいっていうのが、pair の uniqueness だが、これがLimit とか普遍問題の解とか表現可能関手とかいろいろ言われてるだけではある。

　　c
　　|
　　v
a <- (a,b) -> b

で、h : c -> (a ,b) があれば、f : c -> a : h (fst x) を作れる。圏論の用語が煙幕なだけで本質は簡単。

Proofs and types には圏論は一切出てこない

Natural deductionとsequent calculus、system Tとsystem F

さらにsystem Fの強正規化、sequent calculusのcut eliminationが載ってる

しかも、薄い！素晴らしい本だ
http://paultaylor.eu/stable/prot.pdf

圏論だと少し勧めにくいけど、

Introduction to Higher-Order Categorical Logic
https://t.co/avsLk9iCjF

を使ってて、わからないところがあると、

Categories for the Working Mathematician
https://t.co/k2jDYFtixH

を使ってます。