反対圏でのstrength

この記事の文脈

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

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

ある自然変換anyone :: forall a. f a -> aを用いて、自然性・単位律・結合律をすべて満たすcostrを次式の通り作れる。
```
costr = anyone . fmap fst &&& fmap snd
```
ただし、anyoneは自然変換であるから、上式はより簡潔に
```
costr = fst . anyone &&& fmap snd
```
とも書ける。
任意の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

viercc/gist:37b66810257fce0489c7ffff05fbb873

この記事の文脈

準備

目標

証明(1)

証明(2)