Theorems for free
Parametricity
Naturalityを一般化した概念であるらしい。
Collorary
Parametricity theoremより直ちに、二つのfunctor:
について、morphism族:
は、常にnatural。
CoYoneda functor
data CoYoneda f a = forall b. CoYoneda (b -> a) (f b)
とすると、data constructorはこんな感じになっている:
Theorems for free
上のcolloraryにより、 は、 についてnaturalになる:
これを使うと、(CoYoneda functorのことは何も知らないのに)
を証明できる。