Gabriel Bonzalez氏のブログ記事Haskell for All: Comonads are objectsでは、Comonad則の証明問題がいくつかExerciseとして出題されています。このページでは、その証明問題の解答例を示します。
元記事：Haskell for All: Comonads are objects
本ページでは、元記事内で出題されているExerciseへの解答例を示すことを目的としています。記事の内容自体についての説明はほとんどありませんが、元記事を読む際の参考にしていただければと思います。
下記記事も参考となります。
Comonadはオブジェクト？ - Mizon Dev Diary
Comonad則
元記事の後半にも示されていますが、Comonadとは、型コンストラクタwと2つの関数extract :: w a -> a、extend :: (w a -> b) -> w a -> w bから構成されるものです(<`w`, `extract`, `extend`>)。ただし、extractとextendは以下に示すComonad則を満たす必要があります。
Comonad則:
extend extract = id -- 第1則
extract (extend f x) = f x -- 第2則
extend (\x' -> g (extend f x')) x = extend g (extend f x) -- 第3則
抽象的でよくわからないですね。
ともあれ、元記事ではオブジェクト指向プログラミングで用いられる3つのデザインパターン、Builder Pattern、Iterator Pattern、Command Patternを例として取り上げ、各パターンに対してそのパターンの働きをうまく再現するようなextractとextendを定義しています。各パターンで定義されたextractとextendが実際にComonad則を満たすことを証明することで、これらのパターンがComonadとしての構造を持つことを示しています。(さらには一般のオブジェクト指向プログラミングがComonadとしての構造を持つことを示しています)
さて、各パターンで定義されたextractとextendがComonad則を満たすことを示す証明の一部が、元記事ではExerciseとなっています。本ページではそのExercise(Comonad則の証明問題)の解答例を示します。Builder Pattern、Iterator Pattern、Command PatternのそれぞれでExerciseがありますが、まずはBuilder Patternからです。Iterator PatternとCommand PatternでのExerciseの解答例は別ページにて示します。
The Builder Pattern
型の定義
type Option = String
data Config = MakeConfig [Option] deriving (Show)
複数のoptionを与えてconfigを生成する関数すなわち[Option] -> Config型の関数をbuilderと呼ぶことにします。また、builderに作用してconfigを生成する([Option] -> Config) -> Config型の関数を(option) setter, builderから新たなbuilderを生成する([Option] -> Config) -> ([Option] -> Config)型の関数を(option) appenderと呼びます。
extract,extendの定義
Builder pattern でのextractとextendの定義は以下のように与えられています。
-- Definition of extract
extract :: ([Option] -> Config) -> Config
extract builder = builder [] -- (1-1)
-- Definition of extend
extend :: (([Option] -> Config) -> Config)
-> ([Option] -> Config) -> ([Option] -> Config)
extend setter builder =
\opts2 -> setter (\opts1 -> builder (opts1 ++ opts2)) -- (1-2)
extractはbuilderに空のoptionを与えてconfigを得る、もっとも基本的なsetterです。extendはsetterをappenderに変換するものです。
記事を先回りして言うと、以下のように定義された型コンストラクタBuilderと上記のextract、extendによってComonad <`Builder`, `extract`, `extend`>が構成されるようです。
type Builder a = [Option] -> a
Comonad則の証明
では、Excerciseに取り組んでいきます。まず、第1則の証明問題です。
Exercise: Prove that:
extend extract builder = builder -- (2-1)
証明:
extend extract builder -- (2-1)の左辺
-- extendを展開 (1-2)
= \opts2 -> extract (\opts1 -> builder (opts1 ++ opts2))
-- extractの定義を適用 (1-1)
= \opts2 -> (\opts1 -> builder (opts1 ++ opts2)) []
-- (\opts1 -> *)への関数適用
= \opts2 -> builder ([] ++ opts2)
-- [] ++ opts2 = opts2
= \opts2 -> builder opts2
-- 一般に f = \x -> f x
= builder -- (2-1)の右辺 //
第2則
extract (extend setter builder) = setter builder
の証明は記事内にて示されてますので省略します。
では第3則の証明問題です。
Challenge exercise: Prove that:
s1, s2 :: ([Option] -> Config) -> Config -- setters
b, b :: [Option] -> Config -- builders
extend (\b' -> s2 (extend s1 b') b = extend s2 (extend s1 b) -- (3-1)
証明:
(証明方針:左辺、右辺ともにextendを定義に従って展開し、(++)の結合則をもちいて両者が等しくなることを示す。)
-- まず左辺を展開する。
extend (\b' -> s2 (extend s1 b')) b -- (3-1)の左辺
-- 外側のextendの展開 (1-2)
= \opts2 -> (\b' -> s2 (extend s1 b')) (\opts1 -> b (opts1 ++ opts2))
-- (\b' -> *)への関数適用
= \opts2 -> s2 (extend s1 (\opts1 -> b (opts1 ++ opts2)))
-- 残った内側のextendの展開 (1-2)
= \opts2 -> s2 (\opts4 -> s1 (\opts3 -> (\opts1 -> b (opts1 ++ opts2)) (opts3 +++ opt4)))
-- (\opts1 -> *)への関数適用
= \opts2 -> s2 (\opts4 -> s1 (\opts3 -> b ((opts3 ++ opts4) ++ opts2)))
-- 束縛変数 opts2, opts4, opts3の変数名をそれぞれopts', opts'', opts'''へ変更する
= \opts' -> s2 (\opts'' -> s1 (\opts''' -> b ((opts''' ++ opts'') ++ opts')))
-- (++)の結合則 (opts''' ++ opts'') ++ opts' = opts''' ++ (opts'' ++ opts')
= \opts' -> s2 (\opts'' -> s1 (\opts''' -> b (opts''' ++ (opts'' ++ opts')))) -- (3-2)
-- 次に右辺を展開する。
extend s2 (extend s1 b) -- (3-1)の右辺
-- 外側のextendの展開 (1-2)
= \opts2 -> s2 (\opts1 -> (extend s1 b) (opts1 ++ opts2))
-- 残った内側のextendの展開 (1-2)
= \opts2 -> s2 (\opts1 -> (\opts4 -> s1 (\opts3 -> b (opts3 ++ opts4))) (opts1 ++ opts2))
-- (\opts4 -> *)への関数適用
= \opts2 -> s2 (\opts1 -> s1 (\opts3 -> b (opts3 ++ (opts1 ++ opts2))))
-- 束縛変数 opts2, opts1, opts3の変数名をそれぞれopts', opts'', opts'''へ変更する
= \opts' -> s2 (\opts'' -> s1 (\opts''' -> b (opts''' ++ (opts'' ++ opts')))) -- (2-2)
-- (2-2), (2-3)が等しいので、(2-1)が示された。//
まずはここまで。Iterator PatternとCommand PatternでのExerciseの解答例は別ページにて。
つづき
Iterator Patternの解答例