反対圏でのstrength

gistfile1.md

この記事の文脈

https://twitter.com/inamiy/status/1489256068995710976

準備

この記事では、補助的な関数として以下のものを用いる。

-- Special case of Control.Arrow.&&&
(&&&) :: (a -> b) -> (a -> c) -> a -> (b, c)
(f &&& g) a = (f a, g a)
infixr 3 &&&

-- Special case of Control.Arrow.***
(***) :: (a -> a') -> (b -> b') -> (a,b) -> (a',b')
(f *** g) (a,b) = (f a, g b)
infixr 3 ***

leftUnit :: ((), a) -> a
leftUnit = snd

assoc :: ((a,b),c) -> (a,(b,c))
assoc ((a,b),c) = (a,(b,c))

unassoc :: (a,(b,c)) -> ((a,b),c)
unassoc (a,(b,c)) = ((a,b),c)

また、TupleSections言語拡張を前提とした表記を用いる。 これは、関数\b -> (a, b)を(a, )と、\a -> (a,b)を( , b)と略記できるようにする拡張である。

目標

Functor fが「モノイド積(,)に関して、反対圏でのstrengthを持つ」 ことを、次のクラスで表すことを考えてみる。

class Functor f => Costrong f where
    costr :: f (a, b) -> (a, f b)

Strengthと呼ぶためには、costrは次の3つの等式を満たさなければならない。

-- 自然性
--    （ただし、parametricityから常に満たしている）
-- 任意のf, gに対して、
costr . fmap (f *** g) = (f *** fmap g) . costr

-- 単位律
leftUnit . costr = fmap leftUnit

-- 結合律
assoc . costr . fmap unassoc = (id *** costr) . costr

この記事では、以下のことを証明したい。

1. ある自然変換anyone :: forall a. f a -> aを用いて、自然性・単位律・結合律をすべて満たすcostrを次式の通り作れる。

   costr = anyone . fmap fst &&& fmap snd

   ただし、anyoneは自然変換であるから、上式はより簡潔に

   costr = fst . anyone &&& fmap snd

   とも書ける。

2. 任意のcostrは、あるanyoneを用いて、上記(1)で定義したものに等しい。

すなわち、Costrongクラスは、以下のAnyoneクラスと全く同じものを定義している。

class Functor f => Anyone f where
    -- | このクラスは、anyoneが自然変換であること
    --   （parametricityにより自動的に満たす）
    --   以外に満たすべき等式は持たない
    anyone :: f a -> a

証明(1)

複雑に見えるが、証明の各ステップは、 anyoneの自然性とタプルを操作する(***)やsndといった関数たちの 関係だけを使って式変形をしているだけである。

自然性：

costr . fmap (f *** g)
  = (fst . anyone &&& fmap snd) . fmap (f *** g)
  = fst . anyone . fmap (f *** g) &&& fmap snd . fmap (f *** g) 
    -- anyoneの自然性
    -- fmapの結合則
  = fst . (f *** g) . anyone &&& fmap (snd . (f *** g))
    -- fst . (f *** g) = \(a,b) -> fst (f a, g b) = f . fst
    -- snd . (f *** g) = \(a,b) -> snd (f a, g b) = g . snd
  = f . fst . anyone &&& fmap (g . snd)
  = (f *** fmap g) . (fst . anyone &&& fmap snd)
  = (f *** fmap g) . costr

単位律：

leftUnit . costr
  = snd . (fst . anyone &&& fmap snd)
  = fmap (snd :: ((),b) -> b)
  = fmap leftUnit

結合律：

assoc . costr . fmap unassoc
  = assoc . (fst . anyone &&& fmap snd) . fmap unassoc
  = assoc . (fst . anyone . fmap unassoc &&& fmap snd . fmap unassoc)
  = assoc . (fst . unassoc . anyone &&& fmap (snd . unassoc))
    -- fst . unassoc = fst &&& fst . snd :: (a,(b,c)) -> (a,b)
    -- snd . unassoc = snd . snd         :: (a,(b,c)) -> c
  = assoc . ((fst &&& fst . snd) . anyone &&& fmap (snd . snd))
  = assoc . ((fst . anyone &&& fst . snd . anyone) &&& fmap (snd . snd))
    -- assoc . ((f &&& g) &&& h) = f &&& (g &&& h) 
  = fst . anyone &&& (fst . snd . anyone &&& fmap (snd . snd))

(id *** costr) . costr
  = (id *** (fst . anyone &&& fmap snd)) . (fst . anyone &&& fmap snd)
  = id . (fst . anyone) &&& (fst . anyone &&& fmap snd) . fmap snd
  = fst . anyone &&& (fst . anyone . fmap snd &&& fmap snd . fmap snd))
  = fst . anyone &&& (fst . snd . anyone &&& fmap (snd . snd))

証明(2)

自然性・単位律・結合律を満たす任意のcostrについて、以下の2つを示せば良い。

• あるanyone :: f a -> aが存在して、fst . costr = anyone . fmap fst
• snd . costr = fmap snd

前者は、以下のように自然変換anyoneをとればよい。

anyone :: f a -> a
anyone = fst . costr . fmap (, ())

これが自然変換であることは、parametricityを用いてもよいが、そうしなくてもcostrの自然性から従う。（証明略）

後者は、単位律を自然性によって変形すれば示せる。

snd . costr
    -- snd :: (x, y) -> y
    -- leftUnit :: ((), y) -> y
    -- const () *** id :: (x, y) -> ((), y)
  = leftUnit . (const () *** id) . costr
  = leftUnit . (const () *** fmap id) . costr
    -- 自然性
  = leftUnit . costr . fmap (const () *** id)
    -- 単位律
  = fmap leftUnit . fmap (const () *** id)
  = fmap (leftUnit . (const () *** id))
  = fmap snd