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

Gabriel Bonzalez氏のブログ記事[Haskell for All: Comonads are objects][link-1]では、Comonad則の証明問題がいくつかExerciseとして出題されています。このページでは、その証明問題の解答例を示します。

---

元記事：[Haskell for All: Comonads are objects][link-1]

本ページでは、元記事内で出題されているExerciseへの解答例を示すことを目的としています。記事の内容自体についての説明はほとんどありませんが、元記事を読む際の参考にしていただければと思います。

下記記事も参考となります。
[Comonadはオブジェクト？ - Mizon Dev Diary][link-2]

[link-1]:http://www.haskellforall.com/2013/02/you-could-have-invented-comonads.html
[link-2]:http://mizondev.net/d/20130218

# 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編)][link-next]
Command Patternの解答例
- [Haskell for All: Comonads are objects: Comonad則証明問題の解答例(The Command Pattern編)][link-nextnext]


[link-next]:http://qiita.com/rikitoro@github/items/ba40dae8247c71c7c34b
[link-nextnext]:http://qiita.com/rikitoro@github/items/d9e507aca2a2dc84f56d