TaPL 7章までのあらすじ
小咄
Prefaceのchaptersの依存グラフはなんかいい感じのやつで計算されてgraphvizでプロットされている。
注意
原著に基づいてるので邦訳版と異なる言葉を使っているかもしれない。
また、実装の章は飛ばすので、各位読んだり読まなかったりするように。
実装にはしばしばメタ理論としてアルゴリズムが載ってたりする。
1章 Introduction
型はすごいんやということが書いてある。
一方これらはコスパ的にまあまあ高い。プログラマも背景の論理にあんまり詳しくなかったりで使いづらい。
型システムという言葉はしばしば様々な定義が与えられるが、とりあえず以下の定義は広く賛同を得られるものである:
型システムは、計算された値の種類に応じてフレーズを分類することで、特定のプログラムの動作が存在しないことを証明するための扱いやすい構文的手法である。
deeplくんありがとう。
この定義から分かることは、まず型システムとはプログラムについて推論するツールである。さらに一般的に、型システム(または型理論)とは、ロジックの研究、数学、または哲学をも指す。研究自体は1900年代からすでに始まっており、今でも続いている。
もうひとつの重要な点として、型システムは構文による分類をおこなうというものである。
これが指している事実とは、型システムは実行時の挙動を静的に計算して近似するということである。
この静的はしばしば明示的に書かれ、"静的型付き言語"などといい、"動的型付き言語"との対比のためにしばしば用いられる。
しかし、動的型付き言語がおこなっていることは、実行時に型タグを用いてヒープ上の構造を判別するものであり、型検査とは全く異なる。
したがって、"動的型付き"という句はしばしば誤解を招くものであり、"動的検査"などに置き換わるべきである。
型システムは静的なため、必ず保守的に近似をおこなう。
型システムは"悪い"プログラムの動作が存在しないことを証明するが、存在することは証明できない。なので実行時には正しく動くプログラムもしばしばリジェクトする。様々なプログラムに可能な限り型を付けるということは、型理論の研究で永遠に続く課題である。
... あとは型注釈は証明にあたり、型検査器はproof checkerに相当するなどが書いてある。
型システムが担うことは以下
detecting errors
abstraction
interface, module signature
documentation
Haskellerがよくいってるやつ
language safety
efficiency
arityをkindで表すやつとか、最適化にも使われてるわよね
furthure applications
network secury
proof-carrying code
自動証明
メタデータ (e.g. XML)
計算言語学
2章 Mathematical Preliminaries
これからの話をするにあたって、数学(集合論の基本)のおさらいをする。
3章 Untyped Arithmetic Expressions
プログラム言語のエクササイズとして、 真偽値、 if、ペアノ数、iszero から成る小さな言語を、syntax、operational semanticsから構成する。その他構文木のサイズ、深さ、big-step/small-stepなど。 (4章 An ML Implementation of Arithmetic Expressions)
5章 The Untyped Lambda-Calculus
置換の記法 $ (\lambda x. t)\ t' \rightarrow \left[x\mapsto t'\right]t などの基本的な記法
lexical scoping、自由変数などの用語
チャーチエンコーディング
boolean
pair
numeral
再帰とは?
種々のメタ情報の計算方法
6章 Nameless Representation of Terms
変数名をforlamiseして証明に使ったりするのはダルいので名前をなくそう → de Bruijn index。
$ \lambda x. x \mapsto \lambda. 0 ... 最内のラムダ抽象から見て0番目の変数 ($ = x)
$ \lambda x. \lambda y. x \mapsto \lambda. \lambda. 1 最内のラムダ抽象から見て1番目の変数($ = x)
(7章 An ML Inplementation of the Lambda-Calculus)