主張

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

例:以下のFunctorには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に対してat i xはxに依存する。

これを示すため、いま、ある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での値に依存する。これは矛盾である。よって、仮定したことの否定、任意のi :: Nに対してat i xはxに依存する

また、at iに関するさまざまな性質が、Monad則を仮定すると得られる。

join $ at i (U f) = at i (f i) … (at-U)

join $ at i (U f)
 = join . join $ U $ \j -> if i == j then return (U f) else zero
 = join $ U $ \j -> if i == j then (join . return) (U f) else join zero
   -- join . return = id   = join . fmap return
   -- join zero     = zero = join (return zero)
 = join $ U $ \j -> if i == j then (join . fmap return) (U f) else join (return zero)
 = join . fmap join $ U $ \j -> if i == j then (join . fmap return) (U f) else join (return zero)
   -- 結合則
 = join . join $ U $ \j -> if i == j then fmap return (U f) else return zero
   -- fmap return (U f) = U (return . f)
   -- return zero = U (const zero)
 = join . join $ U $ \j -> if i == j then U (return . f) else U (const zero)
 = join . join $ U $ \j -> U (\k -> if i == j then return (f k) else zero
   -- joinUU
 = join $ U $ \j -> if i == j then return (f j) else zero
   -- i == j より j を i に置換
 = join $ U $ \j -> if i == j then return (f i) else zero
 = at i (f i)

さらに、次の補助関数squash, holeを定義する。

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

hole :: forall x. N -> F x -> F x
hole i fx = join $ U $ \j -> if i == j then zero else fx

squash i (at i) = U id .. (squash-at)

squash i (at i)
 = join $ U $ \j -> if i == j then at i j else return j
 = join $ U $ \j ->
     if i == j
       then join $ U (\k -> if i == k then return j else zero)
       else join . return . return $ j
 = join . fmap join $ U $ \j ->
     if i == j
       then U (\k -> if i == k then return j else zero)
       else U (\_ -> return j)
 -- 結合則 + joinU
 = join $ U $ \j ->
     if i == j
       then if i == j then return j else zero
       else return j
 = join $ U $ \j -> return j
 = join . fmap return $ U (\j -> j)
 = U id

hole i (at i x) = zero … (hole-at)

hole i (at i x)
 = join $ U $ \j -> if i == j then zero else (at i x)
 = join $ U $ \j ->
     if i == j
       then zero
       else join $ U $ \k -> if i == k then return x else zero
   -- join . return = id
 = 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 -> U $ \k ->
     if i == j
       then zero
       else if i == k then return x else zero
   -- 結合則 + joinUU
 = join $ U $ \j ->
     if i == j
       then zero
       else if i == j then return x else zero
 = join $ U $ \j -> zero
 = join $ return zero
 = zero

いま、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となるようにできる。さらに、次の式が成り立つ。

hole i (con i x y) = zero … (hole-con)

これは、holeがxに関して自然、すなわちx型の変数の内容に依存して処理を変えることがないことから hole i (con i x y) と hole i (con i x x) = hole i (at i x) を区別できないことから、 (hole-at)を組み合わせるとわかる。

at i (con i x y) = con i x y … (at-con)

join $ at i (con i x y)
 = join . join $ U $ \j -> if i == j then return (con i x y) else zero
   -- 結合則
 = join . fmap 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
   -- (hole-con)より、
   -- join zero = zero = hole i (con i x y)
 = join $ U $ \j ->
     if i == j
       then join $ return (con i x y)
       else hole i (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 ->
     if i == j
       then return (con i x y)
       else 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
   -- 結合則 + joinUU
 = 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)

extraの特別な場合について計算する。

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)
 = join $ U $ \j -> if i == j then fmap f (at i i) else fmap f (return j)
 = join . fmap (fmap f) $ U $ \j -> if i == j then at i i else return j
   -- i == j より i と j を置換
   -- join . fmap (fmap f) = fmap f . join 
 = fmap f . join $ U $ \j -> if i == j then at i j else return j
 = fmap f $ squash i (at i)
   -- (squash-at)
 = fmap f $ U id
 = U f

extraはxに関して自然なので、任意のx, y, fに関して、あるg :: N -> xを用いてextra i x y f = U gとならなければならない。このことを用いると、次のような計算ができる。

join $ at i (extra i x y f)
 = join $ at i (U g)
   -- (at-U)
 = at i (g i)

しかし、extraの定義にもとづいて別の計算を行うと、

join $ at i (extra i x y f)
 = join . join $ U $ \j ->
     if i == j
       then extra i x y f
       else zero
   -- extraの定義, join . return = id
 = 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 . fmap join $ U $ \j -> U $ \k ->
     if i == j
       then if i == k then con i x y else return (f k)
       else zero
   -- 結合則 + joinUU
 = 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)
   -- (at-con)
 = con i x y

である。しかし、at i (g i)はx,yのうち高々一つにしか依存できないのに対し、con i x yは両方に依存する。

これは矛盾である。したがって、Monad則を満たすようにFのMonadのインスタンスを与えることはできない。

疑問点

ただちょっとわからない点があって、Nが無限であることを許したとき、x == yならばf x = f yを保証できるような(==) :: N -> N -> Boolが定義できるか？という問題がある。

この証明は、p x = Trueをみたすxがちょうど1つだけ存在するような p :: N -> Bool が一つでもあれば、(i ==)の代わりにそれを使うように書き換えるのは難しくないはずなので、このようなpが存在しないかもしれない、という問題といってもいい。

まず、|N| >= 2なる条件をHaskellで表現するなら、次の両方が成り立つことだ（と思う）。

あるinj :: Bool -> Nが存在して、任意のX :: Type, f, g :: X -> Boolに対してinj . f = inj . gならばf = g
あるsurj :: N -> Boolが存在して、任意のX :: Type, f, g :: Bool -> Xに対してf . surj = g . surjならばf = g

しかし、これを満たすにもかかわらず、(==)が定義できないような型がある。先程の条件を満たすpも無い。

newtype BitStream = BitStream (Bool, BitStream Bool)

inj :: Bool -> BitStream
inj x = BitStream (x, inj x)

surj :: BitStream -> Bool
surj (BitStream (x, _)) = x

ただ、N = BitStreamのとき、joinは全域関数にできないだろう。一般に、Nが(==)が定義できない(or 条件を満たすpが無い)ような型ならば、joinは全域関数にできないと言えるか？

2019.12.17 追記 なんか一晩寝たら解決した！

BitStreamには、次の関数searchが定義できる。searchは、ある全域関数p :: BitStream -> Boolをとり、 p bs = Trueとなるbsがあればそのようなbsを返す。さもなくば、適当なbs :: BitStreamを返す。 pが全域関数ならばsearch pも常にbottom以外の値を返す。

cons :: Bool -> BitStream -> BitStream
cons b bs = BitStream (b, bs)

search :: (BitStream -> Bool) -> BitStream
search p = let candidate = search (p . cons False)
           in if p (cons False candidate)
                then cons False candidate
                else cons True  (search (p . cons True))

forSome :: (BitStream -> Bool) -> Bool
forSome p = p (search p)

F = ReaderT BitStream Maybeは、当然にMonadである。一方、

type F x = BitStream -> Maybe x

zero :: forall x. F x
zero = const Nothing

isZero :: forall x. F x -> Bool
isZero = not . forSome (isJust . mx)

と定義すると、isZero mx = True ⇔ mx = zeroなので、F xは少なくとも一つの”定数項”と、それ以外の直和である。

isZero mx = Falseとなるようなmx :: F Xのうち、“自由度”(x^n の n)が1のものがあったとする。このとき、以下のようになるはずである。

x :: Xが存在して、x <$ mx = mx
任意のmy :: F Yについて、x <$ my = mxなら、y :: Yが存在してy <$ my = my

しかし、次のように定義されるmiを考えよう。

mi :: F BitStream
mi = join $ \bs -> Just (bs <$ mx)

x <$ mi
 = x <$ (join $ \bs -> Just (bs <$ mx))
 = join . fmap (x <$) $ \bs -> Just (bs <$ mx)
 = join $ \bs -> Just (x <$ (bs <$ mx))
 = join $ \bs -> Just (x <$ mx)
 = join $ \bs -> Just mx
 = mx

なので、i :: ByteStreamが存在して、i <$ mi = miである。

p :: ByteStream -> Bool
p = isJust . mi

を考えると、

p j = Trueとなるようなjが存在する。
p j = Trueならば、mi j = Just jである。
p j = Trueならば、mi j = (i <$ mi) j = Just iである。
p j = Trueならばi = jである。

となるが、このような性質を持つ（全域関数）pは存在しないのだった。したがって、F Xに”自由度”が1の項は存在しない。よって、F = ReaderT BitStream Maybeは

“定数項”とそれ以外との直和に書かれる
“自由度”が1の項は存在しない

ので、多項式Functorの定義として無限次数と無限個の項を許したならば、Fは(主張)の反例になる。

(主張3)の証明が改善の余地ありだったので修正

主張

証明

疑問点