読者です 読者をやめる 読者になる 読者になる

数学初心者のための「型システム入門」入門

book

社内で「TaPLで殴りあう会*1」が開催されるというので、型システム入門(通称TaPL: Types and Programming Languages)を購入したものの、内容が難しくて序盤からまったくと言っていいほど読み進めることができませんでした。

型システム入門 −プログラミング言語と型の理論−

型システム入門 −プログラミング言語と型の理論−

  • 作者: Benjamin C. Pierce,住井英二郎,遠藤侑介,酒井政裕,今井敬吾,黒木裕介,今井宜洋,才川隆文,今井健男
  • 出版社/メーカー: オーム社
  • 発売日: 2013/03/26
  • メディア: 単行本(ソフトカバー)
  • クリック: 68回
  • この商品を含むブログ (7件) を見る

しかし、読めないままにしておくのは悔しいし、内容はとても面白そうなので、やはりちゃんと読めるようになりたい。
そこで基礎的な書籍とWebで情報収集してから再度挑戦したところ、なんとか読み進められるようになりました。

監訳者さんによると、序盤のいくつかの章と中盤以降の好きな章を読めば読んだことになるらしいので、ここでは11章までを読むために必要になった知識をまとめてみたいと思います。

準備

本書の序文には、以下のような前提知識が必要だと書かれています。

型システム入門を読み始める前に、これらの知識のうち不足しているものを補う必要があります。
僕は数学の知識に不安があったので、何冊か本を買って読むことにしました。

数学

最初はどういった数学の知識が必要になるのか分からなかったので、まず、ラムダ計算の勉強のしかた、プログラム意味論 - きしだのはてなを参考にして、論理学の本を読むことにしました。

「入門!論理学」は、一切記号を使わず論理学を説明していて非常に分かりやすい内容です。論理学の背景も解説してあって読み物としても面白い。ただ、導入としてはとてもよいのですが、型システム入門を読むための知識としてはちょっと足りないかな。

入門!論理学 (中公新書)

入門!論理学 (中公新書)

続いて「論理学」を読みました。「入門!論理学」と同じ著者の書籍ですが、こちらは記号も証明もきっちり出てきます。「入門!論理学」を読んでおくと構成が似ているので理解しやすいですね。

論理学

論理学

集合論についてもう少し理解したかったので、「ろんりと集合」も読んでみましたが、1つ1つの説明が薄いのでしっかり学びたい場合にはものたりないかも。また、内容とほとんど関係のないダジャレや先生と学生の会話がでてきたり、注釈がやたらと多くて章末にまとまっていたりして、ちょっと読みにくかったです。

離散数学に関しては、不足している知識を「離散数学―コンピュータサイエンスの基礎数学 (マグロウヒル大学演習)」で確認するくらいで十分だと思います。
もう少し学びたいのであれば、プログラムの動かし方の本 - きしだのはてなを参考に書籍を探してみるのがよさそうです。

あとは、型システム入門の内容に直接関係するわけではないのですが、「圏論勉強会」に参加した*2ことで、集合論や証明の手順などの理解の助けになりました。
資料と動画が公開されているので興味がある方は見てみるとよいかと思います。(1回2時間なので全部見るのは大変です)

高階関数プログラミング言語

本書は関数型プログラミング言語の知識を前提として解説が進むので、何かしら関数型プログラミング言語を知っておく必要があります。
サンプルプログラムはOCamlで記述されていますが、他の関数型言語(F#, Haskell, Scalaなど)しか知らなくても問題ありません。いずれかの言語の入門書レベルの知識があれば十分です。

また、本書を読みながら、サンプルプログラムを写経するか、自分の好きな言語で実装してみることをおすすめします。理解がぐっと深まります。
ちなみに僕はF#とFParsecを使ってコードを書いてます。

実践 F# 関数型プログラミング入門

実践 F# 関数型プログラミング入門

あとは、自分の実装の答え合わせをするために、OCamlのサンプルプログラムも動かせるようにしておくとよいですね。

コンパイラの基礎的な概念

コンパイラの知識としては、抽象構文木BNFなど、基本的なところさえ押さえておけば大丈夫です。

おすすめの書籍は思いつかないので、Webの入門記事を読むくらいで十分だと思います。「言語実装パターン ―コンパイラ技術によるテキスト処理から言語実装まで」でもいいかもしれませんが、この本は理論が少なめで実践的な内容で、型システム入門では使わないような高度な内容も出てくるので、ちょっと違うかも。

また、サンプルコードを書く際には書籍で定義された構文をパースしないといけないので、何らかのパーサジェネレータかパーサライブラリも使えるようになっておく必要があります。
サンプルコードはocamllex/ocamlyaccを使っていますが、lex/yacc系以外のものでも問題ありません。

第3~4章

準備が終わったらさっそく読み進めていきましょう。第2章は飛ばしてしまって構わないと思います。

で、3章から読み始めていくわけですが、ここをきっちり理解しようとすると難しくてくじけてしまうかもしれません。
なので、いまいち分からないところがあったらいったん飛ばして、4章で実装をしてから3章に戻ってくるといいと思います。
1ステップ評価と多ステップ評価がおおよそ分かれば大丈夫。

なお、実装の説明の中で抽象構文木のノードにinfo型が出てきます。これはパースエラーが発生したときの位置情報を格納するための注釈です。パーサの種類によっては不要なものなので、実装するときには無視してしまいましょう。

第5~7章

序盤の山場ですね。ラムダ計算、De Bruijnインデックス、シフト、代入など難しい概念がたくさんでてきますが、これらの概念はこの章以降もずっと使うのでしっかりと理解しておく必要があります。

ラムダ計算については「論理と計算のしくみ」が良書ということで買ってみましたが、この本もなかなか難しい。というわけで、下記のリンク先の記事をおすすめします。

僕は上記リンクの「ラムダ計算の基礎」の記事をいくつか読むことでなんとか理解できました。
ラムダ計算は読むだけではなかなか理解できないので、Church数の足し算や掛け算なんかは実際に手を動かして解いてみるのがよいと思います。

他には、ラムダ計算という言葉は出てこないものの「プログラミング言語の基礎概念」は、型システム入門と同じような内容を非常に分かりやすく解説しています。併読することで非常に理解が進みました。
オンラインの演習システムも用意されていて、パズル感覚で学べるのが楽しいですね。

プログラミング言語の基礎概念 (ライブラリ情報学コア・テキスト)

プログラミング言語の基礎概念 (ライブラリ情報学コア・テキスト)

7章まで進むと構文も少し複雑になってきます。僕は関数適用をうまくパースできなくて悩みました。ParsecやFParsecを使っているときは左再帰が解決できないので、chainlを使うといいみたいです。

第8~11章

ここまでくるとようやく型がでてきます。長かった〜(笑)
第8~11章では、特に新しい知識が必要になることはないように思います。

8章と10章は、4章と7章の実装に型を追加するだけなので、さくっと実装してしまいましょう。

9章は型の一意性と型安全性の定理および証明の解説です。定理自体はそんなに難しくないと思うのですが、証明を追いかけるのがつらい。証明は飛ばしちゃってもいいんじゃないかな・・・

11章では、これまでのプログラムにタプルやレコード、パターンマッチ、バリアントなどの構文を追加します。
パーサを書くのが大変ですが、だいぶプログラミング言語らしくなってきて楽しいですね。

俺達の型システム入門はこれからだ

11章まで読み終わったら、序章にある各章の依存関係グラフを参考にして、興味のある章へと進んでいきましょう。
部分型、再帰型、多相性、高階型などなど面白そうな内容ばかりですね。まだまだ先は長い。

*1:読書会です

*2:僕は第7回で脱落してしまいましたが