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の解答例

Haskell for All: Comonads are objects: Comonad則証明問題の解答例(The Iterator Pattern編)
Command Patternの解答例
Haskell for All: Comonads are objects: Comonad則証明問題の解答例(The Command Pattern編)