Coq で圏論:随伴、モナド、Kleisli triple

  • 4
    いいね
  • 0
    コメント

まとめ

前提

以下の記事を読んでおくとわかりやすいかもしれません。
- Coq で圏論:背景と普遍性について
- Coq で圏論:函手とその等価性
- Coq で圏論:自然変換とデータ型

Kleisli triple とかに関する部分は Haskell などで Monad 使ってたりする方向けです。

Cat_on_Coq のコードを実際に CoqIDE か ProofGeneral かなんかで追っていかないと、色々な部分の型とかがわかりにくくて大変かもしれません。

随伴

函手 $F: C \rightarrow D$ と函手 $G: D \rightarrow C$ が随伴であるとは、

\forall c\in C, d\in D.\ D(F(c),d) \cong C(c,G(d))

が成り立ち、さらにこの同型が $c,d$ について自然であることです。このとき、 $F \dashv G$ と書きます。

この同型を与える同型写像を $\phi_{c,d}: D(F(c),d) \rightarrow C(c,G(d))$(圏の射ではなく写像です) と書くことにすると、「自然である」とは、 $c$ を固定したときに射の族 $\phi_{c,-}$ が自然変換 $\phi_{c,-}:D(F(c),-) \Rightarrow C(c,G(-))$ となり、$d$ を固定したときに射の族 $\phi_{-,d}$ が自然変換 $\phi_{-,d}:D(F(-),d) \Rightarrow C(-, G(d))$ となることを意味します。

定義

上述した二つの自然性は、以下の等式にまとめることができます。

\forall f\in C(c',c),g\in D(d,d'),h \in D(F(c),d.\ \phi_{c',d'} (g \circ h \circ F(f)) = G(g) \circ \phi_{c,d} h \circ f

実際、 $f$ や $g$ を恒等射にした場合を考えてみれば、二つの自然性は簡単に導けます。

Coq 上で定義する際、こちらの等式の方が単純ですので、これを使って随伴を定義することにします。
「同型写像」と言っているので、 $\phi_{c,d}$ の逆写像も随伴の構成要素になっています。

Class IsAdjunction
      (C D: Category)(F: C --> D)(G: D --> C)
      (lr: forall {c: C}{d: D}, Map (D (F c) d) (C c (G d)))
      (rl: forall {c: C}{d: D}, Map (C c (G d)) (D (F c) d)) :=
  {
    adj_iso_lr_rl:
      forall (c: C)(d: D)(f: D (F c) d),
        rl (lr f) == f;

    adj_iso_rl_lr:
      forall (c: C)(d: D)(g: C c (G d)),
        lr (rl g) == g;

    adj_lr_naturality:
      forall (c c': C)(d d': D)(f : C c' c)(g: D d d')(h: D (F c) d),
        lr (g \o h \o fmap F f) == fmap G g \o lr h \o f
  }.

adj_lr が $\phi$ で、 adj_rl が $\phi^{-1}$ です。

Structure Adjunction (C D: Category)(F: C --> D)(G: D --> C) :=
  {
    adj_lr: forall {c: C}{d: D}, Map (D (F c) d) (C c (G d));
    adj_rl: forall {c: C}{d: D}, Map (C c (G d)) (D (F c) d);

    prf:> IsAdjunction (@adj_lr) (@adj_rl)
  }.
Existing Instance prf.

Notation "F -| G ; C <--> D" := (Adjunction (C:=C) (D:=D) F G) (at level 40, no associativity).
Notation "F -| G" := (F -| G ; _ <--> _) (at level 40, no associativity).
Notation "[ 'Adj' 'of' F , G 'by' lr , rl ]" :=
  (@Build_Adjunction _ _ F G lr rl _).
Notation "[ 'Adj' 'by' lr , rl ]" := [Adj of _, _ by lr, rl].
Notation "[ F -| G 'by' lr , rl ]" := [Adj of F,G by lr,rl].

unit & counit

随伴は、 hom 集合の同型写像から定義する方法の他、ある等式を満たす二つの自然変換から定義することもできます。

函手 $F: C \rightarrow D$ と $G: D \rightarrow C$ に対して、二つの自然変換 $\eta: Id_C \Rightarrow G\circ F$ と $\epsilon: F \circ G \Rightarrow Id_D$ が

\epsilon F \circ F \eta = Id_F,\ G\epsilon \circ \eta G = Id_G

を満たすとき、これも随伴を与えます。
この時、 $\eta$ と $\epsilon$ をそれぞれ随伴の unit, counit と呼び、同型写像 $\phi_{c,d}:D(F(c),d)\cong C(c,G(d))$ は $\phi_{c,d}(f) = G(f)\circ \eta_c$ と $\phi^{-1}_{c,d}(f) = \epsilon _d \circ F(f)$ でもって構成できます。

この事実を Coq 上で書き下すと以下のようになります。

Definition adj_triangle 
           (C D: Category)
           (F: C --> D)(G: D --> C)
           (au: (Id C) ==> (G \o F))
           (ac: (F \o G) ==> (Id D)) :=
  ([1 \o * ==> *]
     \o (ac o> F)
     \o Nassoc
     \o (F <o au)
     \o [* ==> * \o 1]
   == Id F
    in Natrans_setoid _ _)      (* acF \o Fau == Id_F *)
  /\
  ([* \o 1 ==> *]
     \o (G <o ac)
     \o Nassoc_inv
     \o (au o> G)
     \o [* ==> 1 \o *]
   == Id G
    in Natrans_setoid _ _).     (* Gac \o auG == Id_G *)

Program Definition Adjunction_by_unit_and_counit
        (C D: Category)
        (F: C --> D)(G: D --> C)
        (au: (Id C) ==> (G \o F))
        (ac: (F \o G) ==> (Id D))
        (Hadj: adj_triangle au ac)
  : F -| G :=
  [Adj by (fun c d => [g in D (F c) d :-> fmap G g \o au c]),
          (fun c d => [f in C c (G d) :-> ac d \o fmap F f])].

はい。満たすべき性質を adj_triangle として定義しましたが、自然変換の合成がぐちゃぐちゃしていますね。
何故かといえば、通常の圏論では暗黙の内に行なわれている変換を明示的に記述しているからです。

\begin{eqnarray*}
(H \circ G) \circ F & = & H \circ (G \circ F) \\
F \circ Id_C & = & F\\
\ Id_D \circ F & = & F
\end{eqnarray*}

みたいなものは、暗黙のうちに左辺の函手から右辺の函手への自然変換(あるいはその逆)を適用することで為されているのです。
S: F ==> GT: G' ==> H が与えられたとき、 $G = G'$ が G = G' ではなく自然同型を表わしている場合、その同型を使って ST の間のクッションにする必要があるわけです。

なお、 Notation を使って見た目でなんとかわかるようにしていますが、結合律や単位元律を意味する自然変換たちの元の定義も載せておきます。中身は全部恒等射なんですけどね。

Program Definition Natrans_id_dom (C D: Category)(F: C --> D): (F \o Id C) ==> F :=
  [X :=> Id (F X)].
Notation "[ * \o '1' ==> * ]" := (Natrans_id_dom _).

Program Definition Natrans_id_dom_inv (C D: Category)(F: C --> D): F ==> (F \o Id C) :=
  [X :=> Id (F X)].
Notation "[ * ==> * \o '1' ]" := (Natrans_id_dom_inv _).

Program Definition Natrans_id_cod (C D: Category)(F: C --> D): (Id D \o F) ==> F :=
  [X :=> Id (F X)].
Notation "[ '1' \o * ==> * ]" := (Natrans_id_cod _).

Program Definition Natrans_id_cod_inv (C D: Category)(F: C --> D): F ==> (Id D \o F) :=
  [X :=> Id (F X)].
Notation "[ * ==> '1' \o * ]" := (Natrans_id_cod_inv _).

Program Definition Natrans_assoc (B C D E: Category)(F: B --> C)(G: C --> D)(H: D --> E): (H \o (G \o F)) ==> ((H \o G) \o F) :=
  [ X in B :=> Id (H (G (F X)))].
Notation Nassoc := (Natrans_assoc _ _ _).

Program Definition Natrans_assoc_inv (B C D E: Category)(F: B --> C)(G: C --> D)(H: D --> E): ((H \o G) \o F) ==> (H \o (G \o F)) :=
  [ X in B :=> Id (H (G (F X)))].
Notation Nassoc_inv := (Natrans_assoc_inv _ _ _).

ついでに、自然変換と函手の合成もいつの間にか使っていますので、それも載せておきます。

Program Definition Natrans_dom_compose (B C D: Category)(E: B --> C)(F G: C --> D)(S: F ==> G)
  : (F \o E) ==> (G \o E) :=
  [X :=> S (E X)].
Notation "S o> E" := (Natrans_dom_compose E S) (at level 50, left associativity).

Program Definition Natrans_cod_compose (C D E: Category)(F G: C --> D)(H: D --> E)(S: F ==> G)
  : (H \o F) ==> (H \o G) :=
  [X :=> fmap H (S X)].
Notation "H <o S" := (Natrans_cod_compose H S) (at level 50, left associativity).

また、随伴が与えられたとき、上述の等式を満たす二つの自然変換を定義することができます。

(** unit of adjunction **)
Program Definition adj_unit (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G)
  : (Id C) ==> (G \o F) :=
  [ c :=> adj_lr adj (Id (F c))].

(** counit of adjunction *)
Program Definition adj_counit (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G):
  (F \o G) ==> (Id D)  :=
  [d :=> adj_rl adj (Id (G d))].

Lemma adj_satisfies_triangle:
  forall (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G),
    adj_triangle (adj_unit adj) (adj_counit adj).

場合によって、同型写像から作ったり unit & counit から作ったりを使い分けることになります。

モナド

$C$ 上のモナドとは、

  • 自己函手 $T: C \rightarrow C$
  • 自然変換 $\eta: Id_C \Rightarrow T$
  • 自然変換 $\mu: T \circ T \Rightarrow T$

からなる組 $\langle T, \eta, \mu \rangle$ で、

\begin{eqnarray*}
\mu \circ \eta T & = & Id_T\\
\mu \circ T \eta & = & Id_T\\
\mu \circ T \mu & = &\mu \circ \mu T
\end{eqnarray*}

を満たすもののことです。

定義

Coq 上でもそのまま書きます。
この記事では Kleisli triple のための踏み台でしかないので、特に深く説明はしません。

Class IsMonad (C: Category)
      (T: C --> C)
      (unit: Id C ==> T)
      (mult: (T \o T) ==> T) :=
  {
    monad_mult_mult:
      mult \o (mult o> T) == mult \o (T <o mult) \o Nassoc_inv;

    monad_mult_unit_T:
      mult \o (unit o> T) \o [* ==> 1 \o *] == Id T;

    monad_mult_T_unit:
      mult \o (T <o unit) \o [* ==> * \o 1] == Id T
  }.

Structure Monad (C: Category) :=
  {
    monad_functor:> C --> C;
    monad_unit: Id C ==> monad_functor;
    monad_mult: (monad_functor \o monad_functor) ==> monad_functor;

    monad_prf:> IsMonad monad_unit monad_mult
  }.
Existing Instance monad_prf.
Notation "[ 'Monad' 'by' T , u , m ]" := (@Build_Monad _ T u m _).

随伴からモナド

$F: C\rightarrow D$, $G: D\rightarrow C$ に対して随伴 $F \dashv G$ が与えられたとき、 $C$ 上のモナドを構成することができます。
この時、随伴の unit $\eta$ と counit $\epsilon$ を使ってモナドを構成すると楽です。

モナドを構成する自己函手は $T := GF$ です。モナドの $\eta$ は $\eta$ そのものであり、 $\mu$ は $G \epsilon F: GFGF \Rightarrow GF$ です。

それを Coq上で記述すると次のようになります。

Definition adj_mult (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G)
  : ((G \o F) \o (G \o F)) ==> (G \o F) :=
  (G <o ([ 1 \o * ==> *] \o (adj_counit adj o> F) \o Nassoc)) \o Nassoc_inv.

Program Definition Monad_from_adj
        (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G) :=
  [Monad by (G \o F), adj_unit adj, adj_mult adj].

証明もそれほど難しくはありません。

Kleisli triple

圏 $C$ 上の Kleisli triple とは

  • 対象の割り当て $T: |C| \rightarrow |D|$
  • 射の族 $\eta_X: C(X,(T X))$
  • 射の割り当ての族 $(-)^{\sharp}_{X,Y}: C(X,T(Y)) \rightarrow C(T(X),T(Y))$

からなる組 $\langle T, \eta, (-)^{\sharp} \rangle$ であって、

\begin{eqnarray*}
\eta_X^{\sharp} & = & Id_{T(X)}\\
f^{\sharp} \circ \eta_X & = & f\\
g^{\sharp} \circ f^{\sharp} & = & (g^{\sharp} \circ f)^{\sharp}
\end{eqnarray*}

を満たすもののことです。

はい。圏論的な定義をがっと並べてもよくわからないですね。

定義

これを Coq 上で定義すると、人によっては見なれたものが出来上がります。

Class IsKt (C: Category)(T: C -> C)
      (ret: forall (X: C), C X (T X))
      (bind: forall {X Y: C}, (C X (T Y)) -> (C (T X) (T Y))) :=
  {
    kt_bind_proper:> forall (X Y: C), Proper ((==) ==> (==)) (@bind X Y);
    kt_ret_bind:
      forall (X: C), bind (ret X) == Id (T X);

    kt_bind_ret:
      forall (X Y: C)(f: C X (T Y)),
        bind f \o ret X == f;

    kt_bind_comp:
      forall (X Y Z: C)(f: C X (T Y))(g: C Y (T Z)),
        bind g \o bind f == bind (bind g \o f)
  }.

Class Kt (C: Category)(T: C -> C) :=
  {
    ret: forall {X: C}, C X (T X);
    bind: forall (X Y: C), C X (T Y) -> C (T X) (T Y);

    kt_prf:> IsKt (@ret) bind
  }.
Existing Instance kt_prf.
Notation "[ 'Kt' 'by' ret , bind ]" := (@Build_Kt _ _ ret bind _).

そうですね。 Haskell でいう Monad が、この Kleisli triple です。
また、 Monad との整合性を取るため、今回 Kt を型クラスとして定義しました。

函数型プログラミングと Kleisli triple

さて、 Kleisli triple を定義してみたわけですが、これは Haskell のモナドよりもまだ一般的な構造です。
何故かといえば、任意の圏に対して定義されているからです。

これがどういう意味を持つのかといいますと、たとえば ret を使って ret x という式を作ることが出来ません。
retC の射であって、函数ではないからです。

しかし、函数型プログラミングをする場合、射は函数として考えます。
となると、実用上は Types (Haskell では Hask 圏ですかね)上の Kleisli triple を考えることになるでしょう。
そうすれば、 ret x なども書けますし、 do 記法的なものも使えるようになります。

ということで、以下のようにして Notation を定義しておきましょう。

(** Special Notation for Kt on Types **)
Notation "m >>= f" := (bind (C:=Types) f m) (at level 53, left associativity).
Notation "[ 'do' M 'in' K ]" := (let _kt := K: Kt Types _ in M). 
Notation "[ 'do' M ]" := [do M in _].
Notation "x <- m ; p" := (m >>= (fun x => p)) (at level 60, right associativity).
Notation ":- x ; m" := (_ <- x ; m) (at level 61, right associativity, x at next level).
Notation "x <-: m ; p" := (x <- ret m ; p) (at level 60, right associativity).
Notation "f >> g" := (bind (C:=Types) g \o f) (at level 42, right associativity).

[do M in K] 記法が地味に重要な役目を持っていますが、使う場面で説明します。

具体例: Maybe & List

つらつら述べていても仕方ないので、具体例を見ていきましょう。

Maybe モナド

まずは失敗しうる計算を表す Maybe です。

Program Instance Maybe: Kt Types option :=
  {
    ret X x := Some x;
    bind X Y f m := match m with
                    | Some x => f x
                    | None => None
                    end
  }.

計算例を見てみましょう。
まずは hd_error が成功する例で、

Eval compute in
    [do x <-: 0;
       y <- hd_error [1;2];
       ret (x, y) in Maybe].
(* = Some (0, 1) *)
(* : option (product nat nat) *)

次は失敗する例です。

Eval compute in
    [do x <-: 0;
       y <- hd_error [];
       ret (x, y) in Maybe].
(* = None *)
(* : option (product nat ?B) *)

はい。ちゃんと機能していますね。

List モナド

では次の例、非決定的計算を表す List モナドです(Kleisli triple です)。

Program Instance List: Kt Types list :=
  {
    ret X x := [x];
    bind X Y f l := flat_map f l
  }.

計算例はこんな感じです。

Eval compute in
    [do x <- [3;1;4;1;5];
       y <-: (x + 1);
       ret y in List].
(* = [4; 2; 5; 2; 6] *)
(* : list nat *)

また、このようにして guard を導入することもできます(一般に、失敗を表現できる計算に対して定義可能(なはず)ですが、今回は List に特化させています)。

Definition guard {X: Type}(b: X -> bool)(x: X): list X :=
  if b x then [x] else [].

これを使った計算例が次の通りです。。

Fixpoint evenb (n: nat): bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => evenb n'
  end.

Eval compute in
    [do x <- [0;1;2;3] ;
       y <-: (x + 1);
       :- guard evenb y ;
       ret x in List].
(* = [1; 3] *)
(* : list nat *)

do 記法

さて、さきほど触れた [do M in K] 記法ですが、これは Coq 上で Monad (Kleisli triple) を扱う上では欠かせません。
なぜなら、利用される Monad のインスタンスが、直近で定義されたインスタンスになってしまうからです(この挙動はどうかと思うのですが、現状そうなってしまっているので、どうしようもないです)。
そのため、 let を使って M を囲むインスタンスを K で上書きすることで、利用する do 記法で利用する型クラスのインスタンスを指定できるようにしているのです。

その結果、以下のようなネストした do 記法も可能になっています。

Eval compute in
    [do x <-: 0;
       y <- (hd_error
               [do x <- [0;1;2;3] ;
                  y <-: (x + 1);
                  :- guard evenb y ;
                  ret x in List]);
       ret (x, y) in Maybe].
(* = Some (0, 1) *)
(* : option (product nat nat) *)

モナドと Kleisli triple の等価性

モナドから Kleisli triple が作れ、その逆も可能で、さらにその二つの構成は互いに逆になっています。
数式で書くのは面倒なので割愛しますが、 Coq 上で書くと次のようになります。

Program Definition Kt_from_Monad (C: Category)(T: Monad C)
  : Kt C T :=
  [Kt by monad_unit T,
         fun (X Y: C)(f: C X (T Y)) =>
           monad_mult T Y \o fmap T f].

Program Definition Monad_from_Kt (C: Category)(T: C -> C)(kt: Kt C T) :=
  [Monad by [Functor by f :-> bind (ret \o f) with X :-> T X],
            [X :=> ret],
            [X :=> bind (Id (T X))]].

この二つが互いに逆であることを示すため、まずはモナドと Kleisli triple の等価性を定義しておきます。

Program Definition Monad_setoid (C: Category) :=
  [Setoid by (fun (M N: Monad C) =>
                (monad_functor M == monad_functor N)
                /\(forall X: C, monad_unit M X =H monad_unit N X)
                /\(forall X: C, monad_mult M X =H monad_mult N X))].

Program Definition Kt_setoid (C: Category)(T: C -> C) :=
  [Setoid by (fun (k k': Kt C T) =>
                (forall X: C, ret (Kt:=k)(X:=X) == ret (Kt:=k'))
                /\(forall (X Y: C)(f: C X (T Y)),
                      bind (Kt:=k) f == bind (Kt:=k') f))].

そうすると、以下のようにしてその事実を示すことができるようになります(証明は省略していますが)。

Lemma Monad_Kt_Monad_eq:
  forall (C: Category)(T: Monad C),
    T == Monad_from_Kt (Kt_from_Monad T) in Monad_setoid C.

Lemma Kt_Monad_Kt_eq:
  forall (C: Category)(T: C -> C)(kt: Kt C T),
    kt == Kt_from_Monad (Monad_from_Kt kt) in Kt_setoid C T.

直積と羃の随伴から State モナドを構成する

さて、有名な例ですが、直積を与える操作 $(-,Y): C \rightarrow C$ と羃を与える操作 $(-)^Y: C \rightarrow C$ はそれぞれ函手になります。
そして、この二つは随伴 $(-,Y)\dashv (-)^Y$ をなし、その随伴から構成されるモナド(から作られる Kleisli triple)が State モナドになります。

以下、順を追ってそれを見ていきましょう。

ですがその前に、まず、大事なことをやっておきます。
Types 上で State モナドを作るには Functional extensionality が必要です。

Require Import FunctionalExtensionality.

直積函手

以前、 Coq 上での直積は定義しました が、再掲しておきます。

Class IsProduct (C: Category)(X Y: C)
      (P: C)(pi1: C P X)(pi2: C P Y)
      (univ: forall (Z: C), C Z X -> C Z Y -> C Z P) :=
  {
    product_universality_1:
      forall (Z: C)(p1: C Z X)(p2: C Z Y),
        (p1 == pi1 \o univ Z p1 p2);

    product_universality_2:
      forall (Z: C)(p1: C Z X)(p2: C Z Y),
        (p2 == pi2 \o univ Z p1 p2);

    product_uniqueness:
      forall (Z: C)(p1: C Z X)(p2: C Z Y)(u: C Z P),
        (p1 == pi1 \o u) ->
        (p2 == pi2 \o u) ->
        u == univ Z p1 p2
  }.

Structure Product (C: Category)(X Y: C) :=
  {
    product_obj:> C;
    product_proj1: C product_obj X;
    product_proj2: C product_obj Y;

    product_univ: forall (Z: C), C Z X -> C Z Y -> C Z product_obj;

    product_prf:> IsProduct product_proj1 product_proj2 (@product_univ)
  }.
Existing Instance product_prf.

Notation "[ 'Product' P 'by' univ 'with' pi1 , pi2 ]" :=
  (@Build_Product _ _ _ P pi1 pi2 univ _).
Notation "[ 'Product' 'by' univ 'with' pi1 , pi2 ]" :=
  [Product _ by univ with pi1, pi2].

Notation "[ f , g 'to' P ]" := (product_univ P f g).
Notation "pi1_{ P }" := (product_proj1 P) (at level 0, no associativity, format "pi1_{ P }").
Notation "pi2_{ P }" := (product_proj2 P) (at level 0, no associativity, format "pi2_{ P }").

次に、 Types 上での Product を構成します。

Inductive product (A B: Type): Type :=
| pair_of (fst: A)(snd: B).

Definition fst (A B: Type)(p: product A B): A :=
  match p with
  | pair_of a _ => a
  end.

Definition snd (A B: Type)(p: product A B): B :=
  match p with
  | pair_of _ b => b
  end.

Notation "( x , y )" := (pair_of x y) (format "( x ,  y )").

Notation "p .1" := (fst p) (at level 5, left associativity, format "p .1").
Notation "p .2" := (snd p) (at level 5, left associativity, format "p .2").

Program Definition product_of_Types (X Y: Type)
  : Product Types X Y :=
  [Product (product X Y) by (fun P f g x => (f x, g x))
   with @fst X Y, @snd X Y].

そして、直積を与える操作から函手を構成します。
条件として必要なのは任意の二対象に対してその直積が存在することです。

Definition product_map (C: Category)(prod: forall (X Y: C), Product C X Y)
           (X X' Y Y': C)(f: C X Y)(g: C X' Y')
  : C (prod X X') (prod Y Y') :=
  [f \o pi1_{prod X X'} , g \o pi2_{prod X X'} to (prod Y Y')].
Notation "[ f \* g 'with' prod ]" := (product_map prod f g).

Program Definition Product_2_functor (C: Category)(prod: forall X Y: C, Product C X Y)(Y: C)
  : C --> C :=
  [Functor by (fun (W X: C)(f: C W X) => [f \* Id _ with prod ])
   with (fun X => prod X Y) ].

羃の圏論的定義は こちら(wikipedia) を御参照ください。
これを Coq 上で定義すると次のようになります。

Class IsExponential
      (C: Category)
      (prod: forall (X Y: C), Product C X Y)
      (Y Z: C)
      (exp: C)(ev: C (prod exp Y) Z)
      (univ: forall (X: C)(g: C (prod X Y) Z), C X exp) :=
  {
    exp_universality:
      forall (X: C)(g: C (prod X Y) Z),
        g == ev \o [univ X g \* Id Y with prod];
    exp_uniqueness:
      forall (X: C)(g: C (prod X Y) Z)(u: C X exp),
        g == ev \o [u \* Id Y with prod] ->
        u == univ X g
  }.

Structure Exponential
          (C: Category)(prod: forall (X Y: C), Product C X Y)
          (Y Z: C) :=
  {
    exp_obj:> C;
    exp_eval: C (prod exp_obj Y) Z;
    exp_univ: forall (X: C), C (prod X Y) Z -> C X exp_obj;

    exp_prf:> IsExponential exp_eval exp_univ
  }.
Existing Instance exp_prf.

Notation "[ 'Exp' exp 'by' univ 'with' eval ]" :=
  (@Build_Exponential _ _ _ _ exp eval univ _).
Notation "[ 'Exp' 'by' univ 'with' eval ]" :=
  [Exp _ by univ with eval].
Notation "[ 'curry' f 'to' exp ]" := (exp_univ exp f) (f at next level).

そして Types 上での羃対象を定義します。
Functional extenstionality が必要になるのはここです。

Program Definition exponential_of_Types (Y Z: Type)
  : Exponential (C:=Types) product_of_Types Y Z :=
  [Exp (Y -> Z)
    by (fun (X: Type) f x y => f (x, y))
   with (fun gy => gy.1 gy.2)].

羃を与える操作からは次のようにして函手が構成できます。

Program Definition Exponential_functor
        (C: Category)(prod: forall (X Y: C), Product C X Y)
        (exp: forall (Y Z: C), Exponential prod Y Z)
        (X: C)
  : C --> C :=
  [Functor by (fun (Y Z: C)(g: C Y Z) => [curry (g \o exp_eval (exp X Y)) to (exp X Z)])
   with (fun Y => exp X Y)].

State モナド

さて、直積、羃、随伴、モナド、Kleisli triple という必要な道具を定義し終えたので、 State モナドを作りましょう。

まず、直積と羃の随伴は次のようにして構成できます。
$C(X\times Y, Z) \rightarrow C(X,Z^Y)$ はいわゆるカリー化ですね。

Program Definition prod_exp_adjunction
        (C: Category)
        (prod: forall (X Y: C), Product C X Y)
        (exp: forall (Y Z: C), Exponential prod Y Z)
        (Y: C)
  : Product_2_functor prod Y -| Exponential_functor exp Y :=
  [Adj by (fun X Z => [f in C (prod X Y) Z :-> [curry f to exp Y Z]]),
          (fun X Z => [f in C X (exp Y Z) :-> exp_eval (exp Y Z) \o [f \* Id Y with prod]])].

ちなみに、定義を見てわかるように、直積と羃が存在すればこの随伴は任意の圏で構成可能です(ということは Setoids 上でも State モナドを作れるんですが、この記事では扱いません)。

そして、 State モナドは次のようにして定義できます。

Instance State (S: Type): Kt Types _ :=
  Kt_from_Monad
    (Monad_from_adj
       (prod_exp_adjunction exponential_of_Types S)).

なお、 Kt の引数として与える型変換子は定義から推論しています。
実際にどんなものなのかを見てみると、

Definition kt_fobj {C: Category}{T: C -> C}(kt: Kt C T) := T.

Definition state (S: Type) := kt_fobj (State S).
Eval compute in state.
(* = fun S H : Type => S -> product H S *)
(* : Type -> Types -> Types *)

はい。普通の State モナドで使われる型変換子と同じ形をしています。
なんか上手くいっているような気がしますね。

では、実際に計算をしてみましょう。

と、その前に補助函数たちを定義します。

Definition put {S: Type}(s: S): state S unit :=
  (fun _: S => (tt, s)).

Definition get {S: Type}: state S S :=
  (fun s: S => (s, s)).

Definition modify {S: Type}(f: S -> S): state S unit :=
  [do s <- get ; put (f s) in State S].

Definition evalState {S: Type}(X: Type)(m: state S X)(s: S) := m s.

見覚えのあるものたちですね。
これらを使った計算例は次のようになります。

Eval compute in
    [do x <-: 0;
       y <-: 1;
       ret (x, y) in State nat].
(* = fun y : nat => ((0, 1), y) *)
(* : (Monad_from_adj (prod_exp_adjunction exponential_of_Types nat)) *)
(*     (product nat nat) *)

Eval compute in
    [do x <-: 0;
       :- modify S;
       s <- get;
       ret (x, s) in State nat].
(* = fun y : nat => ((0, S y), S y) *)
(* : (Monad_from_adj (prod_exp_adjunction exponential_of_Types nat)) *)
(*     (product nat nat) *)

期待通りの挙動ですね。

evalState もこの通りです。

Eval compute in
    evalState [do x <-: 0;
                 :- modify S;
                 s <- get;
                 ret (x, s) in State nat] 5.
(*   = ((0, 6), 6) *)
(* : (Product_2_functor product_of_Types nat) (product nat nat) *)

もちろん、モナドのネストも出来ます。

Eval compute in
    [do x <-: 2;
       y <-: (evalState [do x <-: 1;
                           modify (plus x) in State nat]
                        x);
       ret (x, y.2) in Maybe].
(* = Some (2, 3) *)
(* : option (product nat nat) *)

Eval compute in
    [do x <-: 2;
       y <-: (evalState [do x <-: 1;
                           modify (plus x) in State nat]
                        x);
       ret (x, y.2) in State bool].
(* = fun y : bool => ((2, 3), y) *)
(* : (Monad_from_adj (prod_exp_adjunction exponential_of_Types bool)) *)
(*     (product nat nat) *)

というわけで、 State モナドを作って実際に動くか確かめてみる、でした。

最後に

当然ですが、 State モナドは普通に定義した方が楽です。

Definition state (S: Type) := (fun (A: Type) => S -> product A S).

Program Instance State (S: Type): Kt Types (state S) :=
  {
    ret X x s := (x, s);
    bind X Y f m s := let (x, s') := m s in f x s'
  }.

これまでの議論は、 Coq 上で展開した圏論が、 State モナドみたいなよく使われる道具たちと整合性が取れていることを確認する作業みたいなものです。
そのおかげで Coq 上での圏論の方向性が間違ってないかな、ってのを確認できるので、例としてはとても有意義なんですけどね。

これも含めて四本の記事を書き殴ってきましたが、一応、結論としてやりたかったこと(State モナド)が出来ました。
とりあえず、これまでの方針でもう少し函数型プログラミング寄りの圏論をやっていきたいですね、という感じです。

なんかいいネタないかしら。

次回予告

Kan 拡張。

この投稿は Theorem Prover Advent Calendar 201611日目の記事です。