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

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

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

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

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

---

# The Iterator Pattern
## 型の定義

```
data Iterator a = a :< (Iterator a)

infixr 5 :<
```
`Iterator a`型の値 iterator は`a`型の値からなる無限リストですね。iterator から値を取り出すような`Iterator a -> a`型の関数をretrieval、iterator から新たな iterator を生成する`Iterator a -> Iterator a`型の関数を shift と呼んでいます。

## extract,extendの定義

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

```
-- Definition of extract
extract :: Iterator a -> a
extract (cmd :< _) = cmd -- (1-1)

-- Definition of extend (元記事ではExcerciseのSolutionとして与えられています)
extend :: (Iterator a ->          a)
       ->  Iterator a -> Iterator a
extend f iter@(_ :< as) = (f iter) :< (extend f as) -- (1-2)
```
extractはiteratorの先頭要素を取ってくる、もっとも基本的なretrievalです。extendはretrievalをshiftに変換するものです。

Iterator Patternの場合では上記で定義された<`Iterator`, `extract`, `extend`>がComonadとなるようです。

## Comonad則の証明

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

第1則

```
extend extract iterator = iterator
```

は、元記事内で証明されていますので省略します。


第2則の証明問題です。
**Exercise:** Prove that:

```
extract (extend retrieval iterator) = retrieval iterator -- (2-1)
```

証明:

```
extract (extend retrieval iterator) -- (2-1)の左辺
-- iterator = a :< asと書く 
= extract (extend retrieval iterator@(_ :< as))
-- extendの展開 (1-2)
= extract ((retrieval iterator) :< (extend retrieval as))
-- extractの定義 (1-1)
= retrieval iterator -- (2-1)の右辺 //
```

最後に第3則の証明問題です。
**Challenge Exercise:** Prove that:

```
r1, r2 :: Iterator a -> a -- retrievals
i,  i' :: Iterator a      -- iterators

extend (\i' -> r2 (extend r1 i')) i = extend r2 (extend r1 i) -- (3-1)
```

証明:
(証明方針:左辺と右辺をそれぞれ展開していき、それぞれが同じ形の方程式を構成することを示す)

```
-- 以下のように lhs と rhs を定義する。
lhs :: Iterator a -> Iterator a
lhs = extend (\i' -> r2 (extend r1 i')) -- (3-2)

rhs :: Iterator a -> Iterator a
rhs = \i' -> extend r2 (extend r1 i') -- (3-3)
-- この時(3-1)の左辺と右辺はそれぞれ lhs i、rhs iと与えられる。
-- したがって lhs = rhsが証明できれば良い。

-- i = a :< as としてlhs iを計算する。
lhs i@(a :< as) 
-- lhsの定義 (3-2)
= extend (\i' -> r2 (extend r1 i')) i@(a :< as)
-- extendの展開 (1-2)
= ((\i' -> r2 (extend r1 i')) i) :< (extend (\i' -> r2 (extend r1 i')) as)
-- 前者の(\i' -> *) の関数適用
= (r2 (extend r1 i)) :< (extend (\i' -> r2 (extend r1 i')) as)
-- lhsの定義を逆に使う (3-2)
= (r2 (extend r1 i)) :< (lhs as)

-- まとめるとlhsについての以下の方程式が得られる。
lhs i@(a :< as) = (r2 (extend r1 i)) :< (lhs as) -- (3-4)


-- i = a :< as として今度はrhs iを計算する。
rhs i@(a :< as)
-- rhsの定義 (3-3)
= (\i' -> extend r2 (extend r1 i')) i@(a :< as)
-- (\i' -> *)の関数適用
= extend r2 (extend r1 i@(a :< as))
-- 内側のextendの展開 (extend r1 i = (r1 i) :< (extend r1 as)) (1-2)
= extend r2 ((r1 i) :< (extend r1 as))
-- 残ったextendの展開 (1-2)
= (r2 ((r1 i) :< (extend r1 as))) :< (extend r2 (extend r1 as))
-- extend r1 i = (r1 i) :< (extend r1 as)だったことを利用
= (r2 (extend r1 i)) :< (extend r2 (extend r1 as))
-- 右側をラムダで書き直す
= (r2 (extend r1 i)) :< ((\i' -> extend r1 (extend r1 i')) as)
-- rhsの定義 (3-3)
= (r2 (extend r1 i)) :< (rhs as)

-- まとめるとrhsについての以下の方程式が得られる。
rhs i@(a :< as) = (r2 (extend r1 i)) :< (rhs as) -- (3-5)


-- (3-4), (3-5)をみると、i@(a :< as)およびr1、r2が与えられたとき、
-- lhs、rhsがともに下式に示すsについての同じ形の方程式を満たしていることがわかる。
s i = (r2 (extend r1 i)) :< (s as) 

-- したがって、lhs = rhsが示された。これより(3-1)が言える。
-- (本当は解の一意性を示す必要がありそう・・・) //
```

# つづき

Commonad Patternの解答例に続きます。
- [Haskell for All: Comonads are objects: Comonad則証明問題の解答例(The Command Pattern編)][link-next]

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