レコードによる構造記述

基本概念はレコード型とレコードインスタンスとレコードのアプライだけでなんとかなるのでは？

1. レコード型は、{name1 : type1; ..., nameN : typeN; } の形
2. レコードインスタンスは、{name1 := val1; ...; nameN := valN; } の形
3. 未割り当て型宣言と値割り当てが混じったレコードを抽象レコードと呼ぶ。

抽象レコードがあるとき、未割り当て型宣言だけを抜き出したレコード型をパラメータ型と呼ぶ。すべての型宣言を取り出したレコード型をリザルト型と呼ぶ。抽象レコードは、そのレコードのパラメータ型からリザルト型への関数だと考えられる。

特に、レコード型は、それ自身がパラメータ型でありリザルト型でもある。レコードインスタンスは、パラメータ型が{}で、リザルト型はそのレコードの型になる。したがって、レコード型を入れた型付きラムダ計算があれば、抽象レコードを説明できる。

ラムダ引数は λ{a:A; b:B}.T のようになる。

事例：

define PointedSet := {
 set: Set;
 base: set
}

書き換えると：

define PointedSet := λ{set: Set; base: set}.{ set := set; base := base}

書き換えた抽象レコードは、レコード型のコンストラクタになる。

以上はインスタンス化、他にレコードのサブタイプ化も必要だろう。