Lean Theorem Prover で Maybe モナドを作ってみる。
[2016/12/11 追記]下記はlean2の場合。[/追記]
その前にセットアップ関連のメモ。私は Windows ユーザーなので、Windows の場合について。このダウンロードページ からバイナリをダウンロードできるが、ライブラリが古い感じなので、GitHub からソースコードを取得してビルドする。
GitHubに手順が書いてあるのでそれに従うだけ。Windowsの場合、msys2かCygwinが必要ですが、私はmsys2で。このページに書いてある通りに、まずはmsys2をインストールし、次に依存ライブラリをインストール、そしてGitHubからソースを取得してビルド。特に問題なく終了。
[2016/12/11 追記]
lean3の場合は次のようにする。
- バイナリはまだないようなので、GitHub からソースコードを取得。
- Cygwinの記述がなくなっているので、msys2で。
- Build Lean に記述されている「cmake ../src -G Ninja -D CMAKE_BUILD_TYPE=Release」は「cmake ../src -G Ninja -DCMAKE_BUILD_TYPE=Release」が正しいので注意する。
[/追記]
なお、ドキュメントとしてオンラインとPDFのバージョンのチュートリアルがあり、このページからリンクまたはダウンロードできる。
[2016/12/11 追記]
以下の記述は lean2 のものです。lean3 ではそのままでは動きません。
[/追記]
ではモナドクラスを作ってみる。
structure Monad [class] (M : Type → Type) :=
(return : Π {A : Type}, A → M A)
(bind : Π {A B : Type}, M A → (A → M B) → M B)
(left_identity : Π {A B : Type} (a : A) (f : A → M B),
(bind (return a) f) = (f a))
(right_identity : Π {A : Type} (m : M A), bind m return = m)
(associativity : Π {A B C : Type} (m : M A) (f : A → M B) (g : B → M C),
bind (bind m f) g = bind m (λx, bind (f x) g))
maybeインスタンスを作る。optionはすでに定義されているので、それを使ってreturnとbindを定義。次のコードを下に追加。
namespace maybe
definition return {A : Type} (x : A) := option.some x
definition bind {A B : Type} : option A → (A → option B) → option B
| bind (option.none) f := (option.none)
| bind (option.some x) f := f x
end maybe
続いて、left_identity の定義、というか証明をする。bindの下に次を追加。
theorem left_identity {A B : Type} (a : A) (f : A → option B) :
bind (return a) f = f a :=
begin
end
ここで monad1.lean を lean.exe にかけてみると次のエラーがでる。
c:\example\monad1.lean:21:2: error: 1 unsolved subgoal
A : Type,
B : Type,
a : A,
f : A → option B
⊢ bind (return a) f = f a
c:\example\monad1.lean:21:2: error: failed to add declaration 'maybe.left_identity' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
?M_1
そこで、left_identityのbeginとendの間に apply rfl をいれてみる。
theorem left_identity {A B : Type} (a : A) (f : A → option B) :
bind (return a) f = f a :=
begin
apply rfl
end
こうするとエラーが発生しなくなる。つまり証明できた。
続いて、right_identity の証明は次の通り。さきほどのleft_identityの下に追加する。
theorem right_identity {A : Type} (m : option A) :
bind m return = m :=
begin
cases m,
apply rfl,
apply rfl
end
m のパターンによって場合分けして、それぞれ計算する、ということですね。
最後に associativity の証明。right_identity の下に追加。
theorem associativity {A B C : Type} (m : option A)
(f : A → option B) (g : B → option C) :
bind (bind m f) g = bind m (λx, bind (f x) g) :=
begin
cases m,
apply rfl,
apply rfl
end
こちらもm のパターンによって場合分けして、それぞれ計算、で証明できる。
最後にMaybeインスタンスを作成する。end maybe のあと。
definition Maybe [instance] {A : Type} : Monad option :=
Monad.mk (@maybe.return) (@maybe.bind)
(@maybe.left_identity) (@maybe.right_identity)
(@maybe.associativity)
ちなみに「@」を指定しているのは、型変数を省略しないようにするため。
これでMaybeモナドができた。最終的なコードは次の通り。
structure Monad [class] (M : Type → Type) :=
(return : Π {A : Type}, A → M A)
(bind : Π {A B : Type}, M A → (A → M B) → M B)
(left_identity : Π {A B : Type} (a : A) (f : A → M B),
(bind (return a) f) = (f a))
(right_identity : Π {A : Type} (m : M A), bind m return = m)
(associativity : Π {A B C : Type} (m : M A) (f : A → M B) (g : B → M C),
bind (bind m f) g = bind m (λx, bind (f x) g))
namespace maybe
definition return {A : Type} (x : A) := option.some x
definition bind {A B : Type} : option A → (A → option B) → option B
| bind (option.none) f := (option.none)
| bind (option.some x) f := f x
theorem left_identity {A B : Type} (a : A) (f : A → option B) :
bind (return a) f = f a :=
begin
apply rfl
end
theorem right_identity {A : Type} (m : option A) :
bind m return = m :=
begin
cases m,
apply rfl,
apply rfl
end
theorem associativity {A B C : Type} (m : option A)
(f : A → option B) (g : B → option C) :
bind (bind m f) g = bind m (λx, bind (f x) g) :=
begin
cases m,
apply rfl,
apply rfl
end
end maybe
definition Maybe [instance] {A : Type} : Monad option :=
Monad.mk (@maybe.return) (@maybe.bind)
(@maybe.left_identity) (@maybe.right_identity)
(@maybe.associativity)