これはなに?
TAPLのサンプルコードを単純化してPrologに移植したものです。
- 第Ⅰ部 型無しの計算体系
- arith 型無し算術式 bool+nat(3,4章)
- fulluntyped フル型無しラムダ計算 bool+nat+float+λ+let+record(5,6章)
- untyped 型無しラムダ計算 λ (7章)
- 第Ⅱ部 単純型
- tyarith 単純型付算術演算 bool+nat+単純型(8章)
- fullsimple フル単純型付ラムダ計算 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+単純型(9,11章)
- simplebool 単純型付ラムダ計算+bool bool+nat+λ+単純型(10章)
- fullref フル単純型付ラムダ計算+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+ref+top+bot+source+sink+単純型(13,18章)
- fullerror フル単純型付ラムダ計算+エラー bool+λ+top+bot+try error+単純型(14章)
- 第Ⅲ部 部分型付け
- 第Ⅳ部 再帰型
- fullisorec フル再帰型 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+rec+fold+unfold+単純再帰型(20章)
- fullequirec フル再帰型 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+rec+単純再帰型(20章)
- equirec 再帰型 λ+rec+単純再帰型(21章)
- 第Ⅴ部 多相性
- reconbase 型再構築のベース bool+nat+λ+単純型(22章)
- recon 型再構築 bool+nat+λ+型推論(22章)
- fullrecon フル型再構築 bool+nat+λ+let+型推論(22章)
- fullpoly フル全称型、存在型 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+all+some(23,24章)
- fullfsub フルF<: 有界量化 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+<:+all+some(26,28章)
- fullfsubref フルF<: 有界量化+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+try error+ref+top+bot+<:+source+sink+all (27章)
- purefsub 有界量化 λ+top+<:(28章)
- 第Ⅵ部 高階の型システム
- fomega +kind
- fullomega フル型演算とカインド、高階多相 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+ref+all+some+kind(29,30章)
- fullfomsub フル有界量化サブ bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+<:+all+some+kind(26,31章)
- fomsub 高階部分型付け λ+top+<:+all+kind(31章)
- fullfomsubref フル有界量化サブ+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+try error+ref+top+bot+<:+source+sink+all+some+kind+import
- fullupdate フル純粋関数的オブジェクト 書き換え可能レコード bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+top+<:+all+some+kind+variance(32章)