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

前回の続きです。

前回のまとめ

前回の記事と同様に、R, P, RPを以下のモナドとします。

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

前回は、モナドRP x = MaybeT (Reader A) x = A -> Maybe xが持つ特別な性質として、

• モナドTとモナド準同型r :: R ~> Tとp :: P ~> Tが与えられたとき、 rp = join . fmap p . r :: RP ~> Tもモナド準同型である
• rが単射であれば、上述のrpも単射である

ことを示しました。また、これを用いれば、一部のモナドTの性質に関する証明が簡単になることがわかりました。

一方で、

• リスト関手[]上に定義されたモナドは、必ずpure a = [a]であること（リンク）
• モナド演算を持てない多項式関手の特徴づけ（過去の記事）

といった証明に使うには、単射rpを持つだけでは不十分でした。 これらの証明は、「ある方法で構成したリストの長さが必ずnで、しかも長さnの任意のリストを構成できる」 「特定のコンストラクタがちょうどn個の引数をとる」 といった類の事実を発見することで行っていました。

こういった性質をアドホックに定式化するならば、例えば次のようなかたちを取るでしょう。

• 「ある自然変換f :: (N -> a) -> [a]は、長さがちょうど|N|のリストへの同型になっている」ことを、 「リスト関手を長さが|N|のリストとそれ以外の長さのリストに分割する自然同型split_N, unsplit_N が存在して、f = unsplit_N . Left」と表現する

  -- @unsplit_N@ は @split_N@ の逆
  split_N   :: [a] -> Either (N -> a) (ListButN a)
  unsplit_N :: Either (N -> a) (ListButN a) -> [a]

• 「関手Gは、ある自然変換f :: (N -> a) -> G aを持っており、これは『|N|引数のコンストラクタ』とみなせる」を、 リストの場合と同様に、「ある自然同型split_N, unsplit_Nがあり、f = unsplit_N . Leftであること」と表現する

  split_N   :: G a -> Either (N -> a) (G_ButN a)
  unsplit_N :: Either (N -> a) (G_ButN a) -> G a

より一般に、ある自然変換fが、関手Fを関手Gの「直和成分」にすること、すなわち以下のように定式化することが考えられます。

• 自然変換f :: F a -> G aは、GをFとG_minus_Fの和に分解するような自然同型

  split   :: G a -> Either (F a) (G_minus_F a)
  unsplit :: Either (F a) (G_minus_F a) -> G a

  を使って、f = unsplit . Leftと書ける

しかし、この定式化はいくつかの点で望ましくありません。

1. 自然変換の値域になる関手とならない関手に分けるという操作が煩雑であり、証明の見通しが良くならなかった
2. そもそも、「自然変換の値域にならない関手」が定義できないことがある。例えば、 F x = (Integer -> Integer, x)という関手においてf a = (id, a)の値域にならないもの、という関手を作るには、 Integer -> Integerからidの一点だけを除いた型が必要になるが、そのような型はない。

そのため、こうした問題を迂回できるような、よい定式化を探しました。 そこで見つけたのがequifibered自然変換です。

Equifibered自然変換

定義

Equifibered自然変換(equifibered natural transformation - nLab)とは、 関手F, G 間の自然変換 τ :: ∀a. F a -> G aであって、任意の型a, bと関数f :: a -> bに対して、以下の条件を満たすものです。

• τの自然性を表す以下の可換図式は引き戻しである

           fmap f
      F a --------> F b
       |             |
       | τ           | τ
       |             |
       v   fmap f    v
      G a --------> G b

これは、HaskellのFunctor間の自然変換に限れば、次のように言い換えることができます。

• 任意のf :: a -> b, x :: F bとy :: G aでτ x = fmap f y :: G bを満たすものがあれば、 あるv :: F aが存在してx = fmap f v かつ y = τ v を満たす。 また、この条件を満たすvは唯一つに定まる。

このx :: F bとy :: G aに対して唯一定まるv :: F aのことを、「f :: a -> bに沿って xをyに引き戻した値」と呼ぶことにします。

Equifibered自然変換の例

Equifibered自然変換の具体例を考えます。Fがただ値を2つ保持する関手、Gをリスト関手とします。

data F a = F a a
type G a = [a]

以下の自然変換okとok'はequifiberedですが、badとbad'はequifiberedではありません。

ok, ok', bad, bad' :: F a -> G a
ok (F a1 a2) = [a1, a2]
ok' (F a1 a2) = [a2, a1]

bad (F a1 a2) = [a1]
bad' (F a1 a2) = [a1, a1, a2, a2]

• x = F b1 b2 :: F bが任意に与えられているとき、y :: [a]がok x = fmap f yを満たしたとします。 fmapはリストの長さを変えないので、y = [a1, a2]でしかありえません。更に、

  ok x     = ok (F b1 b2)    = [b1, b2]     =
  fmap f y = fmap f [a1, a2] = [f a1, f a2]

  なので、f a1 = b1, f a2 = b2が成り立っています。したがって、v = F a1 a2とすれば、 fmap f v = x, ok v = yが成り立ちます。

• ok'も同様です。y = [a1, a2]のとき、ただ順序を入れ替えてv = F x2 x1とすれば、 fmap f v = x, ok v = yが成り立ちます。

• badはFに含まれている情報を捨ててしまいます。

  x = F b1 b2
  y = [a1]
  bad' x   = [b1]   =
  fmap f y = [f a1]

  すなわちf a1 = b1であることだけがわかります。v = F a1 a2のうち、 fmap f v = xすなわちf a2 = b2であるようなa2が唯一存在すればよかったのですが、 fは任意の関数であるため、f a2 = b2を満たすa2が一つもないこともあれば複数あって一意に定まらないこともあります。

  そのため、badはequifiberedではありません。

• bad'は単射自然変換ではあるので、少なくともxに関する情報を消してしまうことはありません。 yは長さ4のリストだとわかっています。しかし、

  x = F b1 b2
  y = [a1, a2, a3, a4]
  bad' x   = [b1,   b1,   b2,   b2] =
  fmap f y = [f a1, f a2, f a3, f a4]

  が成り立ちながらa1 /= a2, a3 /= a4であることは十分あり得るにもかかわらず、 bad'の値域はつねに1番目と2番目、3番目と4番目の要素が等しいため、 bad' v = yが成り立つvは存在しないことがあります。

  したがって、bad'はequifiberedではありません。

こういった例からわかるように、リストのような多項式関手の場合は、

• τ :: (N -> a) -> G aがequifibered自然変換 ⇔ Gはτの値域とそれ以外の直和に分けることができ、 値域に対してはτは同型 ¹
• τ :: F a -> G aがequifibered自然変換かつ単射 ⇔ Fはτの値域とそれ以外の直和に分けることができ、 値域に対してはτは同型

となります。

rがequifiberedならばrpもequifibered

モナドTとモナド準同型r :: R ~> Tとp :: P ~> Tが与えられたとき、 「rがequifiberedモナド準同型であればrpもそうである」ことを証明します。

証明には、前回の記事で用いた補助的な関数や等式を使います。 まず、refill, maskという関数を以下のように定義していました。

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

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

前回の記事では、これらの関数について、以下の等式を証明しました。

(Eq3)

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

maskは以下のように書くこともできます。

(Eq4)

mask y cond = join . r $ \i -> if cond i then y else zero

  mask y cond
    = join . fmap p . join . r $ \i ->
        if cond i then fmap Just y else pure Nothing
    = join . r . fmap (join . fmap p) $ \i ->
        if cond i then fmap Just y else pure Nothing
    = join . r $ \i ->
        if cond i then (join . fmap p . fmap Just) y
                  else (join . fmap p . pure) Nothing
    = join . r $ \i ->
        if cond i then (join . fmap pure) y
                  else (join . pure . p) Nothing
    = join . r $ \i -> if cond i then y else zero
    
    -- (*)
    join . fmap p . join . r
    = join . join . fmap (fmap p) . r
    = join . fmap join . fmap (fmap p) . r
    = join . r . fmap (join . fmap p)

任意のxb :: R (P b), ya :: T aに対して、rp xb = fmap f yaが成り立っているならば、 あるxa :: R (P a)が存在してrp xa = ya, fmap (fmap f) xa = xbとなること、 及びそのようなxaが唯一であることを示します。

まず、そのようなxaが存在すれば唯一であることを示します。

次の値zaを考えます。

za :: T (Maybe a)
za = refill ya (isJust . xb)

ここでfmap (fmap f) za = r xbです。

fmap (fmap f) za
= fmap (fmap f) (refill ya (isJust . xb))
  -- 自然性
= refill (fmap f ya) (isJust . xb)
  -- 仮定より fmap f ya = rp xb
= refill (rp xb) (isJust . xb)
  -- (Eq3)
= r xb

いま、任意のxa :: R (P a)について、仮にrp xa = yaかつfmap (fmap f) xa = xbが成り立っているとすると、 (Eq3)よりr xa = refill (rp xa) (isJust . xa) = refill ya (isJust . xb) = zaです。 これは、equifibered自然変換r :: R ~> T の下、 xa が fmap f :: P a -> P bに沿って xb :: T (P a) を za :: T (P a) に引き戻した値であることを意味します。 そのため、このようなxaは存在すれば唯一です。

逆に、xa :: R (P a)を、fmap f に沿って xb を za に引き戻した値とします。 すなわち、r xa = za かつ fmap (fmap f) xa = xbを満たす唯一の値だとします。 このとき、rp xa = ya が成り立ちます。すなわち、xa は f :: a -> bに沿って xb :: R (P b) を ya :: T aに引き戻した値になります。

rp xa
= join . fmap p . r $ xa
= join . fmap p $ za
= join . fmap p $ refill ya (isJust . xb)
= mask ya (isJust . xb)
  -- from (Eq4)
= join . r $ \i ->
    if isJust (xb i) then ya else zero
  -- from (**)
= join . r $ \i ->
    if isJust (xb i) then ya
                     else mask ya (not . isJust . xb)
  -- from (Eq4)
= join . r $ \i ->
    if isJust (xb i)
      then ya
      else join . r $ \j -> if (not . isJust . xb) j then ya else zero
= join . r $ \i ->
    if isJust (xb i)
      then join . r $ const ya
      else join . r $ \j -> if isJust (xb j) then zero else ya
= join . r . fmap (join . r) $ \i ->
    if isJust (xb i)
      then const ya
      else \j -> if isJust (xb j) then zero else ya
  -- from (***)
= join . r . join $ \i ->
    if isJust (xb i)
      then \_ -> ya
      else \j -> if isJust (xb j) then zero else ya
= join . r $ const ya
= ya

-- (**)
fmap f (mask ya (not . isJust . xb)
  = mask (fmap f ya) (not . isJust . xb)
  = mask (rp xb) (not . isJust . xb)
  = zero
mask ya (not . isJust . xb) = zero

-- (***)
join . r . fmap (join . r)
  = join . fmap join . r . fmap r
  = join . join . r . fmap r
  = join . r . join

Equifiberedを使ってわかること

この系として、面倒な等式変形を要した以下の2つの定理が得られます。

• 定数でない多項式FunctorFで、“次数”が1の項を持たず、かつ”定数項”を持つようなもの、 すなわちF(x) = c + x^2 * G(x)と書けるようなものには、Monadのインスタンスが存在しない。 （過去の記事）

  FのMonadのインスタンスを仮定すれば、ある有限な型N（|N| ≥ 2）が存在して equifiberedなモナド準同型r :: (N -> x) -> F xと、単射なモナド準同型p :: Maybe x -> F xをとることができる。 このときrp = coprod r p :: (N -> Maybe x) -> F xも単射かつequifiberedである。 したがって、F xはrpの値域(1 + x)^Nとそれ以外との直和F(x) = (1 + x)^N + H(x) として書かれる。しかし、F(x)は次数が1の項を持たなかったはずなので、これは矛盾である。

  すなわち、FはMonadのインスタンスを持てない。

• リスト関手[]に対するMonadのインスタンスとして、可能なpure :: x -> [x]の選択肢はpure x = [x]のみである。 （ @1to100pen 氏による証明 ） 特に、ZipListと同様にrepeat :: x -> [x]をpureとして用いるMonad []のインスタンスはない²。

  pure x = []ではありえないことはすぐにわかる。length (pure x) = N > 0とおくと、 上記と同様に、単射かつequifiberedなモナド準同型rp :: (N -> Maybe x) -> [x]を持たなければならない。 これによって、 [x] = 1 + x + x^2 + x^3 + ... は [x] = (1+x)^N + G(x)と書けなければならない。 この分解が成り立つNはN=1に限られる。