おいお前ら、TAPL読むぞ!

こんにちは。VOYAGE GROUP エンジニア blog Advent Calendar 最終日分の記事です。

TAPL(Types and Programming Languages, 型システム入門)を一緒に読もうよという内容になります。

アドベントカレンダー最終日、クリスマス・イブだからおもしろネタ記事かと思った?残念!型システムでした! クリスマスだからって浮かれているようではエンジニアとして生き残れないですぞ!(弊社では社内バーでクリスマスにビールを飲んだり楽器を鳴らしたりしてワイワイする voyarock という会がありますので、興味ある方はぜひ参加してみてください https://atnd.org/events/59995

あと、ネタ枠は Slack で役に立たない Bot を運用するときの知見とか - ミントフレーバー緑茶 で勘弁して下さい。

社内読書会について

VOYAGE GROUP では技術書の読書会がいくつかあります。今年参加した/しているものをリストアップしてみると

  • SQLアンチパターン勉強会
  • ハイパフォーマンス ブラウザネットワーキング輪読会
    • 今年の前半に @hagino3000 中心で輪講会がありました
    • モバイルアプリケーションの最適化など色々な分野にまたがっていて、参加者の傾向がバラけていていい感じだった
    • 参考: http://hagino3000.blogspot.jp/2014/08/hpbn.html
  • SICP(Structure and Interpretation of Computer Programs, 計算機プログラムの構造と解釈)輪読会
    • プログラムの動作原理を学べる非常に面白い本
    • 問題を解いていきながら丁寧に理解していく輪読会で、2 年以上掛かかりましたが最近終わりました
    • 2 年掛かってもついてくる人がいるのは、@ajiyoshi のサポートあってこそ
    • 参考: http://d.hatena.ne.jp/ajiyoshi/20121226/1356493118
  • PRML(Pattern Recognition and Machine Learning, パターン認識機械学習)輪読会
    • @a_macbee を中心に最近始まりました
    • 難しいけれどデータ解析周りに興味がある人が多いのか、結構人気(未検定)

と、自分の感覚では質の高い勉強会が開催されています。

最近では上記の勉強会に加えて TAPL 勉強会という、型システムを学ぼうという勉強会を毎週月曜日にやっています。 最初は輪読会のように TAPL のある章を読んで解説するという進め方をしていたのですが、最近の参加者は 2, 3 人で、その少人数で気合入れて資料作ってきてもねぇという雰囲気になり、今はもくもく会の体をとっています。各自で TAPL を好きなように読んで、何かトピックがあればそれについて話すという形です。

以降では TAPL を読む理由や、現在までに自分が 10 章まで読んで学んだことを書きます。取っ付き辛そうと思っている方や、ちょいと割高なので二の足を踏んでるから雰囲気を知りたいと思っている方の参考になったらと思います。

TAPL とは・何が学べるのか

TAPL は型システムについて詳しく解説された本です。動的型付けや静的片付けに関係なく、プログラマなら普段お世話になっている方も多そうな型システムについて理解を深めることができます。

参考: 書評「型システム入門」 - あどけない話

自分が 10 章まで読んで学んだことを箇条書きでまとめると

  • 型システムで解決できること
    • 型の無い場合はどのような不都合があるのか
  • 型無し・型ありラムダ計算器の実装
    • 入力のパース・構文解析・評価・表示という一連の流れを Haskell で実装する方法
      • せっかく少しずつ学んでいる Haskell の利用機会があって良かった(TAPL での実装は OCaml で書かれている)
    • 型検査器の実装

どういう流れで TAPL を読んでいるか・オススメの読み方

最初は1章・2章・3章…と順番に読んでいましたが順番に読んでいると、証明がよく分からない!自分の頭の悪さよ!!辛い!!!という事態になりがちです(少なくとも自分は)。10 章までの流れだと、定義や証明の多い理論の章=>理論の実装という流れになっており、理論ベースの章に書いてあることを完璧に把握しながら進めるのは難易度が高いかと思います。

幸い実装の章があるので、手を動かしながら全体をゆっくり把握していく学び方が性に合っている方は理論の章を斜め読みした後、実装の方を先にやって、分からないがあったら戻るというやり方がオススメです。実装の章はXXのML実装と書いてある章になるかと思います。

ただし、7 章最後の脚注に「実装したからといって、理解したとは限らない -- Brian Cantwell Smith」とあるように、実装しながら理解すると理解したつもりになって実は間違った理解をしていたとか、実装には現れない部分があったなど「TAPL 完璧に理解した」という状況にはなれないことは気をつけておきたいですね。とはいえ難しい問題や証明があるので、そこで足踏みしたり挫折するなら先に行った方が良い。もしくは「TAPL 完璧に理解した」人に焼き肉を奢ってさっさと教えを請う方が良い(自分の周りには「TAPL 完璧に理解した」人はいないのですが、頭の良い人が多いのが救い)。

各章について(10 章まで)

自分の読んだ 10 章までに書いてある事をまとめます。こっからは個人のチラ裏メモレベルの殴り書きで、TAPL の雰囲気を感じてもらえたらと思います。興味ないとかネタバレ嫌だという方は一気にまとめまで。

1 章 はじめに

TAPL における型システムの定義や、型システムがもたらすものについて書かれている。

型システムとは、プログラムの各部分を、それが計算する値の種類に沿って分類することにより、プログラムがある種の振る舞いを起こさないことを保証する、計算量的に扱いやすい構文的手法

  • 1.1 節「計算機科学における型」より

    • プログラムが想定外の振る舞いをしないよう、評価前に検査する仕組みという理解でいる
  • 型システムがもたらすものとして書かれているのは

    • エラーの検出
    • 抽象化
    • ドキュメント
    • 言語の安全性
    • 効率性

2 章 数学的準備

  • 後から分からない部分が出てきたらここで調べる(飛ばした)

3 章 型無し算術式

  • 小さな言語を定義することで、構文や評価の表現方法について学ぶ
  • 評価は t という状態を t' へ進めると表現できる
    • 1 回だけ評価する関係を 1 ステップ評価関係といい (t -> t') で表せる
  • もうこれ以上評価できないという状態の項を正規形と呼ぶ
    • 正規形は true/false や数値のような値である場合と、値ではないが評価できない場合がある
    • 後者は「行き詰まり状態」であり、数値に1を加えるような関数 succ (後者関数) に false を適用したもの succ(false) は、3章で定義された構文では次にどういう状態になるべきか定義されていない
    • 行き詰まり状態を実行時エラーとして表すことができる

4 章 算術式の ML 実装

  • 型無し算術式を OCaml で実装する
    • データの構造による条件分岐が多く、パターンマッチのある言語だと実装しやすい
      • 自分は Haskell で書いているが、Rust で書いている @rail44 もいる
    • 評価器だけで良ければ基本的には定義をそのままプログラムに落としこんでいくだけだが、「ファイル I/O -> 字句解析 -> 構文解析 -> 評価 -> 表示」を行う機能が無いとインタプリタとして使用できない

5 章 型無しラムダ計算

  • ラムダ計算は関数定義と関数適用を関数だけで表現する
    • 項は 3 種類
      • 変数 x
      • ラムダ抽象 λx.t
      • 関数適用 t t
    • 例えば、引数をそのまま返すような関数 id への関数適用 id z は (λx. x) zと表現できる
  • ラムダ計算は単純ながら、色々な計算を表現できて強力である

    • カリー化による複数引数を取る関数の表現
    • Church ブール値 true = λt. λf. t
    • 2つ組
    • Church 数
      • 0 の表現 C0 = λs. λz. z
      • 1 の表現 C1 = λs. λz. s z
      • 後者関数 s を 0 の表現に何回適用したかで n を表す
    • 他にも test (if を表現する)、足し算、掛け算、iszero、不動点コンビネータ
    • 表現力はあるけどパズルみたいな複雑さがあって、よくもまあ定義したなあと思う
      • (λm. λn. λs. λz. m s (n s z)) (λs. λz. s z) (λs. λz. s (s z)) が1+2 を表してます!というのは自分で考えつく気がしない
  • 後は代入の形式的定義など

6 章 項の名無し表現

  • 主に変数の取り扱いについて書かれており、TAPL のラムダ計算では de Bruijn インデックスを用いる
  • de Bruijn インデックス
    • k 番目に束縛されたときの番号を変数名として利用する
    • そもそもなぜこのような名無し表現が必要かというと、変数に名前を付けた場合名前の重複があると実装上ではどの変数(名前無し)を指しているか分からない
  • シフトと代入
    • 代入が入ると自由変数だった変数が束縛された場合、インデックスの付け替えが生じる
    • また、評価(簡約)の場合は変数が消費されるので、これまたインデックスの付け替えが生じる

7 章 ラムダ計算のML実装

8 章 型付き算術式

  • やっと型が出てくる

    • 4 章で実装した算術式を静的な型で強化する
    • 項を評価する前に「行き詰まり状態」にならないかチェックできる
  • 型システムの最も基本的な性質は安全性

    • 正しく型付けされた項はおかしくなることがない
    • おかしくなるとは行き詰まり状態になること
  • 行き詰まり状態にならないことを進行定理と保存定理によって証明する

    • 進行: 正しく型付けされた項は行き詰まり状態ではない
    • 保存: 正しく型付けされた項が評価できるならば、評価後の項も正しく型付されている

9 章 単純型付きラムダ計算

  • ラムダ抽象に型がつく
    • (λx:Bool. x) :Bool->Bool
    • Bool を引数にとり、Bool を返す
  • 進行と保存の証明とかは長いので飛ばした

10 章 単純型のML実装

*Main> run "^x:Bool. x"

"(^x:Bool. x) : Bool->Bool"

Bool->Bool を期待されているのに true が引数なので怒られる例。

*Main> run "(^x:Bool->Bool. ^y:Bool. y) true"

"*** Exception: parameter type mismatch

*Main> run "(^x:Bool->Bool. ^y:Bool. y) (^k:Bool. k)"

"(^y:Bool. y) : Bool->Bool"

まとめ

  • 弊社には良質な読書会がある
  • TAPL を僕と一緒に読もう!
    • 人数が少ないので、社内の方でも社外の方でも興味があればぜひ
  • クリスマスだからって浮かれているようではエンジニアとして生き残れない(弊社では社内バーでクリスマスにビールを飲んだり楽器を鳴らしたりしてワイワイする voyarock という会がありますので、興味ある方はぜひ参加してみてください https://atnd.org/events/59995

VOYAGE GROUP エンジニア blog Advent Calendar 最終日の記事でした!楽しいクリスマスを!