本ページは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の解答例に続きます。