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

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

元記事：Haskell for All: Comonads are objects

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

---

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)が言えた。//