PS

Theorems for free

Parametricity

Naturalityを一般化した概念であるらしい。

Collorary

Parametricity theoremより直ちに、二つのfunctor:

  •  F, G : \mathcal{Hask} \rightarrow \mathcal{Hask}

について、morphism族:

  •  (\alpha _ A : FA \rightarrow GA ) _ A

は、常にnatural。

CoYoneda functor

data CoYoneda f a = forall b. CoYoneda (b -> a) (f b)

とすると、data constructorはこんな感じになっている:

  •  \tau_{A,\ B}\ :\ \text{Hom}(B,\ A) \rightarrow \text{Hom}(F(B),\ \text{CoYoneda}_F(A) )

Theorems for free

上のcolloraryにより、 (\tau_{A,\ B})_{A,\ B} は、 B についてnaturalになる:

f:id:mbps:20131018144623p:plain

これを使うと、(CoYoneda functorのことは何も知らないのに)

  •  \text{CoYoneda} _ F \cong F

を証明できる。

参考文献