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

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章 正規化

単純型付きλ計算のすべての項は正規化可能である!!