Day convolutionいろいろ

  • Posted on 2020-08-07
  • Last modified on 2021-06-26

Edward Kmett (@kmett) August 4, 2020

Applicativeも単なる自己関手の圏での（略）何か問題でも？

Day convolutionという言葉は、 Haskellに圏論を持ち込む勢をフォローしていないとあんまり耳にしないかと思います。

何かというと、既にお約束の内輪ネタみたいになってしまったフレーズ

モナドは単なる自己関手の圏におけるモノイド対象だよ。何か問題でも？

的な物言いを、「Applicativeに対してもArrowに対してもできるよ」 という論文で道具として使っている、圏論由来のナニモノかです。これによると、

Applicativeは単なる自己関手の圏――にDay convolutionを入れてモノイド圏にしたもの――におけるモノイド対象だよ。何か問題でも？

です。

ちょっとここで断らせてほしいのですが、以下、「モナドは単なる……何か問題でも？」 が意味するところは既に知っている方を想定読者にさせてください。でないと、延々と圏論の解説が必要になってしまうので。

その論文でApplicativeのために使ったDay convolutionは、 Haskell的には次のように定義されます。

data Day f g c where
    MkDay :: ((a,b) -> c) -> f a -> g b -> Day f g c

instance Functor (Day f g) where
    fmap :: (c -> c') -> Day f g c -> Day f g c'
    fmap f (MkDay abc fa gb) = MkDay (f . abc) fa gb

type I a = () -> a

ここで、fとgはFunctorだと思ってください。そうするとき、 型コンストラクタDayはFunctorふたつをとってFunctorを作り出す、 Functor上の二項演算と見ることができます。これはちょうど、 (,)が型ふたつをとって型を作り出す二項演算と見ることができるようなものです。

そして、(,)のように、Dayは関手圏でのモノイド積としての性質を持ちます。（証明は省きます。） “モノイド積”というからには単位対象があり、type I a = () -> a（すなわち()を引数にとる関数をFunctorとみなしたもの） がそうです。

このIは Identity と同型なので、特に() -> aとする必要がないように思うかもしれません。 後から一般化するための布石ですので、今は気にしないでください。

さて、あるf :: Type -> TypeがApplicativeであるなら、 fは関手圏にDayとIでモノイド積をいれたモノイド圏におけるモノイド対象です。

type (~~>) f g = forall x. f x -> g x

mult :: (Applicative f) => Day f f ~~> f
mult :: (Applicative f) => forall c. Day f f c -> f c
mult (MkDay abc fa gb) = liftA2 (curry abc) fa gb

unit :: (Applicative f) => I ~~> f
unit :: (Applicative f) => forall c. (() -> c) -> f c
unit i = pure (i ())

逆に、mult と unitが先に与えられてもliftA2とpureがそこから定義でき、 multとunitがモノイドになる（結合則、単位則）ならばApplicative則を満たします。

モナドも自己関手の圏に関手の合成でモノイド積を入れたものにおけるモノイド対象だったので、 モナドもApplicativeも”適切に選んだモノイド圏でのモノイド対象”という書き方ができます。 うれしいね、というのがこの論文でDayが持ち出された理由でした。

Alternativeも（略）何か問題でも？

Day convolutionというのはなにも上に挙げた形のものだけでなく、

  • ある圏CからHaskへの関手 C->Hask のなす圏で
  • C上の任意のモノイド積に対して

構成できる、関手圏 C->Hask 上のモノイド積でもあります。

（当然、数学するときはHask以外の関手の行き先になれる圏(Setsとか)を考えるのですが、 今はおいときます。）

Applicativeに使ったものは、関手圏　Hask->Hask（Functorの自然変換たちの圏）で、 Hask上のモノイド積(,)とその単位()から作ったDay convolutionでした。

もはやHaskellではない疑似コードですが、 一般に、あるモノイド圏(C, ⊗, 1)からHaskへの関手圏で考えたDay convolutionは

data Day(C,⊗) f g c where
    -- C(-,-)は圏CのHom
    -- 言ってなかったけれども、HomはHaskellの型だと思っているので
    --   C(-,-) :: Type
    MkDay :: C(a ⊗ b, c) -> f a -> g b -> Day(C,⊗) f g c

type I a = C(1, a)

です。

今度はHask上の別のモノイド積Eitherとその単位VoidからDay convolutionを作ってみます。

data Day_E f g c where
    MkDay :: (Either a b -> c) -> f a -> g b -> Day f g c
type I a = Void -> a

(,)と()から作ったときのように、モノイド単位Iはもっと単純なProxyと同型です。 今回はさらに、Day_E f gのほうももっと単純なものに同型です。

Day_E f g c
  ~ ∃a b. (Either a b -> c, f a, g b)
  ~ ∃a b. (a -> c, b -> c, f a, g b)
  ~ (∃a. (a -> c, f a),  ∃b. (b -> c, g b))
  ~ (f c, g c)   -- CoYoneda

Applicativeのときと同じように、モノイド対象が何なのか考えると、

-- mult :: Day_E f f ~~> f
-- mult :: forall c. (f c, f c) -> f c
mult :: f c -> f c -> f c

-- unit :: I ~~> f
-- unit :: forall c. (Void -> c) -> f c
-- unit :: Proxy c -> f c
unit :: f c

これは単なるAlternativeですね……といっても、 AlternativeはApplicativeのサブクラスで、 Applicativeとの関係をきめる法則が要求されることもあるので、 Alternativeは単にモノイド対象だよ、とは言いがたいですけどね。

（余談）誰もが納得する、共通認識としてのAlternative則なるものはないです。 私は初めて知ったときはビビりました。 一応、(<|>)とemptyがモノイドになることぐらいはほぼ前提と思っていいですが、 Applicativeとの関係はすごく微妙です。

個人的には、 Alternativeのサブクラスを2つか3つ定義して、それぞれ目的にあった法則を与えたほうがよいと考えています。 例えば、パーサとして期待する法則をもつParsingクラスを定義して、manyなんかはそっちに移管するなど。 大本のAlternative直接使用をdeprecatedにまでできれば心が安らぎます。 ApplicativeをMonadの上に差し込むときを考えても、3年ぐらいかければ可能だと思います。

Contravariantでも考えるぞ

Contravariantは、 HaskからHaskへの反変関手です。言い換えれば、HaskopからHaskへの関手です。

反対圏をとっても、モノイド積は変わりません。 それらを使ったDay convolutionも考えていきます。

-- Hask^opの射
-- 本当は <- っていう識別子は使えないけど許して
type a <- b = b -> a

data DayOp f g c where
    MkDay :: ((a,b) <- c) -> f a -> g b -> DayOp f g c

instance Contravariant (DayOp f g) where
    contramap :: (c <- c') -> DayOp f g c -> DayOp f g c'
    contramap f (MkDay abc fa gb) = MkDay (abc . f) fa gb

type I a = () <- a

f, g, DayOp f gがどれもContravariantである場合を考えているのに注意です。

モノイド対象はどんな演算を持つでしょうか？

-- mult :: DayOp f f ~~> f
-- mult :: forall a b c. ((a,b) <- c) -> f a -> f b -> f c
mult :: forall a b c. (c -> (a,b)) -> f a -> f b -> f c

-- unit :: I ~~> f
-- unit :: forall c. (() <- c) -> f c
-- unit :: forall c. Proxy c -> f c
unit :: f c

これも実はすでに存在する型クラスDivisibleに相当します。 ekmett氏のライブラリなだけあって、このページで説明しているような理論的背景もざっくりとドキュメントに書いてあります。

Haskop で EitherとVoidのモノイドを考えた場合にあたるDecidableも同じライブラリにありますね。

もっとバリエーションがあるかもしれません。Bifunctorなら？Profunctorなら？Higher-Kinded Data ((Hask->Hask)->Hask) なら？

まだ見ぬ有用なクラスが眠っているかもしれないとちょっと思っています。