概要

広い範囲の多項式Functorについて、Monadになれるかどうかがわかった。

準備

ここでは、多項式Functorを、次の形をしたFunctor F のことと定義します。

F(x) ~ x^(a_0) + x^(a_1) + x^(a_2) + ... + x^(a_k)

ただし、~はxについて自然な同型、+は直和型、x^aはxのa個の直積とします。また、項の数kは0以上、すなわちF(x)はVoidでもよいとします。また、a_iも0でもよいとします。 x^0はUnit型、ただ1つの値のみを持つ型です。

Remark.
- 有限個の値をとる型eに対して、F(x) = Either e x, G(x) = (e,x), H(x) = e -> xはすべて多項式Functorです。
- 同じくConst eも多項式Functorです。
- 多項式FunctorF, Gについて、(F :+: G)(x) = F x + G x, (F :*: G)(x) = F x * G xは多項式Functorです。
- 多項式Functorの合成は多項式Functorです。
- 多項式FunctorFは常にTraversableにできます。

よく知っているMonadのほとんどが多項式Functorです。ただし、ここではeを有限な型とします。

Identity Functor newtype Id x = Id x
Either e
(,) e = Writer e
(->) e = Reader e
Maybe = Either ()
Proxy = Const ()

多項式Functorでないものももちろんあります。例えばCont rがそうです。

また、すでにあるMonadのインスタンスから、新たなインスタンスを次々構成する方法が多数あります。各種Monad Transformerなどはおなじみかと思いますが、それ以外にも次のようなものがあります：

Monadの積。Data.Functor.Productという名前でbaseにもあるので、Monad則の証明は省きます。
```
newtype (*) f g a = f a :*: g a
instance (Monad f, Monad g) => Monad (f * g)
```

単位の付加。モナドMに対してT(x) = x + M(x)もモナドにできます。

data T m x = TPure x | TLift (m x)

lower :: (Monad m) => T m x -> m x
lower (TPure x)  = return x
lower (TLift mx) = mx

instance (Monad m) => Monad (T m) where
  return = TPure
  TPure a  >>= k = k a
  TLift ma >>= k = TLift $ ma >>= lower . k

単位則は簡単なので省き、結合則のみ示します。

-- 次の補題をまず示す。
--   lower ma >>= lower . k  =  lower (ma >>= k)
lower (TPure a) >>= lower . k
  = return a >>= lower . k
  = lower (k a)
  = lower (TPure a >>= k)
lower (TLift ma) >>= lower . k
  = ma >>= lower . k
  = lower (TLift $ ma >>= lower . k)
  = lower (TLift ma >>= k)

(TPure a >>= f) >>= g
  = f a >>= g
  = TPure a >>= (f >=> g)

(TLift ma >>= f) >>= g
  = (TLift $ ma >>= lower . f) >>= g
  = TLift $ (ma >>= lower . f) >>= lower . g
    -- `Monad m`のMonad則によって変形できる
  = TLift $ ma >>= \a -> lower (f a) >>= lower . g
    -- 補題を使う
  = TLift $ ma >>= \a -> lower (f a >>= g)
  = TLift $ ma >>= lower . (\a -> f a >>= g)
  = TLift ma >>= \a -> (f a >>= g)

本論

ある多項式Functor Fに対して、FのMonadのインスタンスが定義できるだろうか？という問題を考えます。まず、これが常に可能であるわけではありません。例えば、F ~ Const eはeが2つ以上の異なる値を持つときにMonadになりません。加えて、先日の記事では以下の事実を示しました。

F ~ Maybe (e -> x) は、eが2つ以上の異なる値を持つときにMonadにならない

一方で、非常に広い範囲の多項式Functorに対してMonadのインスタンスが定義できることもわかっています。これらを組み合わせて、任意の多項式Functorに対してMonadのインスタンスが定義できるかどうかを判定する方法を示します。

主張0: ある多項式FunctorFが F(x) ~ c と書けるならば、|c| = 1のとき、またそのときに限りFのMonadのインスタンスが存在する。
主張1: ある多項式FunctorFが F(x) ~ x * G(x) と書けるならば、FのMonadのインスタンスが存在する。
主張2: ある多項式FunctorFが F(x) ~ 1 + x + G(x) と書けるならば、FのMonadのインスタンスが存在する。
主張3: ある多項式FunctorFが F(x) ~ c + x^2 * G(x)(|c| >= 1, G(x) ~/~ 0)と書けるならば、FのMonadのインスタンスが存在しない。
結論: F(x) ~ c + x * b + x^2 * A(x) に対してMonadのインスタンスが存在する ⇔ 以下のいずれかが成り立つ
- c = 1, b = 0, A(x) ~ 0
- c = 0, b = 0, A(x) ~/~ 0
- b >= 1

主張0 ~ 主張3から結論が出ることは簡単に確かめられます。

主張0

ある多項式FunctorFが F(x) ~ c と書けるならば、|c| = 1のとき、またそのときに限りFのMonadのインスタンスが存在する。

証明

（以下、証明部分は常体で書きます）

(⇒)はProxyと同じようにMonadのインスタンスが定義できることからわかる。

(⇐)を示す。pure :: x -> F x はある定数関数 const c0 である。このとき、c0 :: F x ~ c である。任意のc1 :: F x ~ cについて、join (pure c1) = join (const c0 c1) = join c0となるが、Monad則よりjoin . pure = idなのでjoin (pure c1) = c1でもある。したがって、任意のc型の値はjoin c0に等しい。これはすなわち、|c| = 1を意味する。

主張1

ある多項式FunctorFが F(x) ~ x * G(x) と書けるならば、FのMonadのインスタンスが存在する。

例をあげると、

F(x) ~ x + x^3
F(x) ~ x^2 + x^5 + x^6

のように、「定数項」のないFunctorはMonadにできます。

証明

F(x)の項の数kおよび多項式の次数に関する帰納法を用いる。k=1のとき、すなわちF(x) = x^aのとき、FのMonadのインスタンスがあるのは明らか。

k>1, かつ G(x) ~ x * H(x)と書けるならば、G(x)の次数はF(x)より小さいので、帰納法の仮定を用いれば G(x) はMonadにできる。F(x) ~ x * G(x) ~ (Id * G)(x)かつIdもGもMonadなので、Monadの積によってF(x)もMonadのインスタンスを持てる。
k>1, かつG(x) ~ x * H(x)と書けないならば、G(x) ~ 1 + H(x)と書ける。このとき、
```
F(x) ~ x * (1 + H(x)) ~ x + x * H(x) ~ x + (Id * H)(x)
```
かつ、(Id * H)(x)の項の数はF(x)より一つ少ないので、帰納法の仮定を用いれば(Id * H)(x)はMonadにできる。よって、先程述べた”単位の付加”の構成により、F(x) ~ x + (Id * H)(x)はMonadにできる。

主張2

ある多項式FunctorFが F(x) ~ 1 + x + G(x) と書けるならば、FのMonadのインスタンスが存在する。

例:

F(x) ~ c + b * x, 言い換えれば F x = Either C (B, x)であるとき、c >= 1, b >= 1ならばMonadのインスタンスが存在します。F x ~ WriterT B (Either C) x、および任意の空でない型Bに対してMonoid Bが定義できることを考えれば、これは納得がいきます。
F(x) ~ 1 + x + x^2 + x^3, 長さが 0 〜 3 のリストにはMonadのインスタンスが存在します。

証明

どの多項式FunctorもTraversableにできるのであった。G(x)もTraversableであると仮定してよい。次のように F x ~ U g x = 1 + x + g x とそのMonadのインスタンスを定義する。

data U g x = Nothing' | Just' x | Wrap (g x)

toMaybe :: U g x -> Maybe x
toMaybe (Just' x) = Just x
toMaybe _         = Nothing

instance (Traversable g) => Monad (U g x) where
  return = Just'
  Nothing' >>= _ = Nothing'
  Just' a  >>= k = k a
  Wrap ga  >>= k = maybe Nothing' Wrap $ traverse (toMaybe . k) ga

これがMonad則を満たすことを確認する。

[toMaybeはMonad morphism]
toMaybe . return = toMaybe . Just' = Just = return

toMaybe (ma >>= k)
 = case ma of
     Nothing' -> toMaybe (Nothing' >>= k)
     Just' a  -> toMaybe (Just' a >>= k)
     Wrap ga  -> toMaybe (Wrap ga >>= k)
 = case ma of
     Nothing' -> toMaybe Nothing'
     Just' a  -> toMaybe (k a)
     Wrap ga  -> toMaybe (maybe Nothing' Wrap $ ...)
 = case ma of
     Nothing' -> Nothing
     Just' a  -> toMaybe (k a)
     Wrap _   -> Nothing
 = case toMaybe ma of
     Nothing -> Nothing
     Just a  -> toMaybe (k a)
 = toMaybe ma >>= toMaybe . k
(系) toMaybe (f >=> g) = toMaybe f >=> toMaybe g

[左単位] return a >>= k = k a
return a >>= k
 = Just' a >>= k
 = k a

[右単位] ma >>= return = ma
Nothing' >>= return = Nothing'
Just' a  >>= return = Just' a
Wrap ga  >>= return
 = maybe Nothing' Wrap $ traverse (toMaybe . return) ga
 = maybe Nothing' Wrap $ traverse Just ga
    -- traverse則, traverse pure = pure および pure @Maybe = Just
 = maybe Nothing' Wrap $ Just ga
 = Wrap ga

[結合] (ma >>= f) >>= g = ma >>= (f >=> g)
(Nothing' >>= f) >>= g   =   Nothing'    =   Nothing' >>= (f >=> g)
(Just' a  >>= f) >>= g   =   f a >>= g   =   Just' a  >>= (f >=> g)

(Wrap ga >>= f) >>= g
 = (maybe Nothing' Wrap $ traverse (toMaybe . f) ga) >>= g
 = case traverse (toMaybe . f) ga of
     Nothing -> Nothing' >>= g
     Just gb -> Wrap gb >>= g
 = case traverse (toMaybe . f) ga of
     Nothing -> Nothing'
     Just gb -> maybe Nothing' Wrap $ traverse (toMaybe . g) gb
 = maybe Nothing' Wrap $ case traverse (toMaybe . f) ga of
     Nothing -> Nothing
     Just gb -> traverse (toMaybe . g) gb
 = maybe Nothing' Wrap $ traverse (toMaybe . f) ga >>= traverse (toMaybe . g)
Wrap ga >>= (f >=> g)
 = maybe Nothing' Wrap $ traverse (toMaybe . (f >=> g)) ga
    -- toMaybe が Monad morphismであることを用いる
 = maybe Nothing' Wrap $ traverse (toMaybe . f >=> toMaybe . g) ga
    -- Maybeでtraverse補題(後述)を用いる
 = maybe Nothing' Wrap $ (traverse (toMaybe . f) >=> traverse (toMaybe . g)) ga
 = maybe Nothing' Wrap $ traverse (toMaybe . f) ga >>= traverse (toMaybe . g)

[Maybeでtraverse補題]
任意の
    f :: a -> Maybe b
    g :: b -> Maybe c
に対して、
    traverse (f >=> g) = traverse f >=> traverse g
(証明)
    join' :: forall x. Compose Maybe Maybe x -> Maybe x
    join' (Compose mmx) = join mmx
を用いると、
    f >=> g = join' . Compose . fmap g . f
と変形できる。
また、証明は略するが join' はApplicative transformation である。
    join' . pure = pure
    join' (x <*> y) = join' x <*> join' y
よって、
    traverse (f >=> g)
      = traverse (join' . Compose . fmap g . f)
        -- Traversable則 naturality
      = join' . traverse (Compose . fmap g . f)
        -- Traversable則 composition
      = join' . Compose . fmap (traverse g) . traverse f
        -- join' の定義
      = join . fmap (traverse g) . traverse f
        -- (>=>) の定義
      = traverse f >=> traverse g
(証明終)
(注:一般のMonadに対してjoin'はApplicative transformationにならないので、
Maybeを任意のMonadに置き換えることはできない。)

主張3

2019.12.16 追記 ― 証明を読みやすく、あと有限性に依存しないようにできたので修正版を投稿しました

ある多項式FunctorFが F(x) ~ c + x^2 * G(x)(|c| >= 1, G(x) ~/~ 0)と書けるならば、FのMonadのインスタンスは存在しない。

例:

F(x) ~ 1 + x^2
F(x) ~ 3 + x^2 + x^4

証明

まず、どんな多項式Functorに対しても、forall x. x -> F xという型を持つ関数があれば、それはF(x)の特定の項 F(x) ~ ... + x^n + ...に対応するコンストラクタに、n個のxのコピーを渡した値を返す。このコンストラクタは、当然、xに依存せずに決まる。

いま問題としているF(x) ~ c + x^2 * G(x)において、Monadの定義におけるreturn :: forall x. x -> F xに対応する項がx^nであるとしたら、n == 0であるか、またはn >= 2である。

仮にn == 0であったとする。これはすなわちreturnは定数関数であり、return xの値はxに依存しないことを意味している。しかし、Monad則よりjoin (return fx) = fxでなければならず、また空でない型Xにおいてfx :: F Xは2つ以上の異なる値を持つので、returnは定数関数であってはならない。したがって、n >= 2でなければならない。

returnの返り値に対応する項x^nを明示して、F(x)が以下のように定義されているとする。

type N = ...
type C = ...
type G x = ...

data F x = U (N -> x) | L C | R x x (G x)

return :: forall x. x -> F x
return x = U (const x)

また、前提条件として与えられている、Cに1つ以上の値があることが、次のように表されているとする。

-- |C| >= 1
c0 :: C
zero :: forall x. F x
zero = L c0

簡単にわかることとして、join zero = zeroがある。

join (L c0)
 -- fmap f (L c) = L c
 = join (fmap return $ L c0)
 = join . fmap return $ L c0
 -- join . fmap return = id
 = L c0

Monad則から、join :: F (F x) -> F xの満たすべき等式として次のものが得られる。

-- ∀a :: N -> N -> x
join $ U (\i -> U (\j -> a i j)) = U $ \i -> a i i

以降、この等式はjoinUUという名前で呼ぶ。また、これは次のように証明できる。

coord :: F (F (N, N))
coord = U $ \i -> U $ \j -> (i,j)

fmap fst (join coord)
 = join (fmap (fmap fst) coord)
 = join (U $ \i -> U $ \j -> i)
 = join (U $ \i -> return i)
 = join (fmap return (U $ \i -> i))
   -- Monad則(join . fmap return = id)
 = U $ \i -> i

fmap snd (join coord)
 = join (fmap (fmap snd) coord)
 = join (U $ \i -> U $ \j -> j)
 = join (return $ U $ \j -> j)
   -- Monad則(join . return = id)
 = U $ \j -> j

join coord = U $ \i -> (i,i)

join $ U (\i -> U (\j -> a i j))
 = join $ fmap (fmap (uncurry a)) coord
 = fmap (uncurry a) $ join coord
 = fmap (uncurry a) $ U $ \i -> (i,i)
 = U $ \i -> a i i

ここで、次の関数を考える。

at :: forall x. N -> x -> F x
at i x = join $ U (\j -> if i == j then return x else zero)

いま、あるi :: Nにおいてat i xがxに依存しないと仮定する。このとき、次のsweep fはf iの値に依存しないはずである。

sweep :: forall x. (N -> x) -> F (F x)
sweep f = U $ \j -> at j (f j)

一方、join $ sweep fをjoinの結合則を用いて計算すると、以下のようになる。

join $ sweep f
 = join $ U (\j -> at j (f j))
 = join $ U (\j -> join $ U (\k -> if j == k then return (f j) else zero))
 = join . fmap join $ U (\j -> U (\k -> if j == k then return (f j) else zero))
 -- 結合則
 = join . join $ U (\j -> U (\k -> if j == k then return (f j) else zero))
 -- joinUU
 = join $ U (\j -> if j == j then return (f j) else zero)
 = join $ U (\j -> return (f j))
 = join . fmap return $ U (\j -> f j)
 -- 単位則
 = U f

これは明らかにfの任意の点i :: Nでの値に依存する。これは矛盾である。

事実1: 任意のiに対してat i xはxに依存する。

次に、at i /= returnを示す。

U f >>= return
 = U f
U f >>= at i
 = join $ U (\j -> at i (f j))
 = join $ U (\j -> join $ U (\k -> if i == k then return (f j) else zero))
 = join . fmap join $ U (\j -> U (\k -> if i == k then return (f j) else zero))
 = join . join $ U (\j -> U (\k -> if i == k then return (f j) else zero))
 = join $ U (\j -> if i == j then return (f j) else zero)
 = join $ U (\j -> if i == j then return (f i) else zero)
 = at i (f i)

いま、Nには2つ以上の異なる値があるので、i' /= iなるi' :: Nが存在して、U fはf iにもf i'にも依存する。しかし、at i (f i)はf iにしか依存しないので、at i = return ではありえない。

事実2: 任意のiに対してat i /= return

加えて、

hole :: (N -> x) -> N -> (x -> F x) -> F x
hole f i u = join $ \j -> if i == j then u (f j) else return (f j)

hole f i (at k)
 = join $ U $ \j -> if i == j then at k (f j) else return (f j)
 = join $ U $ \j -> if i == j
     then join $ U (\l -> if k == l then return (f j) else zero)
     else join . return . return $ f j
 = join . fmap join $ U $ \j -> if i == j
     then U (\l -> if k == l then return (f j) else zero)
     else U (\_ -> return (f j))
 -- 結合則 + joinUU
 = join $ U $ \j ->
     if i == j
       then if k == j then return (f j) else zero
       else return (f j)

-- i == k のとき
hole f i (at k) | i == k
 = join $ U $ \j -> if (i == j) then return (f j) else return (f j)
 = join $ U $ \j -> return (f j)
 = U f

-- i /= k のとき
hole f i (at k) | i /= k
 = join $ U $ \j ->
     if i == j then zero else return (f j)

より、hole f i (at k)がf iに依存するかどうかは、i == kかどうかによって決まる。したがって、i /= kのとき、at i /= at kである。

事実3: 任意のi, k :: Nに対して、i /= kならばat i /= at k

いま、at i xはxに依存するのであった。returnのときと同様の議論によって、at i xが返すコンストラクタは2つ以上のxの値に依存することができるので、関数con :: N -> x -> x -> F xが存在して、con i x yはxとyの両方に依存し、 con i x x = at i xとなるようにできる。

con iに関する等式をいくつか示す。

join $ U (\j -> if i == j then zero else at i x)
 = join $ U (\j -> if i == j then join (return zero) else join $ U (\k -> if i == k then return x else zero))
 = join . fmap join $ U $ \j ->
     if i == j then return zero else U (\k -> if i == k then return x else zero)
 = join . join $ U $ \j -> U $ \k ->
     if i == j then zero else (if i == k then return x else zero)
 = join $ U $ \j ->
     if i == j then zero else (if i == j then return x else zero)
 = join $ U $ \j -> if i == j then zero else zero
 = join $ return zero
 = zero

-- Because `join` can't discriminate between `at i x = con i x x` and `con i x y`:
join $ U (\j -> if i == j then zero else con i x y)
 = zero

join $ at i (con i x y)
 = join . join $ U (\j -> if i == j then return (con i x y) else zero)
 = join $ U (\j -> if i == j then join (return (con i x y)) else join zero)
 = join $ U (\j -> if i == j then con i x y else zero)
  -- Use above equation in reversed direction
 = join $ U $ \j ->
     if i == j
       then con i x y
       else join $ U (\k -> if i == k then zero else con i x y)
 = join $ U $ \j ->
     if i == j
       then join $ return (con i x y)
       else join $ U (\k -> if i == k then zero else con i x y)
 = join . fmap join $ U $ \j -> U $ \k ->
     if i == j
       then con i x y
       else (if i == k then zero else con i x y)
 = join $ U $ \j ->
     if i == j
       then con i x y
       else (if i == j then zero else con i x y)
 = join $ U $ \j -> con i x y
 = join . return $ con i x y
 = con i x y

いま、次の関数extraを考える。

extra :: forall x. N -> x -> x -> (N -> x) -> F x
extra i x y f = join $ U (\j -> if i == j then con i x y else return (f j))

次の計算によって、2つのことがわかる。

extra i (f i) (f i) f
 = join $ U (\j -> if i == j then con i (f i) (f i) else return (f j))
 = join $ U (\j -> if i == j then at i (f i) else return (f j))
 = hole f i (at i)
 = U f

まず、extraはxに関して自然なので、任意のx, y, fに関してextra i x y f = U _とならなければならない。また、extra i x y fは任意のj /= iにおけるf jと、x, yのいずれか片方に依存する。

さらに、

join $ at i (extra i x y f)
 = join . join $ U $ \j -> if i == j then extra i x y f else zero
 = join . join $ U $ \j ->
     if i == j
       then join $ U (\k -> if i == k then con i x y else return (f k))
       else join (return zero)
 = join . join . fmap join $ U $ \j ->
     if i == j
       then U (\k -> if i == k then con i x y else return (f k))
       else return zero
 = join . join . join $ U $ \j -> U $ \k ->
     if i == j
       then if i == k then con i x y else return (f k)
       else zero
 = join . join $ U $ \j ->
     if i == j
       then if i == j then con i x y else return (f j)
       else zero
 = join . join $ U $ \j -> if i == j then con i x y else zero
 = join $ at i (con i x y)
 = con i x y

である。したがって、extra i x y fはxとyの両方に依存する。

さて、extra i x y f = U gと書くことができ、g :: N -> xなのであった。gは任意のj /= iにおけるf j、x、そしてyのいずれにも依存する。しかし、Nが有限であればこれはN+1個の独立な変数なので、これは不可能である。

事実4: Nは無限個の異なる値をとる。

さらに、at iは各iについて異なる必要があるので、

事実5: F(x)は無限個の項の和である。

いま、多項式Functorは、有限な型a_iについてx^(a_i)の有限個の直和型として定義したのであった。よって、ここで定義したF(x)はMonadになることはない。

モナドを見分けるコツ

概要

準備

本論

主張0

証明

主張1

証明

主張2

証明

主張3

証明