bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

関手ー関手であることの証明

6.2 関手の証明

かつてバークレイの大学院生だった頃に指導教授からプログラムの正当性を研究テーマにしてみないかと誘いを受けたことがある。当時のプログラミング言語と言えばFortlanで、構造がぐしゃぐしゃなプログラムを検証することなど不可能だと直感的に感じて断った経験がある。

関数型言語を使えるようになった今日ではプログラムの検証は随分と簡単になった。今回の記事で紹介するのもその一つである。Maybeが関手であること、即ち、構造を保持していることを証明しよう。

圏の定義を確認しておこう。
1) 対象\(A,B,C,..\)を有する。
2) 射\(f,g,h,..\)を有する。
3) 射はドメインとコドメインを有する。これらは対象である。
4) すべての対象に対して恒等射が存在する。
5) コドメインドメインが一致している射は合成でき、それも射となる。
さらに、圏は次の二つの法則を満たさなければならない。
①  結合律。
②  単位律。

さらに、関手についても確認しておこう。圏論での関手の可換図は次のようである。
f:id:bitterharvest:20170217084834p:plain

この図で重要なところは、構造を保持しているところで、それらは、
\begin{eqnarray}
F(id_A)=id_{F(A)} \\
F(id_B)=id_{F(B)} \\
F(id_C)=id_{F(C)} \\
F(g \circ f) = F(g) \circ F(f)
\end{eqnarray}
である。

Haskellで、関手を定義するときは、上記が成り立っているかどうかを確認しなければならない。プログラムの方は検証をしてくれないので、検証は開発者の責任となる。

それでは、\(Maybe\)が構造を保持しているかどうかを証明することにしよう。
\(Maybe\)の可換図は次のようになっていた。
f:id:bitterharvest:20170217090107p:plain
証明すべき項目は以下のとおりである。
\begin{eqnarray}
fmap \ id_a = id_{Maybe \ a} \\
fmap \ id_b = id_{Maybe \ b} \\
fmap \ id_c = id_{Maybe \ c} \\
fmap \ (g \circ f) = fmap \ g \circ fmap \ f
\end{eqnarray}
である。

それでは証明に移ろう。\(fmap\)は次のように定義していた。

fmap :: (a -> b) -> (f a -> f b)
fmap f Nothing = Nothing
fmap f (Just x) = Just (f x)

である。

ここで、先ほどから使用している\(a,b,c\)は型変数である。前の記事では言葉で説明したが、数学的に記述すると次のようになる。対象の集まりを\(\mathcal {O} = {A,B,C,…}\)とする。型シグネチャのところで\((a -> ...)\)と現れるが、このときの\(a\)は\(\forall a,b,c \in \mathcal {O} \)の意味である。\(\forall\)は全称記号で「任意の」という意味である。即ち、\(a\)は、\(\mathcal {O}\)の要素\(A,B,C,..\)のどれに対してもということになる。

そこで、\(fmap \ id_a = id_{Maybe \ a}\)を証明することとしよう。いま\(id\)を次のように定義する。

id :: a -> a
id x = x

上の定義の\(f\)を\(id\)で置き換えると

fmap id Nothing = Nothing
fmap id (Just x) = Just (id x)

\(id\)の定義より以下が成り立つ。

id Nothing = Nothing

CやJavaなどの逐次型プログラミング言語では\(=\)は代入式であるが、純関数型言語Haskellでは\(=\)は等価、即ち\(==\)である。プログラムで確認してみよう。

Prelude> :t id
id :: a -> a
Prelude> id 3 == 3
True
Prelude> 3 == id 3
True
Prelude> id (Just 5) == Just 5
True
Prelude> Just 5 == id (Just 5)
True

従って、左辺を右辺で、右辺を左辺で置き換えることが可能である。そこで、\(Nothing\)を\(id \ Nothing\)で置き換えると、

fmap id Nothing = Nothing = id Nothing
fmap id (Just x) = Just (id x)

つぎに、2番目の式についても変形してみよう。

id x = x

より、

fmap id Nothing = Nothing = id Nothing
fmap id (Just x) = Just x

また、

id (Just x) = Just x

より、\(Just \ x\)を\(id \ (Just x)\)で置き換えると次のようになる。

fmap id Nothing = Nothing = id Nothing
fmap id (Just x) = id (Just x)

それでは次の\(fmap \ (g \circ f) = fmap \ g \circ fmap \ f\)を証明しよう。

fmap (g . f) Nothing = Nothing
fmap (g . f) (Just x) = Just ((g . f) x)

原理は先ほどと同じなので、式の変形だけを示そう。最初の式は、

fmap (g . f) Nothing = Nothing
                     = fmap g Nothing
                     = fmap g (fmap f Nothing)
                     = ((fmap g) . (fmap f)) Nothing

最後の式は、

fmap (g . f) (Just x) = Just ((g . f) x)
                      = Just (g (f x))
                      = fmap g (Just (f x))
                      = fmap g (fmap f (Just x))
                      = ((fmap g) . (fmap f)) (Just x)

これにより、\(Maybe\)が関手の条件を満たしていることが証明できた。

次回は、\(fmap\)を一般化する。