4
応用数学解説
文献あり

圏論から見るHaskellのApplicative

1506
0

はじめに

← 前回: 圏論から見るHaskellのFunctor

前回記事ではHaskellにおけるFunctorを圏論的な視点から考察してみました。今回はその流れでApplicativeについて見てみたいと思います。

Applicativeはモナドや(強自己)関手に比べてとても新しい概念であり、圏論の範囲でモナドや強自己関手について調べられたのが1960~70年代、モッジ (Eugenio Moggi) によってモナドがプログラミングに応用されたのが1990年前後であるのに比べて、Applicativeが論文に登場したのは2008年とつい最近のことでした (しかも圏論からではなくプログラミング論側、Functional Pearlとしての掲載でした)。

圏論から見た場合、applicative functorを端的に表現するとモノイダル強自己関手というように言い表せます。ApplicativeはFunctorが持っていなかったモノイダルな性質を獲得し、そのためにプログラミングにおいても有用な性質を獲得しています。

前回からの内容

定義の都合上、定義文中ではモノイダル圏上で定義していますが、本稿の内容の範囲ではカルテシアン閉圏に読み替えて構いません。カルテシアン閉圏については前回を参照してください。

対称モノイダル閉圏(C,I,,)の上の自己関手がテンソル強性 (tensorial strength) を持つとは、A,Bについて自然なCの射の族τA,B:ATBT(AB)が存在して、次の図式を可換にするものである:

(AB)TCτAB,CT((AB)C)A(BTC)idAτB,CAT(BC)τA,BCT(A(BC))
1TAτ1,AT(1A)TA

Tがテンソル強性を持つとき、TC上にfmap:(AB)TATBの実装を持ちます。逆にTfmapの実装を持つとき、Tはテンソル強性を持ちます (前回参照)。

Applicativeの導入

関手と積の関係

関手とは圏と圏の間に定まる関係であり、圏の構造のみからその内容が決定されます。言い換えると、型の対応ATAと射の対応fTfのみからその実装が定まります。つまり、関手と二項積の間には本質的には関連性がありません。モノイダル積の構造を保存する関手を(強)モノイダル関手と言います。

モノイダル圏(C,I,),(C,I,)の間の強モノイダル関手とは、関手F:CCであって、A,Bについて自然な同型

  • γA,B:FAFBF(AB)
  • e:IFI
    が存在し、次の図式を可換にするものである:
    (FAFB)FCγA,BidFCFA(FBFC)idFAγB,CF(AB)FCγAB,CFAF(BC)γA,BCF((AB)C)F(A(BC))
    FAIidFAeFAFIγA,IFIFAγI,AIFAeidFAFAF(AI)F(IA)FA

同型γ,eがどちらも恒等射であるとき、Cストリクトモノイダルという。

また、γ,eについての条件が同型ではなく射γA,B:FAFBF(AB), e:IFIについてのみであった場合、Tlaxモノイダル、逆にγA,B:F(AB)FAFB, e:FIIについてのみであった場合、Toplaxモノイダルという。

強モノイダルな関手はlaxかつoplaxなモノイダル関手ということができます。ストリクトモノイダルは強モノイダルのさらに特別な場合であるので、これもlaxでもoplaxでもあります。

カルテシアン積を持つ圏の間の関手は、積に関する普遍性から自然にγA,B:F(A×B)FA×FBを持ちます。またカルテシアン積の単位元は終対象1であるため、ここからγe=!1に関する可換図式が成り立ち、カルテシアン積を持つ圏の間の関手はすべてoplaxモノイダルになります。

モノイダル閉圏(C,I,,)上の自己関手T:CCがテンソル強性を持つlaxモノイダル関手であって、かつ次の図式を可換にするとき、Tapplicative functorという。

(ATB)TCτA,BidA(TBTC)idγB,CT(AB)TCγAB,CAT(BC)τA,BCT((AB)C)T(A(BC))

Applicativeクラス

HaskellにおけるApplicativeは、Functor Tであって、:T(AB)TATBまたはliftA2:(ABC)TATBTC、およびpure:ATAをメソッドに持つものです。
liftA2はどちらか片方が定義されているとき、もう片方を以下で定義します:
__=liftA2(idAB)liftA2=λfxy.fmap(f)(x)y

さらに、Applicative Tは次の公理を満たすことが要請されます:

  • 単位元律 pure(idA)x=x
  • 合成律 ((pure()g)f)x=g(fx)、ただしは関数の合成を表す演算子__:(BC)(AB)ACのこと。
  • pureの自然性 pure(f)pure(x)=pure(f(x))
  • 交換律 fpure(x)=pure(λk.k(x))f

TがApplicativeであるとき、τA,B:A×TBT(A×B)が次で実装できます:
τA,B=λ(a,x).pure(λb.(a,b))x
このτの実装に対して、Applicativeの公理から
λt.pure(λ((x,y),z).(x,(y,z)))(τA×B,Ct)=λ((a,b),c).τA,B×C(a,τB,C(b,c))λ(u,a).a=λt.pure(λ(u,a).a)(τ1,At)
が成り立つため、Tのテンソル強性が示されます。τA,Bを使うとfmapの実装が
fmap(f)(x)=(pure(λ(f,x).f(x))τAB,A)(f,x)
とできるため、従ってApplicative Tにおけるfmapの実装は
fmap=λfx.pure(f)x
となります。

また、γA,B:TA×TBT(A×B)の実装は
γA,B=λ(x,y).liftA2(λab.(a,b))xy=λ(x,y).fmap(λab.(a,b))(x)y=λ(x,y).(pure(λab.(a,b))x)y
となり、ここから(T,γ,η1:1T1)がlaxモノイダル関手をなすことが示されます。従ってApplicative Tはapplicative functorをなすことがわかります。

様々な性質

定義に見られる通り、applicative functorはモノイダル関手的な性質と強自己関手的な性質を両方持ち合わせているため、それら単体の性質および相互的な性質の数々が絡み合っています。この節ではそれらをなるべく個別に考察してみたいと思います。

pure

T:CCはカルテシアン閉圏の上のapplicative functorとします。このとき、pureA:ATAは次で実装できます:
Aid×eA×T1τA,1T(A×1)TA

このとき、pureは自然変換、すなわちf:ABに対してpureBf=TfpureAが成り立ちます。
ApureAfTATfBpureBTB
加えて、以下の図式も併せて可換になります:
A×BpureA×pureBA×BpureA×B1pure1TA×TBγA,BT(A×B)1eT1
モノイダル関手の間の自然変換が上図のようなコヒーレンス条件を満たすとき、pure:IdTモノイダル自然変換であると言います。

pure1eと同一になることから、pureeの代用とすることができます (命題1)。

カルテシアン閉圏Cとその上の関手T:CCに対して、射の族γA,B:TA×TBT(A×B)pureA:ATAが存在して各添字について自然であり、さらに次の図式が可換になるとする。
(TA×TB)×TCγA,B×idT(A×B)×TCγA×B,CT((A×B)×C)TA×(TB×TC)id×γB,CTA×T(B×C)γA,B×CT(A×(B×C))
TA×1id×pure1TA×T1γA,1A×BpureA×pureBA×BpureA×BTAT(A×1)TA×TBγA,BT(A×B)
このとき、Tはapplicative functorである。

モノイダルな適用

カルテシアン閉圏の上のapplicative functor T:CCに対して、A,B:T(AB)×TATBは次で実装できます:
T(AB)×TAγAB,AT((AB)×A)TevA,BTB
定義から、この射はBに対して自然となります。evA,B同様、Aに対しては自然ではないことに注意してください。

C上での関数適用を表す射compA,B,C:(BC)×(AB)(AC)に対して、これをカリー化した射をfmapで持ち上げた射を
fmap(λg.g_):T(BC)T((AB)(AC))
とおきます。このとき、次の2つの図式が可換になります:

  1. ((pure()g)f)x=g(fx)
    (T(BC)×T(AB))×TA(fmap(λg.g_)×id)×idT(BC)×(T(AB)×TA)id×A,B(T((AB)(AC))×T(AB))×TAAB,AC×idT(BC)×TBB,CT(AC)×TAA,CTC

  2. pure(f)pure(x)=pure(f(x))
    (AB)×AevA,BpureAB×pureABpureBT(AB)×TAA,BTB

既に前節で見た通りγpureから構成できるため、関手Tpure,からapplicative functorを構成することができます。

交換律の導出

関数適用に対応するevA,B:(AB)×ABという射は、次のような普遍性を持っています。

カルテシアン閉圏Cの射f:C×ABに対して、射g:C(AB)がただ1つ存在して、次の図式が可換となる:
C×Afg×id(AB)×AevA,BB

一方で、にはこのような普遍性はありません。なので、例えば次のような図式の可換は明らかではなく、実際pureからapplicative functorを構成する際には公理として要請される必要があります。

  • pure(id)x=x
    TAjA×id(AA)×TApureAA×idTAT(AA)×TAA,A

  • fpure(x)=pure(λk.k(x))f
    A×T(AB)(aλf.f(a))×idT(AB)×Aid×pureA((AB)B)×T(AB)pure(AB)B×idT(AB)×TAA,BT((AB)B)×T(AB)AB,BTB

Applicativeな型の例:ZipList

実際にApplicativeの例としてZipListを見てみましょう。ZipListはデータとしてはリストと同一ですが、Applicativeの実装にzippingを採用したものです。

Applicativeの実装は次のようになっています:

      pure x = ZipList (repeat x)
liftA2 f (ZipList xs) (ZipList ys) = ZipList (zipWith f xs ys)
    

この実装の本質であるzipWithの挙動ですが、リスト[x1,x2,][y1,y2,]に対して[f(x1,y1),f(x2,y2),]を返します。リストの長さは2つのリストのうち短い方の長さになり、また評価順の関係で次のような評価が成り立ちます:

      >>> let f = undefined
>>> zipWith f [] undefined
[]
    

ZipListはおそらくMonadにできますが、およそ有用でないらしく2021年12月現在baseなどには実装されていません。

Applicativeの利用例:traverse

Applicativeの利用について、最たる例がおそらくtraverseでしょう。この関数はTraversableクラスのメソッドであり、Traversable tに対して次のような型を持ちます:
traverse :: Applicative f => (a -> f b) -> t a -> f (t b)

具体的な例としては、IOモナドとListに対して次のような関数が与えられます:
traverse :: (a -> IO b) -> [a] -> IO [b]

TraversableはMonadよりよほど特殊なことを要求しているためここでは扱いませんが、事実としてTraversableがApplicativeのサブクラスであることにより次のような関手がTraversableとして実装できます。以下で圏Cはカルテシアン閉かつすべての余積を持つものとします。

  • X1+X (Maybe X型)
  • XA+X (Either A X型)
  • XA×X ((A,X)型)
  • Xi=1Xi=1+X+X2+X3+ (有限リスト)

これらがtraverseの実装を持つことは、applicative functorの性質 (特にlaxモノイダル関手としての性質)と余積の持つ普遍性によって示され、モナドであることは必要としていません。

Haskellのリストは無限リストも許容していますがTraversableの実装を持ちます。実装を読む限りはTraversableがFoldableを要求していることと関連していそうですが、これに関しては調べ切れていません。

おわりに

圏論側に立ってapplicative functorがどのようなものかを観察してきました。Applicativeはどうしてもちょっと弱いMonadというような立ち位置にいるため、いまひとつ立ち位置のつかめないクラスに今後もしばらくなりつづけることと思われます。しかし、圏論的視点に立てばそもそもApplicativeの本質はモナドっぽい部分には無く、モノイダル関手、あるいはモノイダル変換としての構造および機能にあることが分かります。
そもそもAppicativeという言葉自体が、内実がapplication=適用にあることを主張していますから、その意味でもこれをモナドの腐ったのみたいに見る方がおかしいということですね (そんな見方してる人はいない)。

参考文献

[2]
Conor McBride and Ross Paterson, Applicative Programing with Effects, Journal of Functional Programming, 2008, pp. 1–13
投稿日:20211217
更新日:20231123
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。
バッチを贈って投稿者を応援しよう

バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。

投稿者

merliborn
merliborn
36
10181
圏論や普遍代数に興味があります。現在の専門は型理論および圏論的意味論です。

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中
  1. はじめに
  2. 前回からの内容
  3. Applicativeの導入
  4. 関手と積の関係
  5. Applicativeクラス
  6. 様々な性質
  7. pure
  8. モノイダルな適用
  9. 交換律の導出
  10. Applicativeな型の例:ZipList
  11. Applicativeの利用例:traverse
  12. おわりに
  13. 参考文献