６．２ 関手の証明
かつてバークレイの大学院生だった頃に指導教授からプログラムの正当性を研究テーマにしてみないかと誘いを受けたことがある。当時のプログラミング言語と言えばFortlanで、構造がぐしゃぐしゃなプログラムを検証することなど不可能だと直感的に感じて断った経験がある。
純関数型言語を使えるようになった今日ではプログラムの検証は随分と簡単になった。今回の記事で紹介するのもその一つである。Maybeが関手であること、即ち、構造を保持していることを証明しよう。
圏の定義を確認しておこう。
1) 対象\(A,B,C,..\)を有する。
2) 射\(f,g,h,..\)を有する。
3) 射はドメインとコドメインを有する。これらは対象である。
4) すべての対象に対して恒等射が存在する。
5) コドメインとドメインが一致している射は合成でき、それも射となる。
さらに、圏は次の二つの法則を満たさなければならない。
① 結合律。
② 単位律。
さらに、関手についても確認しておこう。圏論での関手の可換図式は次のようである。
この図で重要なところは、構造を保持しているところで、それらは、
\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\)の可換図式は次のようになっていた。
証明すべき項目は以下のとおりである。
\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\)を一般化する。
