多項式Applicative Functorの一般論（補遺）

目次

書いていたら年が明けました。

前回の記事の補足など。

群っぽい多項式Functor

前回の記事のまとめ部分で次のようなことを書きました。

まとめると、モノイドAp F ()が群Gになるような多項式 Applicative F は、

  • Functorとして(G, E -> a) に自然同型
  • どれも曖昧なく以下のデータで表現できる
    • tr, tr' :: G -> E -> E, tr xは全単射でtr' xがその逆写像。
    • G-作用act :: G -> E -> E
data F a = F G (E -> a)

phi :: (G, G, G) -> E -> E
phi (x,t,y) = tr' t . act y . tr (x <> t <> y)

instance Applicative F where
  pure a = F mempty (const a)
  F x x_f <*> F y y_a = F xy (\i -> xy_f i (xy_a i))
    where
      xy = x <> y
      xy_f = x_f . tr' x . act y . tr xy
      xy_a = y_a . tr' y . tr xy

改めてこの部分を読んでみると、Functorとしての(G, E -> a)への自然同型のとりかたを工夫すれば、 tr x = tr' x = idとなるようにできますね。なので、次のようにしたほうが簡潔でした。

モノイドAp F ()が群Gになるような多項式 Applicative F は、

  • Functorとして(G, E -> a)に自然同型
  • 自然同型のとりかたをうまく選べば、 どのFもある 左 G-作用act :: G -> E -> Eによって以下のように定義される：
data F a = F G (E -> a)

instance Applicative F where
  pure a = F mempty (const a)
  F x x_f <*> F y y_a = F (x <> y) (\i -> x_f (act y i) (y_a i))

また、任意の群Hに対して、Ap F Hも再び群になります。

(<<>>) :: forall h. Semigroup h => F h -> F h -> F h
(<<>>) = liftA2 (<>)
-- (<<>>) = coerce ((<>) @(Ap F h))

mempty1 :: forall h. Monoid h => F h
mempty1 = pure mempty
-- mempty1 = coerce (mempty @(Ap F h))

inv1 :: forall h. Group h => F h -> F h
inv1 (F x x_a) = F x' (inv @h . x_a . act x')
  where x' = inv @G x

これが本当に群であることは、actが群作用であることから出ます。

x, x' :: G
x' = inv x

x_a :: E -> H

w :: F H
w = F x x_a
inv1 w = F x' (inv @H . x_a . act x')

w <<>> inv1 w
 = liftA2 (<>) (F x x_a) (F x' (inv @H . x_a . act x'))
 = F (x <> x') (\i -> x_a (act x' i) <> inv (x_a (act x' i)))
 = F (x <> x') (\i -> let b = x_a (act x' i) in b <> inv b)
 = F mempty (\i -> mempty)
 = mempty1

inv1 w <<>> w
 = liftA2 (<>) (F x' (inv @H . x_a . act x')) (F x x_a)
 = F (x' <> x) (\i -> (inv . x_a . act x' . act x $ i) <> x_a i)
   -- act x' . act x = act (x' <> x) = act mempty = id
 = F mempty (\i -> inv (x_a i) <> x_a i)
 = F mempty (\i -> mempty)
 = mempty1

2つの群G,Hと群作用G -> E -> Eから新たな群を作るこの構成は、 群論の中ではズバリそのものがよく知られていて、輪積 という名前が付いています。（とえらそうに言いますが、私自身この補遺を書くまで気づいていませんでしたが。）

まとめると、

  • 多項式Applicative FunctorであるFについて、次は同値

    1. Ap F ()が群である
    2. Fに同型なApplicativeF'として F' a = (G, E -> a)が存在し、 Gは群で、左G-作用act :: G -> E -> Eから定まるApplicative演算を持つ
    3. 任意の群Hについて、Ap F Hは群である。特に、G-作用を持つ集合E上のHの輪積になる。