動機
次のFの形をしたMonadについて考えたかった。
M :: Type
E :: Type
data F a = F M (E -> a)特に、このようなMonad Fを定めるようなM, E上の代数的構造を明らかにしたかった。
例えば、Writer m a ~ (m, a)のMonadのインスタンスには
m上のモノイドが1対1に対応するし、
Reader e a ~ (e -> a)は一意な方法でMonadになるが、これには
e上の唯一の”余モノイド”(const () :: e -> (), join (,) :: e -> (e,e))が対応する。
こんな感じで、Monad Fに対応する代数は何かを考えていた。
が、何日かトライしたもののこれは相当難しい感じがするので、
まずはApplicative Fに何が対応するのかから考えてみた。
Applicative F の構造
ここから、以下の変数が唐突に出てきたら、暗に”任意のxについて…“等が挿入されていると思ってほしい。
x, y, z :: M
f :: E -> a
g :: E -> b
h :: E -> cまず、pure :: a -> F aは、次の形しかありえないことを確認しておく。
mPure :: M
pure a = F mPure (const a)また、Applicativeのインスタンスは、次のprodを与えても決まる。
prod :: F a -> F b -> F (a,b)
prod = liftA2 (,)MとEに関する関数(<>) :: M -> M -> Mとd :: M -> M -> E -> (E, E)が、
prodの実装と1対1に対応する。
prod (F x f) (F y g) = F (x <> y) ((f *** g) . d x y)
x <> y = case prod (F x id) (F y id) of
F z _ -> z
d x y = case prod (F x id) (F y id) of
F _ k -> kApplicative則を満たすためにmPure, <>, dに必要な制約を書き出せば、(mPure, <>) :: (M, M -> M -> M)がM上のモノイドを定めることがわかり、さらにdについても条件を得られる。
-- 右単位
-- 正確なHaskellではないが mPure = 1 と略記する
prod (F (x,f)) (pure b) = (,b) <$> F (x, f)
prod (F (x,f)) (pure b)
= F (x <> 1, (f *** const b) . d x 1)
= (,b) . F (x,f)
x <> 1 = x -- (M-unitR)
fst . d x 1 = id
d x 1 = id &&& dl x -- (d-unitR)
-- ここで dl :: M -> E -> E はある関数
-- 同様に左単位
1 <> x = x -- (M-unitL)
snd . d 1 x = id
d 1 x = dr x &&& id -- (d-unitL)
-- ここで dr :: M -> E -> E はある関数
-- Applicativeの結合法則
-- 結合法則:
(t `prod` u) `prod` v
= assoc $ t `prod` (u `prod` v)
(LHS)
= F (x <> y, f *** g . d x y) `prod` v
= F ((x <> y) <> z, (f *** g . d x y) *** h . d (x <> y) z)
= F ((x <> y) <> z,
first (f *** g) . second h . first (d x y) . d (x <> y) z)
= F ((x <> y) <> z,
(f *** g) *** h . first (d x y) . d (x <> y) z)
(RHS)
= ...(omit)...
= F (x <> (y <> z),
assoc . f *** (g *** h) . second (d y z) . d x (y <> z))
= F (x <> (y <> z),
(f *** g) *** h . assoc . second (d y z) . d x (y <> z))
(x <> y) <> z = x <> (y <> z) -- (M-assoc)
first (d x y) . d (x <> y) z
= assoc . second (d y z) . d x (y <> z) -- (d-assoc)(M-unitR), (M-unitL), (M-assoc)はモノイド則そのものである。
一方でdに関する法則はあまり明らかでない。
これらの法則はむしろ図に書いたほうがわかりやすい。
| |
---+--- +--*--+
d 1 x === | |
-+---+- --+-- |
| | dr x |
| | --+-- |
| | | |
============================================================
| |
---+--- +--*--+
d x 1 === | |
-+---+- | --+--
| | | dl x
| | | --+--
| | | |
============================================================
| |
-------+------- -------+-------
d (x <> y) z d x (y <> z)
-+-----------+- -+-----------+-
| | | |
---+--- | === | ---+---
d x y | | d y z
-+---+- | | -+---+-
| | | | | |具体例を調べる
Applicativeの具体例を挙げて、ここまで述べた法則が満たされていることを確認していく。
もっとも単純には、Compose (Writer M) (Reader E)と同じ
Applicativeのインスタンスが考えられる。これは、
d _ _ = \i -> (i,i)とした場合に相当する。この定義においてdに関する各法則が成り立つことを確認するのは、
式(d-unitL),etc. を使っても簡単だが、
d _ _ が「入力をただコピーする」ことを図で表した
| |
---+--- |
d _ _ === +-*-+
-+---+- | |
| | | |を上の3図式に当てはめれば、法則が成り立っていることは自明である。
また、M = E -> E であるとき、
自然同型 F x ~ (E -> E, E -> x) ~ E -> (E, x) ~ State E x
が得られるが、State EはMonadであり、もちろんApplicativeでもあるので、
F xがApplicativeとして得られたことになる。このとき、dは
d x _ = \i -> (i, x i)である。このとき、M上のモノイド演算としては、mempty = idおよび
x <> y = x >>> y = y . xが使われている。
モノイド作用によるApplicative
State Eと同型になるケースとの中間例として、
MがE上にモノイド作用を持つ場合というものを考えることができる。
モノイドMのE上への(右)モノイド作用(◁) :: E -> M -> Eは
i ◁ 1 = i
(i ◁ x) ◁ y = i ◁ (x <> y)を満たす関数である。モノイド作用◁を用いて、
d x _ = \i -> (i, i ◁ x)と書ける場合、これはApplicative則を満たす。上記の定義を図に書くと、
| |
| +--*---+
---+--- | |
d x y === | ----+---
-+---+- | (◁ x)
| | | ----+---
| | | |となる。法則を表す3図式に当てはめれば、
| | |
| +--*---+ +--*--+
---+--- | | | |
d 1 x === | ----+--- === --+-- |
-+---+- | (◁ 1) dr x |
| | | ----+--- --+-- |
| | | | | |
(モノイド作用であるから(◁ 1)=idであり、dr x = idとおけばよい。)
============================================================
| | |
| +--*---+ +--*--+
---+--- | | | |
d x 1 === | ----+--- === | --+--
-+---+- | (◁ x) | dl x
| | | ----+--- | --+--
| | | | | |
(dl x = (◁ x) とおけばよい)
============================================================
| |
-------+------- -------+-------
d (x <> y) z d x (y <> z)
-+-----------+- -+-----------+-
| | | |
---+--- | === | ---+---
d x y | | d y z
-+---+- | | -+---+-
| | | | | |
|| ||
| |
+----*-----+ +--*--+
| | | |
| ------+------ | ---+---
| (◁ (x <> y)) | (◁ x)
| ------+------ | ---+---
+--*--+ | | |
| | | | +-*---+
| ---+--- | | | |
| (◁ x) | | | ---+---
| ---+--- | | | (◁ y)
| | | | | ---+---
| | | | | |
(モノイド作用の結合法則から両辺は等しい)今考えたものは右モノイド作用であるが、左モノイド作用を考えることもできて、
左モノイド作用 (▷) :: M -> E -> E は次式を満たす。
1 ▷ i = i
x ▷ (y ▷ i) = (x <> y) ▷ iこれを用いて、
d _ y = \i -> (y ▷ i, i)と書ける場合もApplicative則を満たす。右作用と同じように図を描くことでこれも確認できる。
さて、右モノイド作用と左モノイド作用の両方が定義されているとき、次のdを考える。
d x y = \i -> (y ▷ i, i ◁ x)これは各法則を満たすだろうか？図を書いていくと（AAめっちゃ面倒だったので省略）
(z ▷ i) ◁ x = z ▷ (i ◁ x)が任意のz,x :: M, i :: Eに対して成り立っているとき、そのときに限り成り立つことがわかる。
これは左右のモノイド作用が可換であることを言っている。
加群の例に倣うなら”E上の(M,M)-両側モノイド作用”とでも呼べばいいだろうか。
具体例を出してみよう。M = E = Intとし、MのモノイドはIntの加法とする。
x ▷ y = x ◁ y = x + yとすれば、これは左右のモノイド作用を定めており、さらに互いに可換である。
d x y = \i -> (i + y, i + x)を用いてApplicativeの定義式まで展開してみると、
newtype F x = F (Int, Int -> x)
instance Applicative F where
pure x = F (0, const x)
F (x, f) <*> F (y, g) = F (x + y, \i -> f (i + y) (g (i + x)))である。こんなApplicativeは見たことさえないし、何かの役に立つのかまったくわからないが、 ともかく両側モノイド作用を使って、新しいApplicativeを量産する方法を手に入れたことになる。
一般論に戻って
しかし、本来の疑問はすべてのApplicativeのインスタンスと対応する代数はなにかということだった。 両側モノイド作用によるApplicative以外にもそのような例があるだろうか？
まだ次の疑問が解決していない。
- 関手
F x ~ (M, E -> x)に対するすべての可能なApplicativeのインスタンスは、両側モノイド作用によるものか？
多分違うと思うけれども、反例が思いつかない・・・
また、違うなら違うで、もともとの疑問である
- 関手
F x ~ (M, E -> x)に対するすべての可能なApplicativeのインスタンスは、M, Eに関するどんな代数と対応させられるか？
も考える必要がある。