ListとStateがFunctor則とMonad則を満たすことをIdrisで証明した

概要

Idrisの練習のために、ListモナドとStateモナドを自前で実装し、それらが確かにFunctor則とMonad則を満たすことを証明するコードを書きました。
ソースはこちら
https://github.com/yutaro-sakamoto/prove-monad
モナドには色々と種類があるため、他のモナドの証明も随時追加します。
改善点等がありましたら、遠慮なくご指摘ください。

Idrisの補完・推論機能は他の言語処理系に比べて非常に賢く、まるでコンピュータと対話しながら証明を作り出せます。
普通の言語でプログラムを書くのとは全く違う体験ができました。

Functor則と同値性の表現

interface MyFunctor (f : Type -> Type) where
  -- equality
  equalsTo : (x : f a) -> (y : f a) -> Type
  eqReflexive : {x : f a} -> x `equalsTo` x
  eqSymmetry : {x, y : f a} -> x `equalsTo` y -> y `equalsTo` x
  eqTransitive :  {x, y, z : f a} -> x `equalsTo` y -> y `equalsTo` z -> x `equalsTo` z

  -- map
  myMap : (func : a -> b) -> (x : f a) -> f b

  -- functor law
  functorLawIdentity : (x : f a) -> myMap Prelude.id x `equalsTo` x
  functorLawComposition : (v : (b -> c)) -> (u : (a -> b)) -> (x : f a) -> myMap (v . u) x `equalsTo` myMap v (myMap u x)

同値性をわざわざ再度定義する必要はないかもしれませんが、今回はStateモナドの証明における関数の同値性の判定がどうしてもうまくいかなかったため、自前で用意することにしました。

関数の同値性は次のように定義しています。「任意の引数に対して関数を適用した結果が同じなら、関数として同じ」というおなじみの定義です。

data FuncEqType : func1 -> func2 -> Type where
  funcEqType : (f : a -> b) -> (g : a -> b) -> ((x : a) -> f x = g x) -> FuncEqType f g

stateFuncEqTransitive : {f : a -> b} -> {g : a -> b} -> {h : a -> b} -> FuncEqType f g -> FuncEqType g h ->  FuncEqType f h
stateFuncEqTransitive (funcEqType f g f_eq_g) (funcEqType g h g_eq_h) = funcEqType f h (\z => rewrite f_eq_g z in g_eq_h z)

stateFuncEqReflexive : {f : a -> b} -> FuncEqType f f
stateFuncEqReflexive = funcEqType f f (\z => Refl)

stateFuncEqSymmetry : FuncEqType a b -> FuncEqType b a
stateFuncEqSymmetry (funcEqType f g a_eq_b) = funcEqType g f (\z => sym (a_eq_b z))

Monad則の表現

Monad則は次のように定義しています。

interface MyFunctor m => MyMonad (m : Type -> Type) where
  myReturn : a -> m a
  (>>>=) : m a -> (a -> m b) -> m b

  monadLawIdentityLeft : (x : a) -> (f : a -> m b) -> (myReturn x >>>= f) `equalsTo` (f x)
  monadLawIdentityRight : (n : m a) -> (n >>>= myReturn) `equalsTo` n
  monadLawComposition : (n : m a) -> (f : a -> m b) -> (g : b -> m c) ->
                        ((n >>>= f) >>>= g) `equalsTo` (n >>>= \x => f x >>>= g)

実装と証明

Listモナドの証明

詳しくは https://github.com/yutaro-sakamoto/prove-monad/blob/main/MyList.idr を見てください。
最も手間がかかったのはモナド則の結合性の証明でした。

   (xs >>= f) >>= g
== xs >>= (\z => f z >>= g)

証明の流れは、次に示す分配法則(勝手に命名)を示すところから始まります。

   (zs ++ xs) >>= g
== (zs >>= g) ++ (xs >>= g)

帰納法で証明するため、次の等式の証明を試みます。

   ((z :: zs) ++ (x :: xs)) >>= g
== ( ((z :: zs) >>= g) ++ ((x :: xs) >>= g) )

下記のような証明のメモを書いて

   (((z :: zs) ++ (x :: xs)) >>= g)
== (g z ++ ((zs ++ (x :: xs)) >>= g)) -- 帰納法の仮定を使う
== (g z ++ (zs >>= g) ++ ((x :: xs) >>= g))
== (g z ++ (zs >>= g) ++ g x ++ (xs >>= g)) -- ++ の結合法則
== ((g z ++ (zs >>= g)) ++ (g x ++ (xs >>= g)))
== ((z ::: zs) >>= g) ++ ((x :: xs) >>= g)

上のコメントをつけたところ以外はIdris処理系が勝手に式変形して推論してくれた?ようで、帰納法の仮定を使う箇所と++の結合法則を証明を書いて組み合わせることで証明できました。

distributiveLaw : (z : a) -> (zs : MyList a) -> (x : a) -> (xs : MyList a) -> (g : a -> MyList b) ->
                           (induction_assumption : ListEq ((zs +++ (x ::: xs)) >>>== g) ((zs >>>== g) +++ ((x ::: xs) >>>== g))) ->
                           ListEq (g z +++ ((zs +++ (x ::: xs)) >>>== g)) (g z +++ (zs >>>== g) +++ ((x ::: xs) >>>== g))
distributiveLaw z zs x xs g induction_assumption =
  replaceRight (g z) ((zs +++ (x ::: xs)) >>>== g) ((zs >>>== g) +++ ((x ::: xs) >>>== g)) induction_assumption

ここまでの議論で得られた分配法則を使って,次の証明のメモを作ります。帰納法により,これでモナド則の1つである結合性が示せます。

   ((x :: xs) >>= f) >>= g
== (f x ++ (xs >>= f)) >>= g --分配法則
== ((f x) >>= g) ++ ((xs >>= f) >>= g) --帰納法の仮定
== ((f x) >>= g) ++ (xs >>= \z => f z >>= g) --帰納法の仮定
== ((x :: Nil) >>= \z -> f z >>= g) ++ (xs >>= \z => f z >>= g)
== ((x :: Nil) ++ xs) >>= \z => f z >>= g --分配法則
== (x :: xs) >>= \z => f z >>= g`

これをIdrisに書き下せば完成です。

listMonadLawCompositionLemma : (zlist : MyList a) -> (xlist : MyList a) -> (g : a -> MyList b) ->
                               ListEq ((zlist +++ xlist) >>>== g) ((zlist >>>== g) +++ (xlist >>>== g))
listMonadLawCompositionLemma MyNil MyNil g = nilEq
listMonadLawCompositionLemma MyNil (x ::: xs) g = listEqReflexive
listMonadLawCompositionLemma (z ::: zs) MyNil g = listAppendNilLemma (g z +++ (zs >>>== g))
listMonadLawCompositionLemma (z ::: zs) (x ::: xs) g =
  distributiveLaw z zs x xs g (listMonadLawCompositionLemma zs (x ::: xs) g) `listEqTransitive`
  concatAssociative (g z) (zs >>>== g) (g x  +++ (xs >>>== g))

Stateモナドの証明

詳しくは　https://github.com/yutaro-sakamoto/prove-monad/blob/main/MyState.idr を見てください

Stateモナドの定義でlet文を使うとうまくいかないようで(気のせいかもしれませんが)、let文を少し避けるように書きました。

data State : Type -> Type -> Type where
  stateFunc : (s -> (a, s)) -> State s a

mapFirst : (f : a -> c) -> (a, b) -> (c, b)
mapFirst f (x, y) = (f x, y)

mapState : (f : a -> b) -> (state : State s a) -> State s b
mapState f (stateFunc g) = stateFunc (mapFirst f . g)

pureState : (s : Type) -> (x : a) -> State s a
pureState s x = stateFunc (\state => (x, state))

infixl 1 >>>==

(>>>==) : (n : State s a) -> (f : a -> State s b) -> State s b
(>>>==) (stateFunc g) f = stateFunc (\state => let x = g state in getStateFunc (f $ fst x) (snd x))

Listモナドの証明に比べればStateモナドの証明は比較的素直で,Idrisの補完機能の誘導に従って実装すれば、自然と証明が書けたように思います。

残った課題

• Applicative則を満たすことを証明していない
  • どうしてもStateがApplicative則を満たすことを証明できませんでした。Idrisの補完機能がうまく動いてくれない箇所があったためです。Listは挑戦すらしていません。