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