TAPLを読む会(8~12章)
8章 型付け関係
NBに対して型をつけてみる。
型付け関係の逆転(逆転補題)(生成補題) 項を型付けるためのアルゴリズムを与える。(部分型とかが入ってくるとこれが大変になる…かな？)
進行性 項が正しく型付けられているなら、正規形->値(標準形)が成り立つ。
保存性 項が正しく型付けられているなら、項の評価は項の型を変えない。
これらの性質は後々でも保たれるように頑張る。
8.3.4～8.3.8のあたりの答えは考えておいたほうが理解の足しになりそう。
9章 単純型つきラムダ計算
ラムダ計算にとりあえず型をつけてみる。
9.1 関数型
関数に型をつける際に一番適切そうな型の定義は T ::= T -> T である、という話。
9.2 型付け関係
型推論をさせるには型再構築とかそのへんをする必要があるので、22章を待つ必要がある。 とりあえずはλ抽象時に型を付けることにする。(C言語とかはそうですね) 例えば、λx:Bool,λy:Nat,(if x then y else (succ y)) において、 (if x then y else (succ y))の型をつけるには、x,yの型を知っている必要があって、 そのために「型環境」という概念が出てくる。 で、T-VAR,T-ABS,T-APPが導入される。(項tの帰納的定義に対応している)
9.3 型付け関係
8.3と同じ手順ですね。
9.4 Curry-Howard対応
9.4.1が分かんねぇ…(predとsuccについて)
9.5 型消去と型付け可能性
9.5.2.(2)はわりと非自明に思える。
10章 単純型のML実装
やってねぇ…
11章 単純な拡張
Unit -> let -> pair,record -> sum,variant -> fix -> List の順番で導入する。 プログラミング言語を実装している感じ。
11.1 基本型
簡便のため基本型Aを導入する。まああんま使わない。 ちゃんとした恒等関数とか二回適用関数を作るには、「自由な型を代入できる」23章の全称型を待つ必要がありますね。
11.2 Unit型
11.3 派生形式 : 逐次実行とワイルドカード
派生形式の例として逐次実行を導入する。 糖衣構文(もしくはマクロ)かそうでないかという話。
11.4 型指定
部分型付けをする際にちらっと出てくる(p151とか)のでその伏線ですね。
11.5 let束縛
T-LETを使って導出する際は、T_1をエスパー(まあ分かるのだけれど)して導かないといけない。 第22章のlet多相では、これを利用して多相型を表現したりする。(というかこの時点で多相型を表現できていそう)
11.6 二つ組
11.7 組
11.8 レコード
『組を作る操作』と『射影を作る操作』を付け加える。 二つ組は添え字が1と2, 組は1～n, レコードは更に自由になる。
11.9 和
11.10 レコード
『和に埋め込む操作』と『タグと値を取り出す操作』を付け加える。 case文で値を取り出す際にはどのケースも同じ型を返す必要があるのは if文とかと同じ感じですね。
で、これの型チェックをうまくさせるために、 1. 型推論(型再構築)(22章まで) 2. 部分型関係(15章) 3. 型注釈(asによる) という手がある。 とりあえずは3でやっている。 (T-INLとT-INRは部分型関係を予感させる書き方ですね…)
レコードを使うことにより、 ・オプション(Haskellのmaybeっぽいもの) ・列挙型(C言語のenum) ・単一フィールドのバリアント(typedefですかね)
11.11 一般的再帰
fixは派生形式として導入できない!! また、値を持たない、発散する項が作れる。 (停止性を犠牲にして計算能力を獲得する) letrec(再帰的定義)はfixを用いることによりから派生形式として得られる。
11.12 リスト
fixが入ったのでリストも派生形式として定義できる…気はするけれども、 今回は新しく導入されている。(23章を待て)
12章 正規化
単純型付きλ計算のすべての項は正規化可能である!!
