TaPL
https://gyazo.com/700ecc8fd508c11c0f20e1bc68285e23
サポートページ
実装
公式
手を動かして厳密に読もうとするとものすごい時間がかかって永遠に読み終わらない気がするので、もうちょい雑に読んでみても良いのかもしれないmrsekut.icon
ちゃんと読んでないがこれ見ると良いかもmrsekut.icon
TaPL翻訳の裏側
1章 はじめに
2章 数学的準備
第1部 型無しの計算体系
第3章 型無し算術式
第4章 算術式のML実装
第5章 型無しラムダ計算
第6章 項の名無し表現
第7章 ラムダ計算のML実装
第2部 単純型
第8章 型付き算術式
第9章 単純型付きラムダ計算
第10章 単純型のML実装
第11章 単純な拡張
第12章 正規化
第13章 参照
第14章 例外
第3部 部分型付け
第15章 部分型付け
ちゃんと読んでないmrsekut.icon
第16章 部分型付けのメタ理論
第17章 部分型付けのML実装
第18章 事例：命令的オブジェクト
第19章 事例：Featherweight Java
第4部 再帰型
第21章 再帰型のメタ理論
第5部 多相性
第22章 型再構築
一部または全部の型注釈がない項の主要型を求めるアルゴリズム
第23章 全称型
第24章 存在型
第25章 System F のML実装
第26章 有界量化
第27章 事例：命令的オブジェクト再考
第28章 有界量化のメタ理論
第6部 高階の型システム
第29章 型演算子とカインド
第30章 高階多相
第31章 高階部分型付け
第32章 事例：純粋関数的オブジェクト
付録A 演習の解答
付録B 記法
3章 型なし算術式
表記
項: $ \tau
bool値、数値(succ, pred, iszero)を表す
項の集合: $ \mathcal { T }
集合Sはこれらの全ての組み合わせを表す: $ S = \bigcup _ { i } S _ { i }
多ステップ評価関係
*を使う
$ t\rightarrow {}^*t'.
項$ tを複数回簡約すると項$ t'が得られる
ここからわかるのは通常の$ \rightarrowは1回の簡約を示すのか？
4章 実装
Termの定義と簡単なevalの実装
代入の際に変数名がかぶるやつ
ちゃんとした説明は p.53
読了2020/5/17
6章 項の名無し表現
一応読了2020/5/31
7章 実装
未読
8章 型付き算術式
ある式への型の付け方は一意である
一応全部読んだ2019/10/6
とちゅう2019/10/6
10章 実装
未読
11章 単純な拡張
未読
12章 正規化
未読
13章 参照
未読
14章 例外
未読
16章 部分型付けのメタ理論
未読
17章 実装
未読
18章 命令的オブジェクト
未読
未読
未読
未読
p.273~
25章 実装
未読
未読
27章 命令的オブジェクト再考
未読
28章 有界量化のメタ理論
未読
未読
未読
31章 高階部分型付け
未読
32章 純粋関数的オブジェクト
未読
転がってた資料
実装
elmで