Coq/SSReflectでMonad回りの型クラスを定義する

# はじめに

証明支援系CoqでFunctorやMonad、Traverseなどの型クラスを作っていきます。
Coqでは各種演算はもちろん、Monad則等のそれらが満たす性質も記述できるので、公理を満たしていることも型クラスによって保証することができます。


ソースは[こちら](https://github.com/nekonistyle/SSReflect/tree/master/monad)です。


# 概要

まず、作った型クラスの継承関係をみていきます。

![Monad関係の型クラス.001.jpeg](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/602298/3b857f1a-ee38-82da-f41b-92b56f12b3f9.jpeg)

![MonadTransformer.jpeg](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/602298/4fd0c1e9-e550-80fc-a363-3d62cec33dc3.jpeg)


矢印は継承関係で、引き継ぎ先が矢印の先になります。

重要なのは青字の`Functor`と`Functor2`、`Kleisli`、`FF2Sequence`です。
それぞれHaskellの`Functor`と`Applicative`、`Monad`、`Traverse`に対応します。

本記事ではそれらとその他の重要な型クラスついて解説していきます。

## `Pure`

型クラス名は`pureMap`です。
任意の`m:pureMap`に対し、それ自身が`Type -> Type`にcoercionされます。

### 演算

```coq
  Definition Eta (m:Type -> Type) := forall A, A -> m A.

  Check eta. (* forall T:pureMap, Eta T *)
```

## `Functor`

型クラス名は`functorMap`です。これは名前の通りHaskellの`Functor`に対応します。


### 演算

```coq
  Definition Functor (m:Type -> Type) := forall A B, (A -> B) -> m A -> m B.

  Check functor. (* : forall T : functorMap, Functor T *)
```

### 性質

```coq
  Variable (m : functorMap).

  Lemma eq_functor : forall A B (f g:A -> B),
      f =1 g -> @functor m _ _ f =1 functor g.

  Lemma functor_id : forall A (x:m A), functor (@id A) x = x.

  Lemma functorD : forall A B C (f:B -> C) (g:A -> B) (x:m A),
      functor (f \o g) x = functor f (functor g x).
```

1つ目の公理は、Coqでは関数の外延性公理が使えないので追加したものになります。
非常によく使いますし、以下の補題も便利です。

```coq
  Lemma eq_functor_id A (f:A -> A) :
    f =1 id -> @functor m _ _ f =1 id.
```

## `PFunctor`

型クラス名`pfunctorMap`で、`pureMap`と`functorMap`を継承しています。

### 性質

```coq
  Variable (m:pfunctorMap).

  Lemma functor_eta : forall A B (f:A -> B) x,
      functor f (@eta m x) = eta (f x).
```

## `Functor2`

型クラス名は`functor2Map`で`pfunctorMap`を継承しています。これはHaskellでいうところの`Applicative`に該当し、公理も`Applicative`と同値なものになります。また、実際に`applicative`演算やApplicative則も使えるようになっています。

### 演算

```coq
  Definition Functor2 (m:Type -> Type)
    := forall A B C, (A -> B -> C) -> m A -> m B -> m C.
  Definition Applicative (m:Type -> Type)
    := forall A B, m (A -> B) -> m A -> m B.

Check functor2 (* forall T:functor2Map, Functor2 T *)
Check applicative (* forall T:functor2Map, Applicative T *)
```

ちなみに`applicative`は`functor2`を使って以下のように定義されています。

```coq
  Definition applicative : Applicative m := fun A B => functor2 (@id (A -> B)).
```

## 満たす性質

まず`m:functor2Map`に対する
`functor3 : forall A B C D, (A -> B -> C -> D) -> m A -> m B -> m C -> m D`を定義します。

```coq
  Variable (m:functor2Map).
  Let eta := eta m.

  Definition functor3 A B C D (f:A -> B -> C -> D)
             (x:m A) (y:m B) : m C -> m D := functor2 id (functor2 f x y).
```

これを用いて`functor2Map`の性質をみていきます。

```coq
  Lemma eq_functor3 A B C D (f g:A -> B -> C -> D):
    (forall x, f x =2 g x) -> forall (x:m A), functor3 f x =2 functor3 g x.

  Lemma functor2_etal A B C (f:A -> B -> C):
    forall x, functor2 f (eta x) =1 functor (f x).

  Lemma functor2_etar A B C (f:A -> B -> C):
    forall x y, functor2 f x (eta y) = functor (f^~ y) x.

  Lemma functor2D A B C D (f:B -> C -> D) (g:A -> B):
     forall (x:m A), functor2 (f \o g) x =1 functor2 f (functor g x).

  Lemma functor3Dl A B C D E (f:C -> D -> E) (g:A -> B -> C):
    forall x y, functor3 (fun x => f \o g x) x y =1 functor2 f (functor2 g x y).

  Lemma functor3Dr A B C D E (f:A -> D -> E) (g:B -> C -> D):
    forall x y z,
      functor3 (fun x y => f x \o g y) x y z = functor2 f x (functor2 g y z).
```

1つ目の性質は関数の外延性に配慮したもので、`functor2`ではなく`functor3`に関しての性質になっています。
こう定義しないと`functor2Map`が関数合成に関して閉じませんでした。

もちろん`functor2`に関しても同様に
```coq
  Lemma eq_functor2 A B C (f g:A -> B -> C):
    f =2 g -> @functor2 m _ _ _ f =2 functor2 g.
```
という性質が成り立ちます。

それ以外は引数のどちらかが`eta`だった場合と`functor`が混ざっていた場合の公理になっています。


これらの性質から以下の補題が成り立ちます。

```coq
  Lemma functor_def A B (f:A -> B):
    functor f =1 functor2 (fun => f) (eta tt).

  Lemma functor2_def A B C (f:A -> B -> C):
    functor2 f =2 functor3 (fun => f) (eta tt).
    (* tt:Unit は1点集合 *)

  Lemma functor3_eta1 A B C D (f:A -> B -> C -> D) x:
    functor3 f (eta x) =2 functor2 (f x).

  Lemma functor3_eta2 A B C D (f:A -> B -> C -> D) x y:
    functor3 f x (eta y) =1 functor2 (f^~ y) x.

  Lemma functor3_eta3 A B C D (f:A -> B -> C -> D) x y z:
    functor3 f x y (eta z) = functor2 (fun x y => f x y z) x y.

  Lemma functor2Dr A B C D (f:C -> D) (g:A -> B -> C) (x:m A) y:
    functor2 (fun x => f \o g x) x y = functor f (functor2 g x y).

  Lemma functor2Dl A B C D (f:A -> C -> D) (g:B -> C) (x:m A) y:
    functor2 (fun x => f x \o g) x y = functor2 f x (functor g y).
```

`Applicative`則も証明可能です。

```coq
  (* applicative *)
  Lemma applicative_etal A B (f:A -> B) : applicative (eta f) =1 functor f.

  Lemma applicative_etar A B (f:m (A -> B)) x:
      applicative f (eta x) = functor (@^~ x) f.

  Lemma applicativeA A B C (f:m (B -> C)) (g:m (A -> B)) x:
      applicative (applicative (applicative (eta comp) f) g) x =
      applicative f (applicative g x).
```

型クラス`Functor2Map`を`applicative`で定義しなかったのは、証明において`applicativeA`が使いづらく、証明が直感的ではなく冗長になりがちと言うのが大きいです。


## Kleisli

型クラス名は`KleisliMap`で`pfunctorMap`と`monadMap`を継承しています。これはプログラミングの世界でいうMonadですが、圏論の世界ではKleisli圏と呼ばれるものになっているのでこの名前になっています。他にも`MonadMap`がありますが、これは圏論の世界でのMonadでありKleisli圏よりも広いものになっており、実際`KleisliMap`は`MonadMap`を継承しています。

Haskellでは`Applicative`を継承していますが、後述するようにここでは継承しないで定義しています。

具体的にみていきましょう。

### 演算

演算自体は`monadMap`で定義されていますがこちらで紹介します。

```coq
  Definition Mu (m:Type -> Type) := forall A, m (m A) -> m A.

  Check mu. (* forall T:monadMap, Mu T *)
```

### 性質


```coq
  Variable (m : kleisliMap).

  Lemma mu_eta : forall A (x:m A), mu (eta x) = x.

  Lemma mu_functor_eta : forall A x, mu (functor (@eta A) x) = x.

  Lemma mu_functor_mu : forall A x, mu (functor (@mu m A) x) = mu (mu x).
  (* ここまではmonadMapでも成り立つ *)

  Lemma functor_mu : forall A B (f:A -> B) (x:m (m A)),
      functor f (mu x) = mu (functor (functor f) x).
```

プログラミングの世界におけるMonad演算とMonad則も定義してあります。

```coq
  Definition Unit := Eta.
  Definition Bind (m:Type -> Type) := forall A B, m A -> (A -> m B) -> m B.

  Definition unit : Unit m := eta.
  Definition bind : Bind m := fun A B x f => mu (functor f x).

  Lemma eq_bind A B (f g:A -> m B) :
    f =1 g -> (@bind _ _)^~ f =1 (@bind _ _)^~ g.

  Lemma bind_unitr A (x:m A) : bind x (@unit _) = x.

  Lemma bind_unitl A B x (f:A -> m B) : bind (unit x) f = f x.

  Lemma bindA A B C x (f:A -> m B) (g:B -> m C) :
    bind (bind x f) g = bind x (fun y => bind (f y) g).
```

### `functor2`との関係

haskellでは`Monad`は`Applicative`を継承していて、これはCoqでも定義できます。
しかしながらこのライブラリでは継承していません。
詳細は別の記事「[関数型言語におけるMonadクラスはApplicativeを継承するべきなのか？MonadとApplicativeとの関係を再確認する](https://qiita.com/nekonibox/items/2f89a17e0e7f4dc14961)」にもありますが、簡単にまとめるとその理由は2つあります。

1つ目は複数の定義が存在することです。

```coq
  Definition hfunctor2 : Functor2 m :=
    fun A B C f x y => mu (functor (fun x => functor (f x) y) x).
  Definition vfunctor2 : Functor2 m :=
    fun A B C f x y => mu (functor (fun y => functor (f^~ y) x) y).
```

これらは関数として異なっているため、一意に定まらないと言うのがネックになります。
Haskellでは`vfunctor2`に相当するものに固定するという制約を課してこれを回避しているのですが、これにももう1つ問題があります。

それは、Monadの演算`mu`とApplicativeの演算`functor2`の両方がある世界では
`hfunctor2`と`vfunctor2`のどちらで定義しても`KleisliMap`では証明できない以下の性質が欲しくなるからです。

```coq
  Lemma functor2_mu : forall A B C (f:A -> B -> C) (x:m (m A)) (y:m (m B)),
      functor2 f (mu x) (mu y) = mu (functor2 (functor2 f) x y).
```

これは`KleisliMap`の公理

```coq
  Lemma functor_mu : forall A B (f:A -> B) (x:m (m A)),
      functor f (mu x) = mu (functor (functor f) x).
```

が存在することから自然な性質のように見えますが、`functor2_mu`を示そうとすると、`hfunctor2`、`vfunctor2`のどちらを採用したとしても`functor2`の引数を入れ替える性質が必要になります。
しかしながら`KleisliMap`の全ての公理は合成関数の形で書け、どの公理を適用したとしてもその引数は変化しないため証明不能な命題になります。

以上のことから、`KleisliMap`は`functor2Map`を継承するのではなく、それぞれを継承し、公理に`functor2_mu`を追加した新たな型クラス`f2kleisliMap`を定義することにしました。


## FF2Sequence

型クラス名は`ff2sequenceMap`で`functorMap`を継承しています。Haskellにおける`Traversable`に対応していて以下のような演算が定義されています。

### 演算

```coq
  Definition F2Sequence (t:Type -> Type) :=
    forall (m:functor2Map) A, t (m A) -> m (t A).
  Definition F2Traverse (t:Type -> Type) :=
    forall (m:functor2Map) A B, (A -> m B) -> t A -> m (t B).
  Definition F2Consume (t:Type -> Type) :=
    forall (m:functor2Map) A B, (t A -> B) -> t (m A) -> m B.

  Check f2sequence. (* : forall T:ff2sequence, F2Sequence T *)

  Definition f2traverse : F2Traverse t :=
    fun _ _ _ f x => f2sequence (functor f x).
  Definition f2consume : F2Consume t :=
    fun _ _ _ f x => functor f (f2traverse id x).
```

`ff2sequence`自体は単に`fucntor`を継承しているのですが、その演算である`f2sequence`は同じ`functorMap`ではなく`functor2Map`を引数に取っているのが不思議でした。

そこで、この引数を`pfunctorMap`や`functorMap`に変更した演算`pfsequence`や`fsequence`を持つ型クラス`fpfsequenceMap`や`ffsequenceMap`も定義しました。
これらの公理は基本的に`ff2sequenceMap`と同じです。


そこで、これらの公理を説明する前に、まず`functor2Morphism`を定義する必要があります。

### functor2Morphism

`pre pos:funtor2Morphism -> functor2Map`があり、任意の`m:functor2Morphism`は関数`forall A, pre A -> pos A`として使用できます。

これが満たす性質は以下のようなものです。

```coq
  Variable (m:functor2Morphism).

  Definition morph_eta : forall A x, m A (eta _ x) = eta _ x.

  Definition morph_functor2 : forall A B C f x y,
      m C (functor2 f x y) = functor2 f (m A x) (m B y).
```

簡単に説明すると、$F$-Morphismは以下のような可換図式を満たす`m`を表します。

![可換図式.001.jpeg](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/602298/38c7f5c0-6553-af56-60c9-17cb62db15db.jpeg)

実際に、$F$が`eta`の場合は`pre_F = pos_F = id`かつ`m_F = id`

$F$が`functor2`の場合はCurry化して`pre_F (x,y) = (pre x,pre y)`、`pos_F (x,y) = (pos x,pos y)`かつ`m_F (x,y) = (m x,m y)`と定義したものになります。



これを用いて`ff2sequenceMap`の性質をみていきます。

## 性質

```coq
  Variable (t:ff2sequenceMap).

  Lemma f2sequence_functor_functor :
    forall (m:functor2Map) A B (f:A -> B) (x:t (m A)),
      f2sequence (functor (functor f) x) = functor (functor f) (f2sequence x).

  Lemma morph_f2sequence_def : forall (m:functor2Morphism) A x,
      m _ (@f2sequence t _ _ x) = f2sequence (functor (m A) x).

  Lemma f2sequence_idMap : forall A, @f2sequence t id_functor2Map A =1 id.

  Lemma f2sequence_compMap :forall (m n:functor2Map) A x,
            @f2sequence t (comp_functor2Map m n) A x
            = functor (@f2sequence _ _ _) (@f2sequence _ m _ x).
```

2番目の公理が`functor2Morphism`に関するものになります({fpfsequenceMap`や`ffsequenceMap`の場合はこれがそれぞれ`pfunctorMorphism`と`functorMorphism`になります)

ただ、この補題はそのままでは使いづらいので、`m`を`eta`や`mu`に具体化した補題を作っておきます。

```coq
  Lemma morph_f2sequence (m n:functor2Map) (f:forall A, m A -> n A):
    Functor2Morphism.class_of f ->
    forall A x, f _ (@f2sequence t _ _ x) = f2sequence (functor (f A) x).

  Lemma f2sequence_functor_eta (m:functor2Map) A (x:t A) :
      f2sequence (functor (@eta m _) x) = eta m x.

  Lemma f2sequence_functor_mu (m:f2kleisliMap) A (x:t (m (m A))) :
      f2sequence (functor (@mu _ _) x) =
      mu (functor (@f2sequence _ _ _) (f2sequence x)).
```


# 関数合成で閉じているか？

`functorMap`や`functor2Map`、`ff2sequenceMap`は関数合成で閉じています。すなわち、例えば任意の`m n:functorMap`に対し、`m \o n`が`functorMap`になります。
しかしなが`m n:kleisliMap`に対し、一般には`m \o n`は`kleisliMap`になりません。そこで`m \o n`が`kleisliMap`になるような条件が欲しくなります。

実は`n`が`ff2sequenceMap`と`kleisliMap`を継承した型クラス`kf2sequenceMap`に所属している場合に`m \o n`が`kleisliMap`になります。

そこで、この`kf2sequenceMap`についてみてみます。

## kf2sequence

### 性質

```coq
  Variable (m:kf2sequenceMap).

  Lemma f2sequence_eta : forall (m:functor2Map) A (x:m A),
    f2sequence (eta t x) = functor (@eta _ _) x.

  Lemma f2sequence_mu : forall (m:f2kleisliMap) A (x:t (t (m A))),
    f2sequence (@mu t _ x) =
    functor (@mu t _) (f2sequence (functor (@f2sequence _ _) x)).
```

これらは`f2sequence`の引数がそれぞれ`eta`や`mu`だった時の性質です。

これによって任意の`m:kleisliMap`と`n:kf2sequenceMap`に対し、`m \o n`が`kleisliMap`になります。

しかしながら今度は`kf2sequenceMap`が関数合成で閉じなくなります。
なぜならば、`f2sequence`の引数は`functor2Map`でなければならず、単に`kleisliMap`を継承しただけの`kf2sequenceMap`を引数に取れないためです。

ちなみに関数合成で閉じるように`functor2Map`も継承した`f2kf2sequenceMap`も定義しましたが、公理が強すぎてこれを満たす型変換子が限定されてきます。

そこで、`f2sequnece`の引数を`pfunctorMap`に拡張した型クラス`kpfsequenceMap`が必要になってきます。これならば`n:kpfsequenceMap`ならば`m \o n`が`kleisliMap`になりますし、関数合成で閉じるようになります。


このことからも、`sequence`の引数として取るのは`functor2Map`ではなく`pfucntorMap`の方がいいように思えます。


# Monad Transformer

上ではMonadの関数合成を満たす十分条件を見てきましたが、より一般にMonadを受け取ってMonadを返す関数をMonad Transformerと言います。

そのMonad Transformerを表す型クラス`kleisliTransformer`を見ていきます。

`t:kleisliTransformer`は`(Type -> Type) -> Type -> Type`として扱うことができ、演算`klift t:forall (m:kleisliMap) A, m A -> t m A`が定義されています。

任意の`m:kleisliMap`に対し、以下のように`k m`も`kleisliMap`になります。

```coq
  Variable (t:kleisliTransformer).

  Definition transformedKleisli_class_of (m:kleisliMap) :
    Kleisli.class_of (t m).

  Definition transformedKleisliMap (m:kleisliMap) : kleisliMap :=
    Eval hnf in
      @Kleisli.Pack (t m) (transformedKleisli_class_of m).
```

また、演算`klift`に関する公理は以下の通りです。

```coq
  Lemma klift_eta (m:kleisliMap) A x:
    klift (@eta m A x) = @eta (transformedKleisliMap _) _ x.

  Lemma klift_functor (m:kleisliMap) A B f x:
    klift (@functor m A B f x) =
    @functor (transformedKleisliMap _) _ _ f (klift x).

  Lemma klift_mu (m:kleisliMap) A x:
    klift (@mu m A x) =
    @mu (transformedKleisliMap _) _ (klift (functor (@klift _ _) x)).
```

ちなみに、`monadTransformer`自体も関数合成で閉じています。

## 応用

先ほどの`kpfsequenceMap`も`kleisliTransformer`とみなすことが可能です。

```coq
  Definition pfsequence_transformer (m:kpfsequenceMap) :
    kleisliTransformer :=
    Eval hnf in
      @KleisliTransformer.Pack (fun n A => n (m A))
                               (pfsequence_transformer_class_of m).
```

他にもHaskellの`ExpectT`に対応する`sumt`や`WriterT`に対応する`mult`なども`monadTransformer`になることを証明済です。

```coq
  Definition sumt (R:Type) : (Type -> Type) -> Type -> Type :=
    fun m A => m (R + A:Type).
  Definition mult (R:Type) (idx:R) (op:Monoid.law idx)
  : (Type -> Type) -> Type -> Type :=
    fun m A => m (R * A:Type).
```

### 注意

Haskellにおける`readerT`に対応する`appt`や`StateT`などは定義こそできるものの、関数の外延性公理が必要になる関係上、Coqでは公理の追加なしでは証明できないです。

```coq
  Definition appt (R:Type) : (Type -> Type) -> Type -> Type :=
    fun m A => R -> m A.
  Definition statet (R:Type) : (Type -> Type) -> Type -> Type :=
    fun m A => R -> m (R * A:Type).
```


# まとめ

Coq/SSReflectでFunctorやMonad等の型クラスを定義し、それについてまとめました。