前章では、オブジェクト指向プログラミングの主要な機能を、部分型付けとレコード、参照を持つラムダ計算を用いてモデル化した。
本章では、別アプローチとして組み込みのオブジェクトを定義する。

プログラミング言語のような人工物を形式的にモデル化することによる利点

• 設計の正確な説明となる
• ある性質を記述・証明できるようになる

しかし、モデル化には「完全さ」と「コンパクトさ」の間で葛藤がある。

Featherweight Java (FJ)は、Javaの型システムをモデル化するために最低限必要な計算体系を定義したものである。
FJ は、執拗といえるくらいに「完全さ」より「コンパクトさ」を重視している。（項には５つの形式しかなく、破壊的代入さえも省略されている。）

他の性質

• 全てのFJプログラムは、そのままJavaプログラムとして実行可能であり、直接的な対応関係があるといえる。
• FJ の主な応用は、Javaの拡張機能をモデル化すること。「コンパクトさ」のおかげで、拡張の本質的な側面に集中して考えることができる。

以下に、FJの典型的なクラス定義を示す。
class A extends Object { A() { super(); } }

class B extends Object { B() { super(); } }

class Pair extends Object {
  Object fst;
  Object snd;
  
  Pair(Object fst, Object snd) {
    super();
    this.fst = fst;
    this.snd = snd;
  }
  Pair setfst(Object newfst) {
    return new Pair(newfst, this.snd);
  }
}

文法規則は後の節で示されるが、レシーバが this の場合であっても省略禁止などの制約がいくつかある。
破壊的代入が禁止されているため、コンストラクタは代入'=' が現れる唯一の場所である。

項の形は５つしかない。

• オブジェクトコンストラクタ
  例：new A(), new B(), new Pair(...)
• メソッド呼び出し
  例：Receiver.setfst(...)
• フィールド参照
  例：this.snd
• 変数
  例：newfst, this
• キャスト
  例：X = new Pair(new A(), new B()), Y = new A() としたとき
  ((Pair)(new Pair(X, Y).fst).snd)
  fstフィールドはObjectと定義されているので、キャストが必要。

それぞれラムダ計算と対応づけることができるが、いくつか重要な違いがあり、その違いを実現するために別の処理が必要である。

• メソッドオーバーライド
  どのメソッドを呼び出すべきかを、レシーバのクラスが決定する
• selfを介した「オープンな再帰」
  メソッドを呼び出す前にthisにレシーバを代入
• キャスト
  対象のオブジェクトの実行時のクラス が キャスト先のクラス のサブクラスであるかを確認
  (1) サブクラスならば、キャストが取り除かれる
  (2) そうでないなら、計算は行き詰まり状態になる。これは実行時エラーをさす。

計算を行き詰まり状態にしてしまう方法は３つある。

• クラスに宣言されていないフィールドを参照する
• クラスに宣言されていないメソッドを呼び出す
• オブジェクトの実行時のクラスのスーパークラス以外の何かにキャストする

正しく型付けを行えば、最初の２つが起きないことは証明することができる。
また、プログラムがダウンキャストを含まず、かつ正しく型付けされているときは、３つ目も起きないことを証明できる。

ここでは、標準的な値呼び評価を用いる。

FJ と、型付きラムダ計算との基礎的な様式の違いについて述べる。
この違いとは、型名の立ち位置に関することである。

本章以前では、可読性のため、長く複合的な型に短い名前をしばしば定義した。

NatPair = { fst:Nat, snd:Nat };

このような定義は表面的なものである。
名前はただの省略形で、この２つはすべての文脈で相互に置き換え可能である。

一方、Javaでは、型定義がずっと重要な役割を果たす。

Java プログラムで用いられる複合的な型は全て名前を持つ。
ローカル変数、フィールド、メソッドの仮引数を宣言するときは、必ず名前を与える必要がある。
その場面で、{ fst:Nat, snd: Nat }のような「裸」の型を書くことはできない。

これらの型名は、Java の部分型関係において、重要な役割を果たす。
新しいクラスを定義するには新しい名前を導入する必要があるし、extends するクラス名はプログラマが明示的に宣言する。
もしある名前が他の名前の部分型になると宣言されていないなら、それは部分型ではない。

• Java のように、名前が重要で、部分型関係が明示的に宣言される型システムを名前的という。
• 名前が本質的でなく、部分型関係が型の構造上で定義される型システムを構造的という。

名前的型システムが持つ利点

• 実行時の各オブジェクトに「型を表すデータ」へのタグがついており、その型のデータは、直接の上位型へのポインタを保持している。
  → 実行時型検査（instanceOf 検査、ダウンキャスト操作など）に有用
  
  
• List の定義の中で List を参照するのは他の型を参照するのと同じ。型名の集合は最初から与えられているものとみなす。
  → 「どちらが先に定義されたか」という問題が起きず、再帰型 を直感的に説明できる
  
  
• プログラマにextends, implements を明示的に宣言させる
  → ある型が他の部分型かどうかを自明に検査できる
  
  
• 「偽の包摂関係」を防止できる

一方で、プログラミング言語の研究論文のほとんどは、構造的型システムに関心がある。

理由（１）
少なくとも再帰型がなければ、構造的型システムのほうが少し整然・洗練されている。
構造的なほうでは、型式は独立したものとなり、型式の意味を理解するために必要な情報が備わっている。
対して、名前的型システムでは、型名とその定義についてのテーブルを常に扱う必要があり、そのせいで定義も証明もより冗長となってしまいがち。

理由（２）
研究論文が目を向けがちな、より発展的な機能（パラメータ多相、抽象データ型、ファンクタなどの型抽象に関する強力な仕組み）が、構造的型システムと相性が良い。
対して、そういう機能は、名前的型システムとはあまり相性がよくない。例えば、List(T)のような型は複合的な型であり、原始的な名前として扱うことができない。List(T)の挙動を見るには、Listの定義を参照する必要がある。

注釈

• メタ変数 A, B, C, D, E はクラス名
• f, g はフィールド名
• m はメソッド名
• x は仮引数名
• s, t は項
• u, v は値

★ 構文

• <f> は f1, ..., fn の略記
• <C f> は C1 f1, ... , Cn fn の略記
• <C f;> は C1 f1; ... Cn fn; の略記
• this.<f> = <f> は this.f1 = f1; ... this.fn = fn; の略記
• <M> は M1 ... Mn の略記
• 宣言された名前は、重複してはいけない

CL	::=	class C extends C { <C f;> K <M> }		クラス宣言
K	::=	C(<C f>) { super(<f>); this.<f> = <f>; }		コンストラクタ宣言
M	::=	C m(<C x>) { return t; }		メソッド宣言
t	::=	x	変数	項
		t.f	フィールドアクセス
		t.m(<t>)	メソッド呼び出し
		new C(<t>)	オブジェクト生成
		(C) t	キャスト
v	::=	new C(<v>)	オブジェクト生成	値

★ 部分型付け

C <: C

C <: D D <: E C <: E

CT(C) = class C extends D { .. } C <: D

※ コンストラクタ引数は、インスタンス変数とちょうど同じ数だけでなくてはならない。
※ 完全な Java では、スーパークラスのコンストラクタが引数を受け取る場合のみ、スーパークラスのコンストラクタの呼び出しが必須

クラス表 CT は、クラス名 C から クラス宣言 CL への写像である。
クラス表は、以下の健全性条件を満たすものと仮定する。
略

全てのクラスは extends で宣言されたスーパークラスを持つ。
ここでは、Object を特別なクラスとして扱い、クラス表の中に定義が現れない特別なクラス名とする。

演習 19.4.1.
S-Top 規則のように、Object がすべてのクラスの上位型であることを述べた規則はここでは必要ない。なぜだろうか。

	S-TopUnused
C <: Object

解答）
クラス宣言で必ず extends D を書かなければいけないので、上位型をたどっていけば、いつかは Object で止まる。あとは部分型付けの推移律を使えよいかからら。


補助的な定義

型付け規則と評価規則のために、補助的な定義をいくつか定める必要がある。

• クラス C のフィールドの列を fields(C) と書く。スーパークラスで宣言されているフィールドを含む。
• クラス C のメソッド m の型を、mtype(m, C) と書く。
• クラス C のメソッド m の本体を mbody(m, C) と書く。
• 述語 override(m, D, <C> → C0) は、引数の型が<C>で、結果の型が C0 であるメソッド m を D のサブクラスに定義可能かどうかを判断する。

★ フィールドの探索

fields(Object) = φ

CT(C) = class C extends D {<C f;> K <M>} fields(D) = <D g> fields(C) = <D g> + <C f>

★ メソッドの型の探索

CT(C) = class C extends D { <C f;> K <M> }	B m (<B x>) { return t; } ∈ <M>
mtype(m, C) = <B> → B

CT(C) = class C extends D { <C f;> K <M> }	m は <M> の中で定義されていない
mtype(m, C) = mtype(m, D)

★ メソッド本体の探索

CT(C) = class C extends D { <C f;> K <M> }	B m (<B x>) { return t; } ∈ <M>
mybody(m, C) = (<x>, t)

CT(C) = class C extends D { <C f;> K <M> }	m は <M> の中で定義されていない
mbody(m, C) = mbody(m, D)

★ メソッドの正当なオーバーライド

mtype(m, D) = <D> → D0 ならば <C> = <D> かつ C0 = D0
override(m, D, <C> → C0)

評価

標準的な値呼び操作的意味論を用いる。
評価器の正常終了の結果となりうる値は、new C(<v>) という形の、完全に引数の評価されたオブジェクト生成の項である。

fields(C) = <C f> E-ProjNew (new C(<v>)).fi → vi

mbody(m, C) = (<x>, t0) InvkNew (new C(<v>)).m(<u>)

C <: D E-CaseNew (D)(new (<b>)) → new C(<v>)

t0 → t0'	E-Field
t0.f → t0'.f

t0 → t0'	E-InvkRecv
t0.m(<t>) → t0'.m(<t>)

ti → ti'	E-InvkArg
v0.m(<v>, ti, <t>) → v0'.m(<v>, ti', <t>)

ti → ti'	E-NewArg
new C(<v>, ti, <t>) → new C(<v>, ti', <t>)

t0 → t0'	E-Cast
(C)t0 → (C)t0'

型付け

「愚かな」キャストの導入 (C) D

• アップキャスト：D <: C の場合　例：(Object) (new A())
• ダウンキャスト：C <: D の場合　例：(A) (new Object())
• 愚かなキャスト：D と C が無関係の場合

Java コンパイラは愚かなキャストを含む項を、正しく型付けされないもとして拒否する。
しかし FJ では、小ステップ意味論の型保存定理として型安全性を定式化する以上、愚かなキャストを認める必要がある。これは、愚かなキャストを含まない項が愚かなキャストを含む項に簡約されることがあるからである。

(A)(Object)new B() → (A)new B()

このため、前提部に愚かなキャストの性質を含めた規則 T-SCast を定義している。
FJ の型付けが正しい Java の型付けに対応するのは、この規則を除いたときのみである。

M OK in C という形式は、「メソッド宣言 M は、それが C の中にあるなら正しい」と読む。メソッド本体の中に現れ売る自由変数は、メソッドの仮引数と this のみである。

CL OK という形式は、「クラス宣言 CL は正しい形式をしている」と読む。

x : C ∈ Γ	T-Var
Γ├ x : C

Γ├ t0 : C0	fields(C0) = <C f>	T-Field
Γ├ t0.fi : Ci

Γ├ t0 : C0	mtype(m, C0) = <D> → C	Γ├ <t> : <C>	<C> <: <D>	T-Invk
Γ├ t0.m(<t>) : C

Γ├ <t> : <C>	<C> <: <D>	T-New
Γ├ new C(<t>) : C

Γ├ t0 : D	D <: C	T-UCast
Γ├ (C)t0 : C

Γ├ t0 : D	C <: D	C != D	T-DCase
Γ├ (C)t0 : C

Γ├ t0 : D	C !<: D	D !<: C	愚かさの警告	T-SCast
Γ├ (C)t0 : C

<x> : <C>, this : C ├ t0 : E0	E0 <: C0	CT(C) = class C extends D { ... }	override(m, D, <C> → C0)	T-Method
C0 m (<C x>) { return t0; } OK in C

K = C(<D g>, <C f>)	{ super(<g>); this.<f> = <f>; }	fields(D) = <D g>	<M> OK in C	T-Class
class C extends D { <C f;> K <M> } OK

演習 19.4.2.
FJ は Java のサブセットであるので、FJ プログラムは正しく型付けされているときのみ 正しく型付けされた Java プログラムになることが要求されている。
仮にこの要求を捨てて、単に Java 風の核となる計算体系が欲しいとき、設計をどのように考えるだろうか。

解答）
キャストの三つの型付け規則を１つにまとめて、愚かなキャストの概念を捨てるなど。

Γ├ t0 : D	T-Cast
Γ├ (C)t0 : C

演習 19.4.3.
破壊的代入は計算体系の基本を大きく変えることなく追加せよ。13章の参照の扱い方を参考にするとよい。

解答）
省略


演習 19.4.4.
14章の例外の扱い方を参考にして、Java の throw, try のようなもので FJ を拡張せよ。

解答）
省略


演習 19.4.5.
完全な Java と同様、FJ では型付け関係をアルゴリズム的な形式で表現していて、包摂関係はない。今ある規則の代わりに、包摂規則を導入して型システムをより宣言的に形式化しなおせるだろうか。

Γ├ t : S	S <: T	T-SUB
Γ├ t : T

解答）
例えば、Γ├ new A() : A, A <: Object が成り立つとき、T-SUB 規則を導入すると Γ├ new A() : Object が成り立つが、これは今の規則体系と相容れない。代わりに、規則 T-UCast より Γ├ (Object)new A() : Object のようにキャスト表現をつけたものが成り立つ。

包括規則を入れて宣言的な定義に形式化しなおすと、健全性が保てなくなるのでは？


演習 19.4.6.
Java のインターフェースはメソッドの型を指定するが、実装は持たない。また、クラス継承と違い、任意の数のインターフェースを実装することができる。
型付け可能な項に対して最小の型を与えてくれる、
インターフェースと条件式（Java では t1 ? t2 : t3 と書く）の間の相互作用のため、型付け可能な項に対して最小の型を与えるような型付け関係のアルゴリズムが必要である。

(1) Java 流のインターフェースで FJ を拡張する方法を示せ
(2) インターフェースが存在するなら、部分型関係が結びの下で必ずしも閉じるとは限らないことを示せ。（結びの存在は、条件式の最小型付け性に重要な役割を果たす）
(3) 条件式に対する Java の型付け規則はどのようなものだろうか。それは妥当か。

解答）
(1)
クラス宣言に加えて、インターフェース宣言を追加する。

(2) 以下のようなインターフェースを宣言したとする

• interface A {}
• interface B {}
• interface C extends A, B {}
• interface D extends A, B {}

(3)
条件式に対する標準的なアルゴリズム的規則は以下であったが、

Γ├ t1 : boolean	Γ├ t2 : E2	Γ├ t3 : E3
Γ├ (t1 ? t2 : t3) : E2 v E3

これの代わりに、以下のように制限した規則を用いる。

...	Γ├ E2 <: E3
Γ├ ... : E2

...	Γ├ E3 <: E2
Γ├ ... : E3

演習 19.4.7.
FJ に super のキーワードを追加する方法を示せ。

解答）
これを実現するには、「現在実行中のメソッド本体」が属するクラスを覚えておかねばならない。

(1) どこを参照すれば良いかについて、項に何らかの注釈を追加する。
(2) super の参照を this の参照と同じにしておき、現在実行中のメソッドがどのクラスのメソッドなのかという情報を、呼び出したい別のメソッドに埋め込む。

FJ では標準的な型保存定理が証明できる。

定理 19.5.1. [保存] Γ├ t : C かつ t → t' ならば、ある C' <: C に対して Γ├ t' : C'

解答）
t → t' の導出に関する帰納法。最後に適用した規則で場合分けをする。

(1) E-ProjNew の場合 t = (new C0(<v>)).fi, t' = vi, fields(C0) = <D f>

t の形から、Γ├ t : C の導出の最後の規則は T-Field。前提部より、Γ├ (new C0(<v>)) : D0, C = Di だとわかる。
同様に Γ├ (new C0(<v>)) : D0 の最後の導出規則は T-New であるから、前提として Γ├ <v> : <C> かつ <C> <: <D> だとわかる。これより、D0 = C0, Γ├ vi : Ci より Ci <: Di

(2) E-InvkNew の場合

以下、省略。


もしプログラムが正しく型付けされていれば、それが行き詰まり状態になる唯一の方法はキャストできない状態に到達した場合だけである。

補題 19.5.2. t が正しく型付けされた項だとする。

1. t = new C0(<t>).fi ならば、fields(C0) = <C f> かつ fi ∈ <f>
2. t = new C0(<T>).m(<S>) ならば、mbody(m, C0) = (<x>, t0) かつ |<x>| = |<s>|

解答）
(1)
最後に適用した型付け規則は、T-Field のはず。つまり Γ├ t : Ci で、Γ├ new C0(<t>) : C0, fields(C0) = <C f> となる。

(2)
省略


定義 19.5.3. FJ の評価文脈の集合は以下のように定義される。

E	::=	[]	穴
		E.f	フィールド参照
		E.m(<t>)	メソッド呼び出し (レシーバ)
		v.m(<v>, E, <t>)	メソッド呼び出し (引数)
		new C(<v>, E, <t>)	オブジェクト生成 (引数)
		(C)E	キャスト

評価文脈は、[] で示される穴をどこかに含む。E の中の穴を t で置き換えて得られる項を E[t] と書く。
評価文脈は「次に簡約される部分項」の概念を表している。

定理 19.5.4. [進行] t が閉じた、正しく型付けされた正規形であるとする。このとき、
(1) t は値であるか
(2) ある評価文脈 E に対し、t を E[(C)(new D(<v>))] (ただし D !<: C) と表現できる。

解答）
(1) 型付けされていても、キャストできない状態に到達すると行き詰まり状態になるため、必ずしも値（＝オブジェクト生成）ではない。（3章 正規形 参照)

(2) t は正規形なので、評価文脈の穴を持たない。このため、t を任意の項xに対して、E[x] としてよい。



進行の性質はもう少し強くできる。もし t がアップキャストしか含まないなら、行き詰まり状態になることはない。
しかし、一般的には、オブジェクトの静的な型を低い方へ変えるためにアップキャストを使わざるを得ず、キャストが実行時に失敗しうる可能性を受け入れねばならない。

演習 19.5.5.
ラムダ計算の型検査器のどれかを出発点として、FJ の型検査器とインタプリタを構築せよ。

解答）
省略


演習 19.5.6.
元々の FJ の論文では、多相型も形式化している。演習19.5.5のインタプリタを拡張して、これらの機能を実装せよ。（23, 25, 26, 28 章の知識が必要)

解答）
省略

18章では、レコード、参照、ラムダ計算の機能を組み合わせて、オブジェクト、クラス、継承を表現した。
本章では、オブジェクトとクラスを組み込みとして持つ単純な言語を説明した。

この２つの対照的アプローチにはどちらも使い道がある。

オブジェクトの表現により、オブジェクトの仕組みがあらわになるため、低水準な言語にオブジェクトを翻訳するコンパイル方法を考える手助けになる。
組み込み機能としてのオブジェクトにより、操作的意味論や型付けの振る舞いを直接議論することができる。

究極的には、オブジェクトを組み込みで含む高水準な言語から、レコードと関数しか持たないような低水準な言語への変換を示し、その正当性を証明することが良いとされる。

FJ の他の紹介