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

元記事：Haskell for All: Comonads are objects

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

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編)