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

本ページは
[Haskell for All: Comonads are objects: Comonad則証明問題の解答例(The Builder Pattern編)][link-prev]
および
[Haskell for All: Comonads are objects: Comonad則証明問題の解答例(The Iterator Pattern編)][link-prevprev]
の続きです。


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

本ページでは、元記事内で出題されているExerciseへの解答例を示すことを目的としています。
今回はCommand PatternについてのExcerciseの解答例を示します。

[link-prev]:http://qiita.com/rikitoro@github/items/bd2139548a8f48023949
[link-prevprev]:http://qiita.com/rikitoro@github/items/ba40dae8247c71c7c34b
[link-1]:http://www.haskellforall.com/2013/02/you-could-have-invented-comonads.html

---

# The Command Pattern
元記事ではComonad則の証明以外にもExcerciseが出されていますが、ここではComonad則の証明の解答例だけを示します。

## 型の定義

```
newtype Kelvin = Kelvin { getKelvin :: Double }
```
`Kelvin`型の値と`Kelvin`型の値を(ごにょごにょして)`a`型の値として取り出す関数のタプルをthermostatと呼びます。thermostatは`(Kelvin, Kelvin -> a)`という型を持ちます。`(Kelvin, Kelvin -> a)`型の値thermostatを受け取り`b`型の値を返す`(Kelvin, Kelvin -> a) -> b`型の関数をpreviewと呼びます。また、thermostatを受け取り新たなthermostatを返す`(Kelvin, Kelvin -> a) -> (Kelvin, Kelvin -> b)`型の関数をadjustmentと呼びます。

## `extract`,`extend`の定義

Command patternでの`extract`と`extend`の定義は以下のように与えられています。

```
-- Definition of extract
extract :: (Kelvin, Kelvin -> a) -> a
extract (t, f) = f t -- (1-1)

-- Definition of extend (元記事ではExcerciseのSolutionとして与えられています)
extend :: ((Kelvin, Kelvin -> a) ->                    b)
       ->  (Kelvin, Kelvin -> a) -> (Kelvin, Kelvin -> b)
extend preview (t, f) = (t, \t' -> preview (t', f)) -- (1-2)
```
`extract`はthermostatから値を取り出すもっとも基本的なpreviewです。`extend`はpreviewをadjustmentに変換するものです。

Command Patternの場合では下記で定義される型コンストラクタ`Thermostat`と、上記で定義された`extract`と`extend`がComonadを成すようです。

```
type Thermostat a = (Kelvin, Kelvin -> a)
```

## Comonad則の証明

Exerciseに取り組んでいきます。

第1則の証明です。

**Exercise:** Prove that:

```
extend extract thermostat = thermostat -- (2-1)
```

証明:

```
-- 一般にthermostat = (t, f)と置けることに注意する。

extend extract thermostat -- (2-1)の左辺
-- thermostat = (t, f)と置く
= extend extract (t, f)
-- extendの展開 (1-2)
= (t, \t' -> extract (t', f))
-- extractの定義 (1-1)
= (t, \t' -> f t') 
-- \t' -> f t' = f
= (t, f)
-- thermostat = (t, f)と置いたので
= thermostat -- (2-1)の右辺 
```

続いて第2則の証明です。

**Exercise:** Prove that:

```
extract (extend preview thermostat) = preview thermostat -- (3-1)
```

証明:

```
-- 一般にthermostat = (t, f)と置けることに注意する。

extract (extend preview thermostat) -- (3-1)の左辺
-- thermostat = (t, f)と置く
= extract (extend preview (t, f))
-- extendの展開 (1-2)
= extract (t, \t' -> preview (t', f))
-- extractの定義 (1-1)
= (\t' -> preview (t', f)) t
-- 関数適用
= preview (t, f)
-- thermostat = (t, f)と置いたので
= preview thermostat -- (3-1)の右辺
```


最後に、第3則の証明です。

**Challenge Exercise:** Prove that:

```
p1, p2  :: (Kelvin, Kelvin -> a) -> b
th, th' :: (Kelvin, Kelvin -> a)

extend (\th' -> p2 (extend p1 th')) th = extend p2 (extend p1 th) -- (4-1)
```

証明:
(証明方針: 左辺、右辺においてそれぞれextendを展開し両者が等しいことを示す)

```
-- 一般に、th = (t, f)と置けることに注意する。

-- まずは(4-1)の左辺を計算していく。
extend (\th' -> p2 (extend p1 th')) th -- (4-1)の左辺
-- th = (t, f)と置く
= extend (\th' -> p2 (extend p1 th')) (t, f)
-- 外側のextendの展開 (1-2)
= (t, \t' -> (\th' -> p2 (extend p1 th')) (t', f))
-- 関数適用
= (t, \t' -> p2 (extend p1 (t', f)))
-- 残ったextendの展開 (1-2)
= (t, \t' -> p2 (t', \t'' -> p1 (t'', f))) -- (4-2)
 
-- 次に、(4-1)の右辺を計算していく。
extend p2 (extend p1 th) -- (4-1)の右辺
-- th = (t, f)と置く
= extend p2 (extend p1 (t, f))
-- 内側のextendの展開 (1-2)
= extend p2 (t, \t' -> p1 (t', f))
-- 外側のextendの展開 (1-2)
= (t, \t'' -> p2 (t'', \t' -> p1 (t', f)))
-- 束縛変数t'', t' の変数名をそれぞれt', t''に変更する
= (t, \t' -> p2 (t', \t'' -> p1 (t'', f))) -- (4-3)

-- (4-2)と(4-3)は等しい。よって(4-1)が言えた。//
```