「プログラミング言語の基礎理論」を読む

gistfile1.md

メモです。

• Amazon: プログラミング言語の基礎理論 (情報数学講座) 単行本 – 1997/2/1

1. プログラミング言語のモデル

• 記法の定義
• 型無しラムダ計算

2. 型付きラムダ計算(Λ)

3. 型付きラムダ計算の拡張

👀 いろんな機能を足してみます

• unit(3.1) バリアント(3.1) ラベル付きデータ構造(3.1)

• 再帰的データ型(3.2)

• 再帰関数(3.3)

• ユーザ定義データ型(3.4) パターンマッチ(3.4)

• 参照(3.5) 継続(3.5)

• 3.1.1 unit : void的なやつ

• 3.1.2 バリアント型 : 直和型(union的なやつ)

• 3.1.3 ラベル付きデータ構造 : レコード・バリアントの要素にラベルを付けられるようにする

• 3.2 再帰的データ型(Λ^μ1) : List ::= Nil | (n, List)みたいに、型の定義が自分自身を含んでもよいことにする

• 3.3 再帰的関数

• 3.4 ユーザ定義型 : datatype構文を使って、ユーザ定義型(直積＋直和)を定義できるようにする

• 3.5.1 参照型(Λ^ref)

• 3.5.2 継続

4. 型推論

4.1 暗黙に型付けられたラムダ計算(λ)

4.2 λの型推論

4.3 拡張

5. 多相型言語 (Λ^∀)、ML多相(λ^let)

5.1

5.2 多相型ラムダ計算(Λ^∀)

5.3 表示的意味論

5.4 公理的意味論

5.5 種々のデータ構造の表現

5.6 MLの多相(λ^let)

6. レコード多相

6.1 背景

• フィールドX: intを持っているレコード、をまとめて扱いたい
• フィールドX: intをもつバリアント型、をまとめて扱いたい

2種類の方法がある(6.2, 6.3)

6.2 レコード計算＋部分型

6.3 多相レコード