sequenceA == distribute?

sequenceA-eq-distribute.md

https://twitter.com/lotz84_/status/1787796266484908211

lotz @lotz84_

これを書いていて Vector n a 同士の sequenceA が distribute のように振る舞うのが気になった👀 一般に Traversable の distribute が Distributive の sequenceA に一致することが則を使って言えないだろうか？🤔 QuickCheck で少し探してみたけど反例はなさそう

大枠

次の(1)-(3)のステップに分けられそうです。

(1) 任意のTraversable tに対して、sequenceA :: t (k -> a) -> k -> t a と distribute :: t (k -> a) -> k -> t a が等しい

(2) Representable f、すなわちある型kを使って(->) kと同型なFunctor fが持ち得るApplicative fのインスタンスは唯一つ

(3) 任意のDistributiveはRepresentableでもある

(1)-(3)をまとめると、任意のTraversable tとApplicative fかつDistributive fについて、 sequenceA @t @f = distribute @f @tが成り立ちます。

(1)について

(1) 任意のTraversable tに対して、sequenceA :: t (k -> a) -> k -> t a と distribute :: t (k -> a) -> k -> t a が等しい

これは以下のように示せます。

次の関数evを考えます。

ev :: k -> (k -> a) -> Identity a
ev i f = Identity (f i)

任意のk型の値iに対して、ev iは自然変換 ((->) k) ~> Identityで、しかもこれは Applicative準同型にもなっています。そのため、Traversable則Naturalityから、

sequenceA . fmap (ev i) = (ev i) . sequenceA :: t (k -> a) -> Identity (t a)

が成り立ちます。この左辺のsequenceAの型はt (Identity a) -> Identity (t a)であり、 Traversable則Identityから

sequenceA . fmap (ev i) = Identity . fmap (runIdentity . ev i)

が得られます。η展開したりevの定義を展開するなどして両辺を整理すると、 任意の(x :: t (k -> a))に対して

Identity (fmap ($ i) x) =  Identity (sequenceA x i)

すなわち

fmap ($ i) x = sequenceA x i

を得ます。定義より distribute x i = fmap ($ i) x なので

sequenceA x i = distribute x i

です。i, xともに任意の値について成り立っているため、sequenceA = distributeです。

(2)について

(2) Representable f、すなわちある型kを使って(->) kと同型なFunctorが持ち得るApplicative fのインスタンスは唯一つ

Applicative ((->) k)のインスタンスはに、以下の定義以外のものがあり得ないことを示せば十分です。（もし、あるRepresentable fが2つの異なるApplicative fのインスタンスを取れたとすると、fは(->) kと同型なのだから、同型で写すことで((->) k)にも2つのインスタンスが作れてしまいます。）

instance Applicative ((->) k) where
    pure :: forall a. a -> (k -> a)
    pure x _ = x
    
    (<*>) :: forall a b. (k -> (a -> b)) -> (k -> a) -> (k -> b)
    f <*> g = \i -> (f i) (g i)

Parametricityを使うと、まずpureは型によってこの定義以外にないことがわかり、 更に(<*>)と同じ型をもつ関数は必ず、 あるop1, op2 :: k -> kを使って以下のように書くことができることがわかります。 (Applicative則を考慮に入れずともこの形に限られます。)

f <*> g = \i -> (f (op1 i)) (g (op2 i))

ここでApplicative則も用いると、op1 = op2 = idであることが示せます。（証明略）

(3)について

このことはData.Distributiveのドキュメントにおいて証明なしに書かれています。 実際に成り立つという証明は、（実は自分ではあまりきちんと理解できていないのですが、）以下のブログで詳しく説明されていました。

https://duplode.github.io/posts/every-distributive-is-representable.html