Too lazy to evaluate - 多項式Applicative Functorの一般論

多項式Functor
多項式Applicative Functorの特徴づけ
- 証明
phiを関手として見る
まとめ
例
- Maybe
- List
モノイドより強い条件

多項式Functor

半年ぐらい前から、 newtype F x = F (M, E -> x) の形をしたApplicative Functorのすべてを決めるような MとE上の代数的構造を考えていました。

最近この問題が自分の中で再燃し、いろいろ考えたところ、 一般の多項式Functorを考えたほうが自然であるという結論に達しました。

一般の多項式Functor F を、ここでは次のように定義します：

type M :: Type
type E :: M -> Type  -- Dependent Type!

type    F :: Type -> Type
newtype F a = F (Σ(x :: M). E x -> a)

instance Functor F where
    fmap f (F (x, g)) = F (x, f . g)

ここで Σ(x :: M). E x -> a はDependent sum typeです。この型をもつ値は、対(x, f)であって、x :: M かつ f :: E x -> aとなるようなものです。

fの型が値であるxに依存するので、このような型はHaskellでは(自然には)書くことができませんが、拡張を駆使していろいろ工夫すると不可能ではないです。

このような型は、多項式Functorを表現します。

例を挙げるなら、Mがちょうど2つの値M0, M1をもち、 E M0 = Void, E M1 = ()とすれば、FはMaybeと同型になります。

data M = M0 | M1

type E :: M -> Type
type family E x where
  E M0 = Void
  E M1 = ()

toF :: forall a. Maybe a -> F a
toF Nothing  = F (M0, absurd)    -- absurd  :: Void -> a  ~  E M0 -> a
toF (Just x) = F (M1, const a)   -- const a :: () -> a    ~  E M1 -> a

fromF :: forall a. F a -> Maybe a
fromF (F (M0, _)) = Nothing
fromF (F (M1, f)) = Just (f ())

また、Mが自然数で、E mが『mより小さい自然数』の型であるようにすると、 E mはちょうどm個の異なる値をとる型で、Fは（有限）リスト関手です。

[]      <-> F(0, absurd)   -- E 0 ~ Void
[a]     <-> F(1, \0 -> a)
[a,b]   <-> F(2, \case {0 -> a, 1 -> b})
[a,b,c] <-> F(3, \case {0 -> a, 1 -> b, 2 -> c})
  :
  :

このように定義されたFがApplicativeになるためには、 MとE x上にどのような代数構造が必要か？を次節から考えます。

多項式Applicative Functorの特徴づけ

どんなApplicativeに対しても、モノイドAp f () ~ f ()を考えられます。 (cf. Data.Monoid.Ap)

ApplicativeであるFが多項式Functorでもあって、上のような表現がされていれば、Ap F ()とMの間に全単射

prj :: F () -> M
prj (F (x, _)) = x

inj :: M -> F ()
inj x = F (x, const ())

があります。この全単射でAp F ()上のモノイド演算をM上に写せば、 Mはモノイド演算(mempty, <>)を持ちます。このモノイド演算を前提として、 Applicative Fの実装がどうなっているか考えれば、 parametricityから

pure :: forall a. a -> F a
pure a = F (mempty :: M, const a)

および

liftA2 :: forall a b c. (a -> b -> c) -> F a -> F b -> F c
liftA2 abc (F (x, x_a)) (F (y, y_b)) = F (z, z_c)
  where
     z = x <> y
     z_c :: E z -> c
     z_c i = abc (x_a (_left i)) (y_b (_right i))
     
     _left  :: E z -> E x
     _right :: E z -> E y

である必要があります。ただし、_leftと_rightは、まだ正体のわかっていない関数です。

天下り的ですが、次の型をもつ関数phiを考えます。

phi :: Π((x,y,z) :: (M,M,M)). E (x <> y <> z) -> E y

ここでΠはDependent productです。

_left, _rightがphiを使って次のように定義されているとします。

-- 以下に注意:
--   mempty <> x <> y = x <> y = z
--   x <> y <> mempty = x <> y = z

_left :: E z -> E x
_left = phi (mempty, x, y)

_right :: E z -> E y
_right = phi (x, y, mempty)

このとき、phiが次の等式を満たすならば、FのApplicative則が従います。(証明略)

phi (mempty, y, mempty) = id
phi (x, y, z) . phi (x', x <> y <> z, z') = phi (x' <> x, y, z <> z')

逆に、各x, y :: Mの組み合わせにおける_left, _rightを、次の関数leftFactor, rightFactorにまとめたとします。

leftFactor :: Πx. Πy. E (x <> y) -> E x
rightFactor :: Πx. Πy. E (x <> y) -> E y

このとき、関数phiを以下のように定義できて、

phi :: Π(x,y,z). E (x <> y <> z) -> E y
phi (x, y, z) = rightFactor x y . leftFactor (x <> y) z

FのApplicative則からphiが上記の等式1,2を満たすことが従います。

証明

FのApplicative則から

pure id <*> (F (y, y_b)) = fmap id (F (y, y_b)) = F (y, y_b)
 = let _left = ...
       _right = rightFactor mempty y :: E y -> E y
    in F (y, \i -> (const id) (_left i) (y_b (_right i)))
 = F (y, y_b . rightFactor mempty y)

y_b = y_b . rightFactor mempty y

const <$> F (x, x_a) <*> pure () = F (x, x_a)
 = let _left = leftFactor x mempty :: E x -> E x
       _right = ...
    in F (x, \i -> const (x_a (_left i)) (const () (_right i)))
 = F (x, x_a . leftFactor x mempty)

x_a = x_a . leftFactor x mempty

prod :: F a -> F b -> F (a,b)
prod = liftA2 (,)

fabc :: F ((a,b),c)
fabc
 = (F (x, x_a) `prod` F (y, y_b)) `prod` F (z, z_c)
 = let xy_x = leftFactor x y
       xy_y = rightFactor x y
       xyz_xy = leftFactor (x <> y) z
       xyz_z = rightFactor (x <> y) z
       
       xyz_a = x_a . xy_x . xyz_xy
       xyz_b = y_b . xy_y . xyz_xy
       xyz_c = z_c . xyz_z
   in F (x <> y <> z, (xyz_a &&& xyz_b) &&& xyz_c)

fabc' :: F (a,(b,c))
fabc'
 = F (x, x_a) `prod` (F (y, y_b) `prod` F (z, z_c)
 = let xyz_x = leftFactor x (y <> z)
       xyz_yz = rightFactor x (y <> z)
       yz_y = leftFactor y z
       yz_z = rightFactor y z
       
       xyz_a = x_a . xyz_x
       xyz_b = y_b . yz_y . xyz_yz
       xyz_c = z_c . yz_z . xyz_yz
    in F (x <> y <> z, xyz_a &&& (xyz_b && xyz_c))

(\((a,b),c) -> (a,(b,c))) <$> fabc = fabc'

より、5つの等式

(1a) rightFactor mempty y = id
(2a) leftFactor x mempty = id
(3a) leftFactor x y . leftFactor (x <> y) z = leftFactor x (y <> z)
(4a) rightFactor x y . leftFactor (x <> y) z = leftFactor y z . rightFactor x (y <> z)
(5a) rightFactor (x <> y) z = rightFactor y z . rightFactor x (y <> z)

が得られる。これらを用いると、

phi (mempty, y, mempty)
   -- 定義
 = rightFactor mempty y . leftFactor (mempty <> y) mempty
 = rightFactor mempty y . leftFactor y mempty
   -- 等式(1a)および(2a)
 = id . id
 = id


phi (x, y, z) . phi (x', x <> y <> z, z')
   -- 定義
 = rightFactor x y . leftFactor (x <> y) z .
   rightFactor x' (x <> y <> z) . leftFactor (x' <> x <> y <> z) z'
   -- 内側の2項に注目
 = rightFactor x y .
   (leftFactor (x <> y) z . rightFactor x' ((x <> y) <> z)) .
   leftFactor (x' <> x <> y <> z) z'
   -- 等式(4a)で()内を変形
 = rightFactor x y .
   (rightFactor x' (x <> y) . leftFactor (x' <> (x <> y)) z) .
   leftFactor (x' <> x <> y <> z) z'
   -- ()のくくりを変更
 = (rightFactor x y . rightFactor x' (x <> y)) .
   (leftFactor (x' <> x <> y) z . leftFactor (x' <> x <> y <> z) z')
   -- 等式(5a) をはじめの()に、等式(3a)をうしろの()に適用
 = rightFactor (x' <> x) y . leftFactor (x' <> x <> y) (z <> z')
   -- 定義
 = phi (x' <> x, y, z <> z')

よって、phiの満たすべき等式1., 2.が示された。

`phi`を関手として見る

前節のphiの満たすべき法則、

phi (mempty, y, mempty) = id
phi (x, y, z) . phi (x', x <> y <> z, z') = phi (x' <> x, y, z <> z')

とてもFunctor則に似ていますね？

モノイド M が適当に与えられているとき、圏 MFac を次のように定義します。（Mの単位元は1で、Mの乗法は単に並べて書くことにします。）

MFacの対象はモノイドMの各要素
MFacの対象（モノイドMの要素）s, t に対して、射はMの要素の三つ組 (x, t, z) であって、s = xtz を満たすもの

MFac(s,t) = { (x, t, z) | s = xtz }
各対象 s に対して、 (1, s, 1) ∈ MFac(s,s) がidentity
(x, u, z) ∈ MFac(t,u) および (x’, t, z’) ∈ MFac(s,t) に対して、射の合成 ∘ が

(x, u, z)∘(x’, t, z’) = (x, u, z)∘(x’, xuz, z’) = (x’x, u, zz’) ∈ MFac(s,u)

phiの満たす法則は、とりもなおさずE :: M -> Typeが圏MFac から圏Hask への関手で、 phi がMFacの射 (x,y,z)∈MFac(xyz, y) を Haskの射E (x <> y <> z) -> E yに移すfmapであることを表しています。

※ちなみに、モノイド（対象が１つの圏と見ることもできる）の代わりに任意の圏で同じようなことをしたものが、Category of factorizationsやtwisted arrow categoryなどと呼ばれているらしいことまでは調べきれたのですが、以降力尽きました・・・

まとめ

多項式FunctorであるFがM, Eによって次のように表示されているとき、

newtype F a = F (Σ(x :: M). E x -> a)

F上のApplicativeのインスタンスは、M, Eに関する次のデータで必ず表されます。

M上のモノイド演算
EをこのモノイドMについての圏 MFac から Hask への関手にする方法(phi関数)

例

Maybe

Maybeの表示

data M = M0 | M1

instance Monoid M where
  mempty = M1
  M0 <> _ = M0
  M1 <> y = y

type family E (x :: M) where
  E M0 = Void
  E M1 = ()

に対して、圏MFacは

MFac(M1, M1) = { (M1, M1, M1) }
MFac(M1, M0) = {}
MFac(M0, M1) = { (M0, M1, M1), (M1, M1, M0), (M0, M1, M0) }
MFac(M0, M0) = { (*, M0, *) }

phiが（全く面白くないですが）

phi (M1, M1, M1) = id
phi (M0, _,  _)  = absurd
phi (_,  M0, _)  = absurd
phi (_,  _,  M0) = absurd

となります。

List

有限リストの表示

data Nat = Z | S Nat

data E (x :: Nat) where
  EZ :: E (S x)
  ES :: E x -> E (S x)

newtype List a = List (Σ(x :: Nat). E x -> a)

に対して、[]と同じApplicativeを考えると、 Natに入るモノイド演算は、自然数としての乗算によるものです。

instance Num Nat where
  fromInteger = ...
  Z   + y = y
  S x + y = S (x + y)
  
  Z   * _ = Z
  S x * y = y + (x * y)

instance Monoid Nat where
  mempty = S Z
  (<>) = (*)

圏MFacは

MFac(s,t) = { (x,t,y) | x :: Nat, y :: Nat, s == x * t * y }

phiは次のようになります：

phi :: Π(x,y,z). E (x*y*z) -> E y
phi (x,y,z) i | x*y*z == 0
  = case i of { }
      -- E (x*y*z) = E 0 is an empty type
phi (x,y,z) i | x*y*z > 0
  = (i `div` z) `mod` y

モノイドより強い条件

Mがモノイドであるだけでなくより強い条件を満たす、例えば群でもあるような場合はどうなるでしょうか？

群Gに対する圏GFacは、任意の射に対して逆射がある圏、groupoidになります。さらに、任意の2対象（= 群Gの任意の2元）の間に射があります。Eがこれからの関手であるため、どのE x, E yの間にも全単射があることがわかります。これはつまり、E xたちが有限個の値をとる型ならば、それらは全て同じ個数でなければならないということです。

群Gの単位元1に対して、GFac(1,1)は群になりますが、特にこれは群G自身と同じものです。実際、GFac(1,1)とGは1対1に対応します

GFac(1,1) = { (x,1,y) | x :: G, y :: G, 1 = x1y } = { (y^(-1), 1, y) | y :: G }

また、Gにおける単位元・合成・逆元がそのままGFac(1,1)におけるそれになります。

さらに、“標準”移動 (s,1,1) :: GFac(s,1) とその逆射 (s^(-1),s,1) :: GFac(1,s)によって、任意のGFac(s,t)とGFac(1,1)に 1対1対応がつけられます。

getPerm :: GFac(s,t) -> GFac(1,1)
getPerm (x,t,y) {- xty == s -}
 = (t,1,1) ∘ (x,t,y) ∘ (s^(-1), s, 1)
 = (s^(-1)xt, 1, y)
 = (y^(-1), 1, y)

これにより、任意の関手E :: GFac -> Haskは、そのGFac(1,1)上での挙動(= 群GFac(1,1)のE 1への作用 = G-作用)および各sにおける全単射phi (s,1,1) :: E s -> E 1のみで定義されることになります。

まとめると、モノイド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

多項式Applicative Functorの一般論