Too lazy to evaluate - MaybeモナドとReaderモナドの特別な関係 (1)

概要
MaybeT m は Maybe と m の余積である
rが単射ならばcoprod r pも単射である
「rpが単射である」ことの意義

概要

Aを適当な型とします。 MaybeT (Reader A) xとReaderT A Maybe xという2つの型は、 newtypeの包みを剥がせばどちらもA -> Maybe xとなり、更にこれらは実質的に同じモナドを定義しています。

この記事ではこれらのモナド（Reader A, Maybe, MaybeT (Reader A)）に何度も言及するので、以下のように省略して書くことにしましょう。

type P   = Maybe    -- Pointed の P
type R x = A -> x   -- Reader の R
--   R   = Reader A

type RP x = A -> Maybe x
--   RP   ~ R ∘ P
--        ~ ReaderT A Maybe
--        ~ MaybeT (Reader A)

また、f ~> gという表記で自然変換∀x. f x -> g xを表すことにします。

type (~>) f g = forall x. f x -> g x

このモナドRPは以下の3つの特別な性質を持ちます。

MonadとMonad準同型からなる圏において、RとPの余積（後述; Eitherのようなもの）とみなせる対象である
- 標準入射（Eitherに対するLeftやRightのような射）となるモナド準同型liftP :: P ~> RPとliftR :: R ~> RPがある
- 任意のモナドTと2つのモナド準同型r :: R ~> Tとp :: P ~> Tが与えられたとき、普遍射（Eitherに対するeither f gのような射）となるモナド準同型coprod r p :: RP ~> Tをもつ
rが単射ならばcoprod r pも単射である
rがEquifibered自然変換ならばcoprod r pもEquifibered自然変換である
- Equifibered（nLab、日本語の訳語はわかりません）については次回の記事をお待ちください

これを使うことで、過去の記事においては力業で行った証明を、見通しよくすることができます。

`MaybeT m` は `Maybe` と `m` の余積である

RP = MaybeT (Reader A)はMaybeとReader Aの余積です。より一般に、任意のモナドmについて、MaybeT mはMaybeとmの余積になります。

モナドの余積という言葉について、明確に定義しておきます。あるモナドLMがモナドLとモナドMの余積であることを、次のように定義します。

L, MのそれぞれからLMへのモナド準同型をもつ。
```
lift1 :: L ~> LM
lift2 :: M ~> LM
```
これらの準同型は標準入射とよぶ。
任意のモナドNと、L, MそれぞれからNへのモナド準同型 tr1 :: L ~> N, tr2 :: M ~> Nが与えられたとき、以下の性質を満たす唯一のモナド準同型coprod tr1 tr2 :: LM x ~> Nが存在する。
```
coprod :: Monad n => (L ~> n) -> (M ~> n) -> (LM ~> n)
coprod tr1 tr2 . lift1 = tr1
coprod tr1 tr2 . lift2 = tr1
```

モナドLとMの余積は、存在すればいずれも同型なモナドになります¹。

MaybeT mがMaybeとmの余積であることは、先日の記事において説明した

FreeとFreeTの普遍性
MaybeがFree Proxyと同型である
MaybeT mがFreeT Proxy mと同型である

から得られます。FreeとFreeTの普遍性はそれぞれ

Freeの普遍性: Free fからモナドTへの準同型tr :: Free f x -> T xは、自然変換h :: f x -> T xと一対一に対応する
FreeTの普遍性: FreeT f mからモナドTへの準同型tr :: FreeT f m x -> T xは、準同型tr1 :: m x -> T xと自然変換h :: f x -> T xとの組(tr1, h)と一対一に対応する

でしたが、ここでFreeTの普遍性に対してFreeの普遍性を使うと

FreeTの普遍性(余積ver.): FreeT f mはmとFree fとの余積である。すなわち、FreeT f mからモナドTへの準同型tr :: FreeT f m x -> T xは、準同型tr1 :: m x -> T xと準同型tr2 :: Free f x -> T xの組(tr1, tr2)と一対一に対応する

と書くことができます。前回の記事で述べたように、モナドの同型Maybe ~ Free ProxyとMaybeT ~ FreeT Proxyがあるため、 MaybeT mはMaybeとmの余積であることがわかります。

coprodの実装も、ここで明示的に書いておきます。

coprod :: (Monad m, Monad t)
       => (∀x. m x -> t x)
       -> (∀x. Maybe x -> t x)
       -> m (Maybe x) -> t x           -- MaybeT m x ~ m (Maybe x)
coprod tr1 tr2 = join . fmap tr2 . tr1

`r`が単射ならば`coprod r p`も単射である

ふたたび、RP = MaybeT (Reader A)モナドに限った議論をします。

Tを任意のモナドとして、モナド準同型r, pが以下のように与えられているとします。

r :: R x -> T x
p :: P x -> T x

RPはR = Reader A とP = Maybeの余積でしたから、以下のモナド準同型があります。

rp :: RP x -> T x
rp = coprod r p
   = join . fmap p . r

このとき、r が単射²ならば、rp = coprod r p も単射であることがいえます。

モナド準同型p :: P x -> T xは、Tが自明なモナド（Data.Proxy）でない限り常に単射です。したがって、「rが単射ならばrpも単射」は、「r, pがともに単射ならばrpも単射」と、自明なケースを除いて同じことを言っています。

これは非常に珍しいことであり、一般の余積について言えることではありません。例えば、Haskにおける余積Eitherが持つ普遍射either :: (x -> z) -> (y -> z) -> Either x y -> zにおいては、 f,gがそれぞれ単射であってもeither f gが単射であるとは限りません。

更に、MaybeT mに限っても、任意のモナドmについて成り立つわけではありません。反例をひとつあげると、id :: Maybe x -> Maybe xは明らかに単射なモナド準同型ですが、 coprod id id :: MaybeT Maybe x -> Maybe xは単射ではありません。実際、MyabeT NothingとMaybeT (Just Nothing)は、どちらもNothingに写されます。

ほかの圏で同じことが起きる例には、「アーベル群の圏における ℤ/cℤ と ℤ/dℤ の余積(=直積) ℤ/cℤ ⊕ ℤ/dℤ でcとdが互いに素なとき」などがあります。

証明の補助のため、以下の2つの関数を定義します。

zero :: T a
zero = p Nothing

refill :: T a -> R Bool -> T (P a)
refill ta cond = join . r $ \i ->
  if cond i then fmap Just ta else pure Nothing

-- 型シノニムに注意
--   P = Maybe
--   R x = A -> x

mask :: T a -> R Bool -> T a
mask ta cond = join . fmap p $ refill ta cond

xを任意のRP a型の値としたとき、refill (rp x) condを以下のように計算することができます。

(Eq1)

refill (rp x) cond =
  rp $ \i -> if cond i then fmap Just (x i) else Just Nothing

証明

refill (rp x) cond
 = join . r $ \i ->
     if cond i then fmap @T Just (rp x) else pure @T Nothing
 = join . r $ \i ->
     if cond i then rp (fmap @RP Just x) else rp (pure @RP Nothing)
 = join . r . fmap rp $ \i ->
     if cond i then (\j -> fmap Just (x j)) else const (Just Nothing)
 = join . r . fmap rp $ \i j ->
     if cond i then fmap Just (x j) else Just Nothing
   -- 下記 (Eq1') より 
 = join . fmap p . r . join @R $ \i j ->
     if cond i then fmap Just (x j) else Just Nothing
 = rp $ \i ->
     if cond i then fmap Just (x i) else Just Nothing

-- (Eq1')
join . r . fmap rp
 = join . r . fmap (join . r . fmap p)
 = join . r . fmap join . fmap r . fmap (fmap p)
 = join . fmap join . fmap (fmap p) . r . fmap r
 = join . join . fmap (fmap p) . r . fmap r
 = join . fmap p . join . r . fmap r
 = join . fmap p . r . join @R

同様に、mask (rp x) condも計算すると以下のようになります。

(Eq2)

mask (rp x) cond = rp $ \i -> if cond i then x i else Nothing

証明

mask (rp x) cond
 = join . fmap p $ refill (rp x) cond
 = join . fmap p . join . fmap p . r $ \i ->
     if cond i then fmap Just (x i) else Just Nothing
   -- 下記(Eq2')より
 = join . fmap p . fmap (join @P) . r $ \i ->
     if cond i then fmap Just (x i) else Just Nothing
 = join . fmap p . r $ \i ->
     if cond i then join (fmap Just (x i)) else join (Just Nothing)
 = rp $ \i -> if cond i then x i else Nothing

-- (Eq2')
join . fmap p . join . fmap p
 = join . join . fmap (fmap p) . fmap p
 = join . fmap join . fmap (fmap p) . fmap p
 = join . fmap (join . fmap p . p)
 = join . fmap (p . join @P)
 = join . fmap p . fmap (join @P)

(Eq1)を用いてrefill (rp x) (isJust . x)を計算すると、次の(Eq3)を得ます。

(Eq3)

refill (rp x) (isJust . x) = r x

証明

refill (rp x) (isJust . x)
 = join . fmap p . r $ \i ->
     if isJust (x i) then fmap Just (x i) else Just Nothing
 = join . fmap p . r $ \i ->
     case x i of
       Just a -> Just (Just a)
       Nothing -> Just Nothing
 = join . fmap p . r $ \i -> Just (x i)
 = join . fmap p . r . fmap Just $ x
 = join . fmap (p . Just) . r $ x
 = r x

(Eq3)により、次のことがわかります。

(Lemma1) rpによってzeroに写るのはconst Nothingのみ: rp x = zero ⇒ x = const Nothing

証明

rp x = zeroとなるxに対して、あるi :: Aがあってx i = Just _と仮定すると、以下の自然変換f :: a -> RP aが単射になります。

f :: a -> RP a
f a = fmap (fmap (const a)) x

このとき、refill (rp (f a)) (isJust . f a) = r (f a)です。しかし、isJust . f aはaに依存しないisJust . xに等しく、仮定よりrp (f a)はaによらずzeroに等しいためこちらも定数です。したがって、左辺は定数です。これはr . fが単射であることと矛盾します。したがってx i = Just _となるようなiは存在せず、x = const Nothingです。

次に、以下の事実を示します。

(Lemma2): mask (rp x) cond = zero ⇒ (\i -> cond i && isJust x i) = const False

証明

(Eq2)より

mask (rp x) cond
 = rp (\i -> if cond i then x i else Nothing)
 = zero

です。したがって、(Lemma1)より

         (\i -> if cond i then x i else Nothing) =          const Nothing
isJust . (\i -> if cond i then x i else Nothing) = isJust . const Nothing

です。この左辺は\i -> cond i && isJust x iに、右辺はconst Falseに等しくなります。

これらを用いれば、refill . rpが単射であること、結果としてrpも単射であることを証明できます³。

refill . rpの単射性: 任意のx,y :: RP aに対して、 refill (rp x) = refill (rp y)ならばx = y

証明

maskの定義より、refill (rp x) = refill (rp y)ならばmask (rp x) = mask (rp y)です。

また、(Eq2)より

mask (rp x) (not . isJust . x)
 = rp $ \i -> if not (isJust (x i)) then x i else Nothing
 = rp $ \i -> Nothing
 = zero

です。ここで、仮定よりmask (rp x) = mask (rp y)なので、(Lemma2)より次式(*)が成り立ちます。

(\i -> not (isJust (x i)) && isJust (y i)) = const False -- (*)

xとyを入れ替えて、同様に次式(**)も成り立ちます。

(\i -> not (isJust (y i)) && isJust (x i)) = const False -- (**)

これらが両方成り立つのは、(\i -> isJust (x i) /= isJust (y i)) = const Falseのとき、すなわちisJust . x = isJust . yのときに限ります。

更に(Eq1)を用いると

   r x = refill (rp x) (isJust . x) = refill (rp y) (isJust . y) = r y

が成り立ちます。rは単射なので、x = yでなければなりません。

「`rp`が単射である」ことの意義

「rが単射ならばrp = coprod r pも単射である」ことがわかりましたが、これがどのように役立つのか説明していませんでした。役立つ一例を見てみましょう。

以下に定義するHに対してMonad Hというインスタンスを定義するならば、必ずpure a = One aでなければいけません。

data H a = Err Integer | One a | Two a a
  deriving (Functor)

instance Monad H where
    pure :: a -> H a
    join :: H (H a) -> H a

「rが単射ならばrp = coprod r pも単射である」を使えば、このことを容易に示せます。

join . pure = idが成り立たなくなるため、pure _ = Err iにはなり得ません。
pure a = F2 a aであるようなMonad Hのインスタンスがあったと仮定して、矛盾を導きます。

このとき、モナド則からjoin (Two (Two aa ab) (Two ba bb)) = Two aa bbとなります。ここでr :: (Bool -> a) -> H aとp :: Maybe a -> H aを以下のようにおくと、これらはモナド準同型になり、更にrは単射です。したがって、rp :: (Bool -> Maybe a) -> H aも単射です。
```
r f = Two (f False) (f True)
p Nothing  = Err 0
p (Just a) = pure a
```
Bool -> Maybe aは以下の4つの異なる”コンストラクタ”
```
\_ -> Nothing                                        :: Bool -> Maybe a
\a0 -> \case { False -> Just a0; True -> Nothing}    :: a -> (Bool -> Maybe a)
\a1 -> \case { False -> Nothing; True -> Just a1}    :: a -> (Bool -> Maybe a)
\a0 a1 -> \case { False -> Just a0; True -> Just a1} :: a -> a -> (Bool -> Maybe a)
```
を持ちます。rpが単射であるためには、rpはこれらをFの異なるコンストラクタに写さなければならず、更に最初の1つ以外をErr _に写すことができません。ですが、これは不可能です。

しかし、この事実（rが単射ならばrpも単射）だけでは力不足な目標もあります。実は、次のような既知の事実を一挙に証明することを目論んでいました。

リスト関手[]に対するMonadのインスタンスとして、可能なpure :: x -> [x]の選択肢はpure x = [x]のみである。
- @1to100pen 氏による証明
定数でない多項式FunctorFで、“次数”が1の項を持たず、かつ”定数項”を持つようなもの、すなわちF(x) = c + x^2 * G(x)と書けるようなものには、Monadのインスタンスが存在しない。
- このブログで以前証明しました（過去の記事）

リスト関手[]に関する事実は、前述のHについての証明をなぞれば、「n個の値をとる型Aに対してrp :: (A -> Maybe a) -> [a]が単射であることができない」といった形で証明できそうに見えます。しかし、リスト関手には「定数でない項」が無限個あるため、単射(A -> Maybe a) -> [a]が取れなくなることはありません。2つめの事実も、同様に「単射である」だけでは不十分です。

既にあるこれらの証明では、Fのあるコンストラクタの”次数”、[]の”長さ”・・・といったものが丁度 n である、という形の制約を発見し、うまく利用しています。しかし、「単射である」という事実からは、“次数”nのコンストラクタが写される先のコンストラクタの”次数”はn以上であるということしかわからず、ぴったり n であるという条件が得られません。

ここでの「“次数”nのコンストラクタが写される先のコンストラクタの”次数”がぴったりnに一致する」を厳密に述べるための概念がEquifibered自然変換というものです⁴。このブログの次回の記事でそれを説明しようと思います。

ここでの余積の定義は、一般の圏における余積をモナドとモナド準同型からなる圏に特殊化したものです。そのため、一般の圏における「余積は存在すれば同型を除いて一意」という証明がそのまま通用します。

モナドL, Mの余積として、モナドLM, LM'があったとします。それぞれ標準入射と普遍射の名前を
```
lift1 :: L ~> LM
lift2 :: M ~> LM
coprod :: Monad n => (L ~> n) -> (M ~> n) -> (LM ~> n)

lift1' :: L ~> LM'
lift2' :: M ~> LM'
coprod' :: Monad n => (L ~> n) -> (M ~> n) -> (LM' ~> n)
```
とします。このとき
```
f = coprod lift1' lift2' :: LM ~> LM'
g = coprod' lift1 lift2  :: LM' ~> LM
```
とおくと、普遍性からfとgは互いに逆であることが示せます。↩︎
fが単射である⇔「任意のx,yに対してf x = f y⇒x = y」と定義します。↩︎
一般に、f . gが単射ならばgも単射です。 ∵ g x = g y ⇒ f (g x) = f (g y) かつ f (g x) = f (g y) ⇒ x = y↩︎
正確には、「私がこの概念を厳密化したものを探し求めて本やネットを漁っていたら、最近になってようやく見つけた用語」がEquifibered自然変換です。

なので、「より適切な概念があるよ」などのご指摘がございましたら教えていただけると嬉しいです。（加えて、どんなコメントでも元より大歓迎です。メール viercc@gmail.com またはtwitter @viercc まで！）↩︎

MaybeモナドとReaderモナドの特別な関係 (1)

概要

MaybeT m は Maybe と m の余積である

rが単射ならばcoprod r pも単射である

「rpが単射である」ことの意義

`MaybeT m` は `Maybe` と `m` の余積である

`r`が単射ならば`coprod r p`も単射である

「`rp`が単射である」ことの意義