fmapの一意性
命題
Functor:
について、
を満たす関数族:
が存在するならば、
証明
Free theoremにより、 は、 についてfreely naturalなので
vs. Applicative
\f -> \x -> pure f <*> x
は、functorialなので、上記の命題より
fmap f x = pure f <*> x
Functor:
について、
を満たす関数族:
が存在するならば、
Free theoremにより、 は、 についてfreely naturalなので
\f -> \x -> pure f <*> x
は、functorialなので、上記の命題より
fmap f x = pure f <*> x