Logical Foundationsの2章まで読んだ＆Coqこと始め雑感
Coqでソフトウェア工学の基礎をいろいろ証明するよという趣旨（多分？）のSoftware Foundationsというウェブ上で読める教科書シリーズがある。
softwarefoundations.cis.upenn.edu
第1巻Logical FoundationsはそのままCoqの教科書になっている。これを読み進めていきたい。
とりあえず最初の2章までできたので（ただし最後の問題はいったん飛ばした・・・）、復習がてら雑感をメモ。
Fixpoint
再帰的な関数をFixpointで定義できる。例えばペアノ数として定義されているcoqの自然数の足し算：
Fixpoint add (n : nat) (m : nat) : nat := match n with | O => m | S n' => add n' (S m) end.
coqでは停止性が自明な関数しか書けない。その自明性もかなり粗いチェックになっていて、再帰のたびに必ず構造的に小さくなっていく引数が必要になる。上記のadd関数では停止するまで第一引数が必ず小さくなっていく（Sが一つずつ外されていく）。
こういう関数すら許容されない：
Fixpoint one (n : nat) : nat := match n with | O => one (S n) | _ => S O end.
one (S n)と引数が大きくなるような再帰は（人間の目からは自明に停止する関数でも）弾かれてしまう。
この制約でどううまく記述していくかはまだ慣れが必要（第2章最後の演習問題がそこで詰まっている・・・）
tactics
Fixpointを含むプログラミング構文で記述した関数などについての命題をtacticsを組み合わせて証明していくのがCoqの主眼。
第２章までで出てくるtactics：
introssimplreflexivityrewritedestructinductionassertreplace
今のところ出てきたtacticsだと、contextにH : c = trueが入っていてgoalもc = trueだとrewrite -> H. reflexivityとやってgoalをtrue = trueに変換してから自明に左右が同値だと指摘しないといけないのだけど、非常に冗長。多分contextとgoalが同じだと指摘するtacticsがあるはず・・・
assertとreplaceの使い分けがまだよくわかっていない。
assertは同じ証明の中で複数回使いたいような（でも完全に別の証明に分けるほどではない）補題のためにあるのかな。
Logical Foundationsではassertの方が先に出てくるので演習などでそっちを使いまくっていて、その後replaceを知って書き直して少し簡潔になったケースが多かった。
ただ、
coqでassertを使うと冗長だけどすぐにsubgoalの証明に移れて、replaceだとスッキリかけるけどsubgoalの証明がずっと先になるのが気になる・・・
— zehnpaard (@zehnpaard) March 31, 2021
こう書いたとおり、assertを使うとその場で導入した補題をsubgoalとして証明するのに対して、replaceだとその正当性を証明するのは当面のsubgoalの後になるので、証明の流れがわかりにくい気がする。
spacemacs develop branch
Clojureの関係でspacemacsのdevelop branchに切り替えたらそれまで不安定だったcompany-coqの補完機能の問題が全部解決した（以前は行末をm.で終わらせると自動的にmatch ....に補完されるなど非常にめんどくさかった・・・）
多分この記事：
に書いた手動でいじらないといけない部分も全部解決しているっぽい。spacemacsはdevelop branchを使うのがかなりベターなようだ。
和、積の法則の証明
演習問題に出てきた、自然数の和と積に関して交換則、結合則、分配則などの証明：
Coq proofs for addition/multiplication laws based on Software Foundations · GitHub
ゲーム性が高くて非常に楽しい。
OCamlで存在型を試してみた（その４ーーGADT）
ここまで
とモジュール関連の機能で存在型を扱う話をしてきた。
しかし、OCamlでもっとも直接的に存在型をエンコードしたいならGADTが使える。
ダメな例
まずはうまくいかない例。素直に存在型を記述しようと思ったらこんな感じになるかと思う：
type t = {create:int->'a; to_int: 'a->int; add:'a->'a->'a} (* あるいは *) type t = E of {create:int->'a; to_int: 'a->int; add:'a->'a->'a}
右辺で型変数を持ったレコードを定義するが、左辺には型変数が出てこない。
しかしこれは：
Line 1, characters 22-24: Error: The type variable 'a is unbound in this type declaration.
と怒られてしまう。普通の型だと右辺に出てくる型変数は左辺にも出てくる必要がある。
GADTを使った実装
GADTにはそんな制約はない。なのでこういう存在型の書き方ができる：
type t = E : {create:int->'a; to_int: 'a->int; add:'a->'a->'a} -> t
統一的な存在型tに型変数aとその型を使った値create、to_int、addが定義されているレコードを閉じ込めることに成功している。
この存在型に合致する、OCamlのnativeなintを使った実装は：
let ints = E {create=(fun x -> x); to_int=(fun x -> x); add=(+)}
そして同じくこの存在型に合致するペアノ数を使った実装は：
type peano = | Zero | Succ of peano let rec peano_create n = if n = 0 then Zero else Succ (peano_create (n-1)) let rec peano_to_int = function | Zero -> 0 | Succ x -> 1 + (peano_to_int x) let rec peano_add x = function | Zero -> x | Succ y -> peano_add (Succ x) y let peanos = E { create=peano_create ; to_int=peano_to_int ; add=peano_add }
となる。
使ってみる
注目する点としては、これらは両方まったく同じt型であること。
なので同じリストに放り込めるし、この値を引数にする関数も作れる：
let glist = [ints; peanos] let f x y (E r) = r.to_int @@ r.add (r.create x) (r.create y)
List.mapで関数を適用してみる：
utop # List.map (f 3 4) glist;; - : int list = [7; 7]
成功。
また、'a型の値がリークするような処理は書けない：
utop # let E r = ints in r.add (r.create 3) (r.create 4);; Line 1, characters 18-49: Error: This expression has type $E_'a but an expression was expected of type 'a The type constructor $E_'a would escape its scope
そしてもちろん'a型の内部実装を前提としたコードも書けない：
utop # let E r = ints in r.to_int @@ r.add 3 4;; Line 1, characters 36-37: Error: This expression has type int but an expression was expected of type $E_'a
存在型との対応
type tが存在型{∃X, {create:int->X; to_int:X->int; add:X->X->X}}に、let x = E { ... }がpackに、let E r = x in ...がunpackに対応しており、type tがリークできないことも含めて、しっかりと存在型で拡張されたシステムFに合致する挙動となっている。
というわけで過不足なく存在型がエンコードできるという意味で、GADTの方がモジュール機構を使うより直接に存在型に対応する書き方だと言える。
参考文献
Advanced Functional Programming: Abstraction and parametricity, Leo White https://www.cl.cam.ac.uk/teaching/1415/L28/abstraction.pdf
OCamlで存在型を試してみた （その３ーーモジュール）
今回はパラメトリックな機構はまったく使わないただのモジュールと存在型について。
第１級モジュールやファンクタによる抽象化機能と存在型について書いてきたが、型としての「存在型」はどちらの場合でもモジュールシグニチャだった。
つまり例えば：
module type ADDABLE_INT = sig type t val zero : t val create : int -> t val to_int : t -> int val add : t -> t -> t end
これが「あるt型が存在し、そのt型があてはまる以下の値が定義されている」という存在型になり、この存在型をインタフェースとして第１級モジュールやファンクタはパラメトリックな挙動を可能にしている。
しかしOCamlでモジュールシグニチャを使うためには第１級モジュールやファンクタのような強力な機能を使うまでもなく、ただのモジュールでも普通に使えるし実際使う：
module IntInt : ADDABLE_INT = struct type t = int let zero = 0 let create x = x let to_int x = x let add = (+) end module PeanoInt : ADDABLE_INT = struct type t = | Zero | Succ of t let zero = Zero let rec create n = if n = 0 then Zero else Succ (create (n-1)) let rec to_int = function | Zero -> 0 | Succ x -> 1 + (to_int x) let rec add x = function | Zero -> x | Succ y -> add (Succ x) y end
IntIntもPeanoIntもstruct ... endで定義されている実装に対し、抽象型を持つシグニチャADDABLE_INT型としてモジュール名を束縛されている。
これでTaPLでいうところの「抽象的データ型としての存在型」的なことはできている。つまり内部実装は全然違うモジュールの型を隠蔽することで、統一されたインタフェースを通してのみデータを操作できるようになっている。
ただし、同一のインタフェースであるからといって異なるモジュールを同じデータ構造に入れたり動的に入れ替えて使ったりなどはできない。
これまでの三記事をまとめると
モジュール
シグニチャで隠蔽することで抽象型を作成し、抽象的データ型のように内部実装は触れずインタフェースを通してのみ操作できるデータを提供できる。その場合隠蔽された抽象型と、提供されたインタフェースが「存在型」的となる。動的な入れ替えを含めた「同一インタフェースを持つモジュールを統一的に扱う」といった処理はファンクタ・第１級モジュールを使わないとできない。
ファンクタ
ファンクタ内部では、引数モジュールをシグニチャのインタフェースを通してのみ操作できる、という制約によって同じコードで「同一のインタフェースを持つ（≒特定の存在型に属するモジュール？）モジュールなら何でも扱える」パラメトリック性を持つ。ただし完全に静的な挙動でファンクタを特定のモジュールに適用して新しいモジュールを作成する必要があり、動的な入れ替えなどはできない。その分、t型のデータを返す（t型がファンクタ外部にリークする）ような関数も書くことができる。
第１級モジュール
「存在型で拡張されたシステムF」の挙動と合致させることができる（ただし第１級モジュールでは抽象型がないシグニチャを使うこともでき、その場合は存在型にはならない）。pack/unpackに個別に相当する構文let m = (module M : T)、let module M = (val m)が存在し、モジュールをそのままデータとして扱える。例えばリストなどのデータ構造に異なるモジュールをデータ化したものを入れたり、引数を「特定のシグニチャに合致するデータ化されたモジュール」とすることで関数を「モジュールにパラメトリック」にすることができる。（ただし「モジュールにパラメトリック」な関数はt型を返すことはできない。これも「存在型で拡張されたシステムF」と同じ挙動だ）
というわけで
- 完全に存在型に合致した挙動が欲しいなら第１級モジュール
- 実装を隠蔽した抽象的データ型が欲しいだけならモジュール、
- モジュール選択は静的に解決されるが「存在型」的なインタフェースにパラメトリックなコードを書きたいならファンクタ
という使い分けになるかと思う。実際のOCamlプログラミングで第１級モジュールが必要となるのは稀な印象だ。
ちなみに存在型をそのままエンコードするだけが目的ならモジュール機構に頼る必要はなく、GADTでもできる。
次回はその話。
OCamlで存在型を試してみた （その２ーーファンクタ）
の続き。
前回は第１級モジュールを非常に綺麗に存在型に対応させられることが示せた。
しかし第１級モジュールを使わずとも、OCamlだとモジュールのシグニチャ自体が存在型的だ。（ただし微妙だが重要な差異もある）
今回はファンクタを通してシグニチャを使うことと存在型の関連について。
ファンクタ
「同じインタフェースを提供するモジュールに対してパラメトリックなコードを書く」という必要がある場合、第１級モジュールを使う手もあるが、OCamlでのより一般的な言語機構は「モジュールを引数にモジュールを返す『関数的なもの』」であるファンクタである。
前回に続いてADDABLE_INTというシグニチャとそれに合致するnative intとペアノ数を使った実装の二つのモジュールを用意する：
module type ADDABLE_INT = sig type t val zero : t val create : int -> t val to_int : t -> int val add : t -> t -> t end module IntInt = struct type t = int let zero = 0 let create x = x let to_int x = x let add = (+) end module PeanoInt = struct type t = | Zero | Succ of t let zero = Zero let rec create n = if n = 0 then Zero else Succ (create (n-1)) let rec to_int = function | Zero -> 0 | Succ x -> 1 + (to_int x) let rec add x = function | Zero -> x | Succ y -> add (Succ x) y end
前回の記事にはなかった要素として、ゼロに対応する値zeroをシグニチャ・ストラクチャ両方に追加した。
これでt * intの掛け算を計算する関数をパラメトリックに定義できる：
module MakeMul (M : ADDABLE_INT) = struct let rec mul x n = if n = 0 then M.zero else if n = 1 then x else M.add x (mul x (n-1)) end module MulInt = MakeMul(IntInt) module MulPeano = MakeMul(PeanoInt)
utop # IntInt.to_int @@ MulInt.mul (IntInt.create 5) 6;; - : int = 30 utop # PeanoInt.to_int @@ MulPeano.mul (PeanoInt.create 5) 6;; - : int = 30
MakeMulファンクタはADDABLE_INTに合致するモジュールを受け取り、mul : t -> int -> t関数を持つモジュールを返す。 ファンクタの内部では渡されたモジュールがどんな実装になっているかはわからないので、インタフェースを通してのみ引数モジュールを使える。
というわけでファンクタの引数のシグニチャに抽象型（この例ではtype t）があれば、概ね存在型だと見做せる。
ただしTaPLで定義されている存在型で拡張されたシステムFの機能とは違うところもある：
- ファンクタの中でも依然としてモジュールのままで値としてデータ構造に入れたりなどはできない
- 引数となるモジュールごとに新しいモジュールが返されるので、ファンクタの外ではモジュールを統一的に使うことにはならない
- ファンクタを使って作成したモジュールの関数から存在型の
type tがリークしてもいい
１に関しては「ファンクタ内に入る時点で引数のモジュールがpackとunpackを立て続けにされる」という見方もできる。なので途中経過であるpackされた値が出てこない（結果できることの自由度は下がる）。
２についてはMulInt.mul (IntInt.create 5) 6とMulPeano.mul (PeanoInt.create 5) 6と、結局別モジュールであることを明示しないといけないのがポイント。
３は重要なポイントで、TaPLに載っているシステムFの存在型拡張やOCamlの第１級モジュールを使うと、最終的な戻り値がtype tな関数は書けない。何らかの非多相的な確定した型（intとかstringとか）である必要がある。
それに対して例えばMulInt.mulが返すのはIntInt.t型だしMulPeano.mulが返すのはPeanoInt.t型である。ファンクタ内部では引数モジュールのtype tの実装に触れることはできないが、ファンクタの外に出てしまえば作成されたモジュールはしっかり引数モジュールのtype tにパラメータ化されている。
存在型で拡張されたシステムF、そして第１級モジュールに比べて、ファンクタはこの点に関してより自由度が高い・より表現力が強いとも言えるし、実装の隠蔽が弱いとも言える。
ファンクタの戻り値であるモジュールに対してもシグニチャを設定でき、そこで型を抽象化することもできる：
module MakeMul (M : ADDABLE_INT) : sig type t val mul : t -> int -> t end = struct type t = M.t let rec mul x n = if n = 0 then M.zero else if n = 1 then x else M.add x (mul x (n-1)) end
がこれをしてしまうと今度は引数モジュールのtype tと戻り値モジュールのtype tが一致しなくなってしまうので使い勝手が悪い。
utop # MulInt.mul (IntInt.create 5) 6;; Line 1, characters 11-28: Error: This expression has type int but an expression was expected of type MulInt.t
実装を隠蔽したいなら、ファンクタの方でシグニチャをいじるより、大元の引数モジュールのtype tを抽象型にしてしまった方がいい。
次回はそのモジュールとシグニチャと存在型の話。
spacemacsにcoq layerを入れた
四月はCoqとClojureをやっていきたい
— zehnpaard (@zehnpaard) March 27, 2021
というわけでemacsでcoq環境を整備したのでメモ。
インストールが必要だったもの：
- coq
- proof general
- spacemacs-coq
前提として
- spacemacs
- opam
は入っているものとする（opamはOCamlのパッケージマネジャー）
coq
coq本体は
opam install coq
で入る。
proof general
Proof GeneralはcoqをEmacsからアクセスできるようにするインタフェースを提供する、らしい。（ただしCoqに限らないgeneric interfaceだという説明がある。Isabelleなども使えるようだ）
インストールに関しても説明はあるのだが
Skip this step if you already use MELPA. Otherwise, add the following to your .emacs and restart Emacs
と書いてあって、具体的にどの部分が"this step"なのか一見してわかりにくかった・・・ 指示を箇条書きにしてくれればわかりやすいかなーと思うのだが・・・
とりあえずMELPAがあるならM-x package-refresh-contents RETとM-x package-install RET proof-general RETしておけば問題なくインストールできるようだ。
spacemacs-coq
Proof Generalとcompany-coqをcoq layerとしてspacemacsで使えるようにする設定集。（company-coqというのはcoq関連の補完や表示の整備、定義へのジャンプなどの機能を追加する拡張）
~/.emacs.d/privateにgit cloneした・・・ だけではダメで、~/.emacs.d/private/spacemacs-coqというディレクトリ名を~/.emacs.d/private/coqに変えてやる必要がある。
さらにmelpaを使ってProof Generalをインストールした場合、このレポジトリのデフォルトのままではうまくいかない。
このPRにある通り、proof generalのパスを指定している箇所を削除する必要がある：
その後~/.spacemacsのdotspacemacs-configuration-layersにcoqと追加してやればいい。
これで再起動してcoqがSpacemacs上で使えるようになった。
ただし何故か.v拡張子のファイルを開いてもcoq-modeに自動的にならない。今のところは手動でcoq-modeに移行させていて問題なく使えているが、今後の要調査事項である。
これで四月はSoftware Foundationsの第1巻を進めていきたい。
追記：
@fetburner さんの設定も非常に参考になる（ありがとうございます！）：
Spacemacs，僕はこんな感じの設定で Coq 書いてる https://t.co/WyUMyOM9YY
— . (@fetburner) March 27, 2021
OCamlで存在型を試してみた （その１ーー第１級モジュール）
Types and Programming Languagesの24章の主題は存在型（Existential Types）である。
私は何回読んでもここでつまづく。
この章に到達するまでに部分型やら再帰型やら型推論やら全称型やら出てくるが、まあ難しくとも、なんとなくどういった言語機能に関連する型なのかがそれなりにイメージできた。
しかし存在型に関してはまったくイメージがわかず困っていた。
To understand existential types, we need to know two things: how to build (or introduce, in the jargon of 9.4) elements that inhabit them, and how to use (or eliminate) these values in computations
とか言われて目が回ったり（useとeliminateが同じ意味なのか？）。ある存在型に含まれる値というのが「型と値の組」というのもよくわからなかった（型の値として型が出てきていいのか？）
最近OCamlのモジュール周りをいろいろ試してきてようやく直観がついてきた気がする。
というわけで復習がてらOCamlで存在型が出てくる局面を：
- 第１級モジュール
- ファンクタ
- 一般的なモジュール
- GADT
を使って示してみる。
第１級モジュール
第１級モジュールはまさに存在型！という感じの機能だ。
module type ADDABLE_INT = sig type t val create : int -> t val to_int : t -> int val add : t -> t -> t end
というシグニチャが{∃X, {create:int->X; to_int:X->int; add:X->X->X}}という存在型に対応している。
このシグニチャを満たし得る実装を二つ用意する：
module IntInt = struct type t = int let create x = x let to_int x = x let add = (+) end module PeanoInt = struct type t = | Zero | Succ of t let rec create n = if n = 0 then Zero else Succ (create (n-1)) let rec to_int = function | Zero -> 0 | Succ x -> 1 + (to_int x) let rec add x = function | Zero -> x | Succ y -> add (Succ x) y end
最初のものはOCamlのnativeな整数型であるintをそのまま使った実装、もう一つはペアノ数を使った実装となる。
第１級モジュールの機能を使うとこれらモジュールを普通の値のように扱える：
let ints = (module IntInt : ADDABLE_INT) let peanos = (module PeanoInt : ADDABLE_INT) let mlist = [ints; peanos]
intsとpeanoは元となるモジュールの内部実装は相当違うが、第１級モジュール化した時点で型が同じmodule ADDABLE_INTになる。なので両方を同一のリストに入れることができる。
そして多相的（？）に関数に渡せる：
let f x y m = let module M = (val m : ADDABLE_INT) in M.to_int @@ M.add (M.create x) (M.create y)
utop # List.map (f 3 4) mlist;; - : int list = [7; 7]
ただし戻り値は多相にはできない：
utop # let g x y m = let module M = (val m : ADDABLE_INT) in M.add (M.create x) (M.create y);; Line 3, characters 2-33: Error: This expression has type M.t but an expression was expected of type 'a The type constructor M.t would escape its scope
詳細はTaPL24章を参考にしてほしいが、明確に
let ints = (module IntInt : ADDABLE_INT) let module M = (val ints : ADDABLE_INT)
が存在型のpack/unpackに対応している。
存在型のポイントとなる言語機能は：
- 実装が異なる型とその型に関連する値を、統一的な存在型の値に変換するpack
- packされた値を再度分解して使えるようにするunpack
- unpackされたものも存在型に明示されたインタフェースのみで扱える
といったところ。抽象的データ型（代数的データ型ではないのに注意！）をカプセル化して外部インタフェースのみアクセス可能にするような機能である。
長くなってきたのでファンクタ以降の話は次回。
モジュールシグニチャの多重継承
module type ADD = sig type t val add : t -> t -> t val to_string : t -> string (* ここ *) end
のようなシグニチャを書いたが、書いていて「うーん、これはおかしいな」と思った。
MULでto_stringが必要だったからといってADDのインターフェースに追加するような関数ではない。
本当は
module type ADD = sig type t val add : t -> t -> t end module type PRINT = sig type t val to_string : t -> string end module MakeMul ( M : ???) = struct ... end
と書きたかったのだが、ここでMをADDでもありPRINTでもあると表現する???部分に当たるシグニチャの書き方に詰まってしまった。OOPでいうところのインタフェースの多重継承にあたる機能・構文である。
OCamlのモジュールシステムで継承といえばincludeなのだが、例えばこういうのはうまくいかない：
module MakeMul (M : sig include ADD include PRINT end) = struct ... end
Error: Illegal shadowing of included type t/??? by t/???などとエラーが出る。ADDでtype tが定義されるのをincludeした後にPRINTでも同じくtype tがincludeされて衝突してしまう。
そこでdestructive substitutionの出番だ！と
module MakeMul (M : sig include ADD include PRINT with type t := ADD.t end) = struct ... end
としてみたのだがError: Unbound module ADDと怒られてしまう。ストラクチャ（モジュール実装）の方だとtype t := ADD.tでいけると思うのだが、シグニチャだとADD.tのようにアクセスできないのが問題。
もうちょっと調べてみたところ：
このStackOverflow記事を見つけ、そこでこのReal World OCamlの箇所について知った：
すでにinclude ADDしてるのでinclude PRINT with type t := tでいい：
module MakeMul (M : sig include ADD include PRINT with type t := t (* 二番目のtはADDから来ている *) end) = struct ... end
include PRINT with type t := tが何をしているかというと、PRINTシグニチャに出てくるtへの言及を現在のスコープにあるtに置き換えた上でPRINT内のtype tという定義を消し去ってしまう。これでto_stringはADDに定義されているtからstringへの関数になる。
しかしRWOで書かれている通り、確かに：
module MakeMul (M : sig type t include ADD with type t := t include PRINT with type t := t end) = struct ... end
の方がADDもPRINTも統一的に扱っていていい感じだ。こちらを使っていきたい。
ちなみに
module MakeMul (M : sig type t include ADD with type t = t include PRINT with type t = t end) = struct ... end
とtype t = tとしてしまうと
Error: Multiple definition of the type name t.
Names must be unique in a given structure or signature.
とエラーになる。includeで継承する時は大抵=ではなく:=でdestructive substitutionを使う必要がある。
最初に知った時は「なんだこの変な機能は」と思ったものだが、destructive substitutionは意外と非常に便利な機能である。
