CoPLを読んでいる

最近Scrapboxが捗りすぎて、ブログを書く頻度が減ってきました。
軽くざっくりCoPLを読み、終わりに近づいてきたので少しメモを書き残しておきます。

CoPLとは

通称「CoPL」は、京大の五十嵐淳先生の「プログラミング言語の基礎概念」という本のことを指します。

プログラミング言語の動作を数学的に厳密に記述するための操作的意味論や、プログラムの誤りを実行前に検知する型システムについて解説されています。

題材となる言語にはOCamlが使われており、再帰や高階関数、パターンマッチなど、OCamlの機能を数学的に導出する方法を学びます。

この本の中でも最も特徴的なものに「オンライン学習システム」があります。
本の中で出てくる演習問題の答えを規則に則って記述して送信することで正誤判定をしてくれます。

このオンライン学習システムで実際に手を動かすことで、本をパラパラしてわかった気になっているのを打ち破ってくれるので学びが深まります。

目次は以下のようなものです。

目次

  • 第1章 自然数の加算・乗算・比較
  • 第2章 メタ定理と帰納法による証明
  • 第3章 整数・真偽値式の評価
  • 第4章 定義、変数束縛と環境
  • 第5章 関数と再帰
  • 第6章 静的有効範囲と名前無し表現
  • 第7章 リストとパターンマッチング
  • 第8章 単純型システム
  • 第9章 多層的型システム
  • 第10章 型推論

1,2章でペアノ自然数などを学びながら導出システムの扱いに慣れていきます。
3章から7章はMLの機能を導出していき、8章からは型の話に入ります。

前提知識や関連しそうな本について

関連する知識や本について少し紹介します。

OCamlの話

この本を読むに当たって、関数型言語の知識、特にOCamlの知識があるとだいぶ楽ができますが、基礎文法について少し解説があるので絶対に必要というわけでもなさそうです。

OCamlを学ぶに当たっては同じ著者の表紙がラクダの本が詳しいですが、ぱぱっと文法を知りたいぐらいであればこの資料が役に立つかもです。

それ以外の話

論理学の初歩や、ペアノ自然数などの話題が出てくるので、この辺に慣れておくとだいぶ楽な気がします。

論理学については、「入門!論理学」という本が易しいです。

オンライン学習システムで例題を解く時の手順として、規則とにらめっこして導出していく感覚は、数学ガールを読んだことがあれば数学が苦手な人でもなんとなく感覚がわかる気がします。

特に3作目の「数学ガール/ゲーデルの不完全性定理」では、最初の方にペアノ自然数や論理式についての話が出てきます。
僕たちは自然数がどんなものかは知っているけど、あえて知らないふりをして進めていく会話が描かれています。

これを先に読んでおくと、ほう、これがあのテトラちゃんが言っていた「知らないふりゲーム」か、となったりして楽しいです。

ちなみに数学ガールは1作ごとに(つながっているところもあるが)話としては独立しているので最初から3作目を読んでも大丈夫です。

次に読みたい本

順序としては逆ですが、僕はCoPLよりも先に「型システム入門」(通称TaPL)を手に取りました。
これは主に型について学ぶための本ですが、意味論もOCamlもシークエントも知らなかった当時の僕としては、まじでわけわかめで挫折しました。

しかし、いったんCoPLを先に読むことで、難なく導入できるようになります。

この章のまとめ

つまり、まとめると以下のようになります。

この本の前に読んでると良さそうなもの

この本を読んだあとに読んでみると良さそうなもの

進め方

どういう順番で進めるのがいいか、参考程度にメモっておきます。

まずはざっくり本を読みながら概要を掴んで、「演習問題」というところまで来たら、オンライン学習システムで実際に手を動かします。

この時に、少し前に買った電子メモ帳を使うと便利でした。
ただ、中盤辺りまで進めると、記述量が膨大になるので大きさが足りなかったりします・・。

演習問題はその日読んだ章のものを少しやって終わり、日をまたいだ時に、前章の残してた問題を解くことで復習できるようにしてました。

オンライン学習システムについて

オンライン学習システムでは、用意された文法に則り、推論規則とにらめっこしながら記述していきます。
第n問の下に「導出システムこれこれを使いましょう」とあるので、それを見落とさないように注意です。

最初は、先の問題にアクセスできないようになっていますが、各章の問題を半分くらい解くと次に進めるようになります。

中盤まで来ると、1問解くのに1時間以上かかる大層なものも出てきます。
こんなのとか。

オンライン学習システムには「統計」というページがあり、ここに登録した人たちが何日かけて今何問目なのかをランキング形式で確認することが出来ます。

これはモチベーションの維持には効果的で、解くことに集中しなければという気になってしまいますが、あんまり気にせずところどころ飛ばしながら自分のペースで進めればよいのかなと思います。

(早い人は3日で160問すべて解いている人もいる)

また、これ途中経過を採点できないので、1時間かけて作った解答を提出し、「ミスってるよ」と言われたときの絶望感が半端ないです。

VSCodeのextentionを公開しました

手書きで解いていくのも良いのですが、大変そうなのでスニペットを作りながら進めました。
ニーズは薄いとは思いますがせっかく作ったのでVSCodeの拡張機能として公開しています。

【参考】copl-snippets – Visual Studio Marketplace

まだ制作段階(ver 0.0.2)で、READMEも整理されていませんが随時更新していく予定です。

拡張機能をインストールし、ファイルの拡張子を「.copl」とすれば利用できます。

最後に

この本を読もうと思ったきっかけは、型について知りたいというものでしたが、付随していろいろ学べたのは良かったです。

今まで数学の教科書に出てきた交換則とか、あたりまえやろとか思っていましたが、1章ではそれがなく苦労するところが多々あったりしました。

これが数学か、これがプログラミングか、という気にさせられる一冊でした。