パラメトリシティを使って自由モノイドが構成できることの証明

目的

この記事では、以下のように定義したFMが、一定の条件のもとで自由モノイドになっていることをパラメトリシティを使って証明したい。

動機としては、https://qiita.com/lotz/items/424abee02fe598c60247 のコメント欄における$\bar f$の一意性についての議論に答えを出したかった。

{-# LANGUAGE RankNTypes #-}
module FM where

newtype FM a = FM { runFM :: forall m. (Monoid m) => (a -> m) -> m }

instance Semigroup (FM a) where
  FM a <> FM b = FM (\k -> a k <> b k)

instance Monoid (FM a) where
  mempty = FM (\_ -> mempty)

embed :: a -> FM a
embed x = FM (\k -> k x)

foldMap :: (Monoid m) => (a -> m) -> FM a -> m
foldMap f (FM g) = g f

前提条件

以下を仮定する。

• Free theoremが成立するようなHaskellのサブセットで考える。具体的には、seqと⊥については考慮しない。
• 関数の外延性を仮定する。つまり、同じ引数に対して同じ値を返す関数は、実行効率などの点で違いがあっても、同じとみなす。

また、証明の中ではnewtypeを付けたり外したりする関数FMとunFMを省略して書く。

命題0

foldMap fはモノイド準同型である。

証明

定義を展開すれば分かる。

命題1

fが関数で、uがモノイド準同型であるとき、

foldMap (u . f) = u . foldMap f

証明

型forall m. (Monoid m) => (a -> m) -> mについてのfree theoremを計算すると、この型の項tは以下の性質を満たすことが分かる。

任意の関数fと、任意のmemptyと(<>)を保存する関数uについて、t (u . f) = u . t f

ただし、「uがmemptyと(<>)を保存する関数である」とは、任意のa、bについて以下が成り立つことである。

u mempty = mempty
u (a <> b) = u a <> u b

uはモノイド準同型だから、memptyと(<>)を保存する。foldMapの定義を使うと、示すべき命題が示される。

命題2

任意のfについて、

foldMap f . embed = f

証明

定義を展開すれば分かる。

命題3

foldMap embed = id

証明

foldMap embed g fを変形していく。

foldMap embed g f
= {foldMapの定義を逆向きに使う}
  foldMap f (foldMap embed g)
= {命題1を内側のfoldMapに適用する。命題0よりこれは許される}
  foldMap (foldMap f . embed) g
= {命題2}
  foldMap f g
= {foldMapの定義}
  g f

外延性の仮定から、foldMap embed = idがいえる。

命題4

FM aはaをアルファベットとする自由モノイドである。

証明

「任意のfについて、h . embed = fを満たすモノイド準同型hが唯一つ存在する」を示せばよい。

このようなhが存在して、foldMap fで与えらえることは命題2と命題0から分かる。

次に一意性を示す。このようなhが他にも存在したとすると、

foldMap f
= {仮定より}
  foldMap (h . embed)
= {命題1}
  h . foldMap embed
= {命題3}
  h

従って、このようなhは全てfoldMap fに等しく、よって一意である。これで証明できた。