PS

Functor則

圏論命題 Haskell Free-theorem

Free theoremのもと、いわゆるfunctor則は一つでいいらしい。

命題

$\mathcal{Hask}$ における型族:

$(F _ A) _ A$

について、

$\mathtt{fmap}(1 _ A) = 1 _ {F A}$

を満たす関数族:

$(\mathtt{fmap} _ {A , B} : (A \to B) \to (F A \to F B) ) _ {A, B}$

が存在するならば、

$\mathtt{fmap}(f \circ g) = \mathtt{fmap}(f) \circ \mathtt{fmap}(g)$

証明(の試み)

関数:

$a: A \to A'$

のrelationによる表現:

$\mathcal{A} := \mathsf{graph}(a) = \lbrace (x, a(x)) \mid x \in A \rbrace : A \Leftrightarrow A'$

について、relation:

$F \mathcal{A} := \mathsf{graph}(\mathtt{fmap}(a)) = \lbrace (x, \mathtt{fmap}(a)(x)) \mid x \in FA \rbrace : FA \Leftrightarrow FA'$

を定義できて*1、 $(\mathtt{fmap} _ {A , B}) _ {A, B}$ のparametricity:

$f' \circ a = b \circ f \implies \mathtt{fmap}(f') \circ \mathtt{fmap}(a) = \mathtt{fmap}(b) \circ \mathtt{fmap}(f)$

が得られる。

参考文献

*1:このrelationが有効なのか分からない