概念

さて、サブタイプ(subtyping)の学習に入ります。 サブタイプはオブジェクト指向プログラミングをサポートするのに重要な機能の一つです。

動機付け

以下に定義する二つのレコード型が出現するプログラムを書いているとしましょう。

      Person  = {name:String, age:Nat} 
      Student = {name:String, age:Nat, gpa:Nat} 

レコードを持つ単純型付きラムダ計算では、項

      (\r:Person. (r.age)+1) {name="Pat",age=21,gpa=1} 

は型付けできません。 なぜなら、これはフィールドが2つのレコードを引数としてとる関数に3つのフィールドを持つレコードが与えられている部分を含んでいて、一方、T_App規則は関数の定義域の型は引数の型に完全に一致することを要求するからです。 しかしこれは馬鹿らしいことです。 実際には関数に、必要とされるものより良い引数を与えているのです！ この関数の本体がレコード引数rに対して行いうることは、そのフィールドageを射影することだけです。 型から許されることは他にはありません。 すると、他にgpaフィールドが存在するか否かは何の違いもないはずです。 これから、直観的に、この関数は少なくともageフィールドを持つ任意のレコード値に適用可能であるべきと思われます。 一般に、より豊かなフィールドを持つレコードは、そのサブセットのフィールドだけを持つレコードと「任意のコンテキストで少なくとも同等の良さである」と言えるでしょう。 より長い（多くのフィールドを持つ）レコード型の任意の値は、より短かいレコード型が求められるコンテキストで「安全に」(safely)使えるという意味においてです。 コンテキストがより短かい型のものを求めているときに、より長い型のものを与えた場合、何も悪いことは起こらないでしょう（形式的には、プログラムは行き詰まることはないでしょう）。 ここで働く一般原理はサブタイプ（付け）(subtyping)と呼ばれます。 型Tの値が求められている任意のコンテキストで型Sの値が安全に使えるとき、「SはTのサブタイプである」と言い、 S <: T と書きます。 サブタイプの概念はレコードだけではなく、関数、対、など言語のすべての型コンストラクタに適用されます。 Safe substitution principle:

• S is a subtype of T, written S <: T, if a value of type S can safely be used in any context where a value of type T is expected.

サブタイプとオブジェクト指向言語

サブタイプは多くのプログラミング言語で重要な役割を演じます。 特に、オブジェクト指向言語のサブクラス(subclassing)の概念と近い関係にあります。 JavaやC#等のオブジェクトはレコードと考えることができます。 いくつかのフィールドは関数(「メソッド」)で、いくつかのフィールドはデータ値（「フィールド」または「インスタンス変数」）です。 オブジェクトoのメソッドmを引数a1..anのもとで呼ぶことは、大雑把に言うと、oからmフィールドを射影として抽出して、それをa1..anに適用することです。 オブジェクトの型は「クラス(class)」や、言語によっては「インターフェース(interface)」と呼ばれます。 この両者はどちらも、どのメソッドやどのデータフィールドをオブジェクトが提供するかを表しています。 クラスやインターフェースは、サブクラス(subclass)関係やサブインターフェース(subinterface)関係で関係づけられます。 サブクラス（またはサブインターフェース）に属するオブジェクトには、スーパークラス（またはスーパーインターフェース）に属するオブジェクトのメソッドとフィールドのすべての提供することが求められ、さらに追加で他のメソッドやフィールドを提供することもできます。 サブクラスのオブジェクトをスーパークラスのオブジェクトの場所で使えるという事実は、複雑なライブラリの構築にきわめて便利なほどの柔軟性を提供します。 例えば、Javaの Swingフレームワークのようなグラフィカルユーザーインターフェースツールキットは、スクリーンに表示できユーザとインタラクションできるグラフィカルな表現を持つすべてのオブジェクトに共通のフィールドとメソッドを集めた、抽象インターフェースComponentを定義するでしょう。 そのようなオブジェクトとしては、典型的なGUIのボタン、チェックボックス、スクロールバーなどがあります。 この共通インターフェースのみに依存するメソッドはこれらのどのオブジェクトにも適用できます。 もちろん、実際のオブジェクト指向言語はこれらに加えてたくさんの機能を持っています。 例えば、フィールドを更新できます。 フィールドやメソッドをprivateと宣言できます。 クラスにオブジェクトを作り上げるための「初期化子(initializer)」を定義できます。 サブクラスのコードが「継承(inheritance)」を通じてスーパークラスのコードと協調できます。 クラスが静的なメソッドやフィールドを持つことができます。 などなど、です。 ものごとを単純なまま進めるために、これらの問題を扱うことはしません。 実際、これ以上オブジェクトやクラスについて話すことはありません。 （もし興味があるなら、 Bib.v 内の Pierce 2002 にたくさんの議論があります。） その代わり、STLCの単純化された設定のもとで、サブクラス/サブインターフェース関係の背後にある核となる概念について学習します。

包摂規則

この章のゴールは（MoreStlcの拡張機能を持つ）単純型付きラムダ計算にサブタイプを追加することです。 これは2つのステップから成ります：

• 型の間の二項サブタイプ関係(subtype relation)を定義します。
• 型付け関係をサブタイプを考慮した形に拡張します。

2つ目のステップは実際はとても単純です。型付け関係にただ1つの規則だけを追加します。 その規則は、包摂規則(rule of subsumption)と呼ばれます：

                         Gamma |- t \in S     S <: T 
                         ---------------------------                    (T_Sub) 
                               Gamma |- t \in T 

この規則は、直観的には、項について知っている情報のいくらかを「忘れる」ようにしてよいと言っています。

例えば、tが2つのフィールドを持つレコード（例えば、S = {x:A->A, y:B->B}）で、フィールドの1つを忘れることにした（T = {y:B->B}）とします。 するとtを、1フィールドのレコードを引数としてとる関数に渡すことができるようになります。

サブタイプ関係

最初のステップ、関係 S <: T の定義はすべてのアクションに関して存在します。 それぞれの定義を見てみましょう。

構造規則

まず最初に、2つの「構造規則」("structural rules")を追加します。 これらは特定の型コンストラクタからは独立したものです。 推移(transitivity)規則は、直観的には、SがUよりも（安全、豊かさの面で）良く、UがTよりも良ければ、SはTよりも良いというものです。

                              S <: U    U <: T 
                              ----------------                        (S_Trans) 
                                   S <: T 

そして反射(reflexivity)規則は、任意の型はそれ自身と同じ良さを持つというものです。

                                   ------                              (S_Refl) 
                                   T <: T 

直積型

次に、直積型です。 ある一つの対が他の対のサブタイプであるとは、それぞれの成分が対応するもののサブタイプであることです。

                            S1 <: T1    S2 <: T2 
                            --------------------                        (S_Prod) 
                             S1 * S2 <: T1 * T2 

関数型

関数型のサブタイプ関係はやや直観から外れます。 次の型を持つ2つの関数fとgがあるとします：
       f : C -> Student
       g : (C->Person) -> D

つまり、fは型Studentのレコードを返す関数であり、gは引数として、型Personのレコードを返す関数をとる高階関数です。 そして、Student が Person のサブタイプであるとします。 すると、関数適用 g f は、両者の型が正確に一致しないにもかかわらず安全です。 なぜなら、gがfについて行うことができるのは、fを（型Cの）ある引数に適用することだけだからです。 その結果は実際にはStudent型のレコード値になります。 ここでgが期待するのはPerson型のレコードです。 しかしこれは安全です。なぜならgがすることができるのは、わかっている2つのフィールド（nameとage）を射影することだけで、それは存在するフィールドの一部だからです。 この例から、関数型のサブタイプ規則が以下のようになるべきということが導かれます。 2つの関数型がサブタイプ関係にあるのは、その結果が次の条件のときです:

                                  S2 <: T2 
                              ----------------                     (S_Arrow_Co) 
                            S1 -> S2 <: S1 -> T2 

同様に、これを一般化して、2つの関数型のサブタイプ関係を、引数の条件を含めた形にすることができます:

                            T1 <: S1    S2 <: T2 
                            --------------------                      (S_Arrow) 
                            S1 -> S2 <: T1 -> T2 

ここで注意するのは、引数の型はサブタイプ関係が逆向きになることです。 S1->S2 が T1->T2 のサブタイプであると結論づけるには、T1がS1のサブタイプでなければなりません。 関数型のコンストラクタは最初の引数について反変(contravariant)であり、 二番目の引数について共変(covariant)であると言います。 このことを表す例を見てみましょう。
       f : Person -> C
       g : (Student -> C) -> D

関数適用g fは安全です。 なぜなら、gの本体でのfの使い方は、Student型の引数に適用することだけだからです。 fは（少なくとも）Personのもつフィールドを含んだレコードを要求するだけなので、これはうまく動きます。 よって、StudentがPersonのサブタイプであるため、Person -> CはStudent -> Cのサブタイプとなります。 直観的には、型S1->S2の関数fがあるとき、fは型S1の要素を引数として許容することがわかります。 明らかにfはS1の任意のサブタイプT1の要素も引数として許容します。 fの型は同時にfが型S2の要素を返すことも示しています。 この値がS2の任意のスーパータイプT2に属することも見ることができます。 つまり、型S1->S2の任意の関数fは、型T1->T2を持つと見ることもできるということです。

レコード

レコード型のサブタイプは何でしょうか？

基本的直観は、「より小さな」レコードの場所で「より大きな」レコードを使うことは常に安全だということです。 つまり、レコード型があるとき、さらにフィールドを追加したものは常にサブタイプになるということです。 もしあるコードがフィールドxとyを持つレコードを期待していたとき、レコードx、y、zを持つレコードを受けとることは完璧に安全です。 zフィールドは単に無視されるだけです。 例えば次の通りです。
    {name:String, age:Nat, gpa:Nat} <: {name:String, age:Nat}
    {name:String, age:Nat} <: {name:String}
    {name:String} <: {}

これはレコードの「幅サブタイプ(width subtyping)」として知られます。

レコードの1つのフィールドの型をそのサブタイプで置き換えることでも、レコードのサブタイプを作ることができます。 もしあるコードが型Tのフィールドxを持つレコードを期待するとき、型Sが型Tのサブタイプである限り、型Sのフィールドxを持つレコードが来ても何の問題も起こりません。 例えば次の通りです。
    {x:Student} <: {x:Person}

これは「深さサブタイプ(depth subtyping)」として知られています。

最後に、レコードのフィールドは特定の順番で記述されますが、その順番は実際には問題ではありません。 例えば次の通りです。
    {name:String,age:Nat} <: {age:Nat,name:String}

これは「順列サブタイプ(permutation subtyping)」として知られています。

これらをレコードについての単一のサブタイプ規則に形式化することもできはします。 次の通りです:

                        forall jk in j1..jn, 
                    exists ip in i1..im, such that 
                          jk=ip and Sp <: Tk 
                  ----------------------------------                    (S_Rcd) 
                  {i1:S1...im:Sm} <: {j1:T1...jn:Tn} 

つまり、左のレコードは(少なくとも)右のレコードのフィールドラベルをすべて持ち、両者で共通するフィールドはサブタイプ関係になければならない、ということです。 しかしながら、この規則はかなり重くて読むのが大変なので、3つの簡単な規則に分解されます。 この3つをS_Transを使って結合することで、同じように作用させることができます。

最初に、レコード型の最後にフィールドを追加したものはサブタイプになります。

                               n > m 
                 ---------------------------------                 (S_RcdWidth) 
                 {i1:T1...in:Tn} <: {i1:T1...im:Tm} 

S_RcdWidthを使うと、複数のフィールドを持つレコードについて、 前方のフィールドを残したまま後方のフィールドを取り除くことができます。 この規則で例えば {age:Nat,name:String} <: {age:Nat} を示せます。

二つ目では、レコード型の構成要素の内部にサブタイプ規則を適用できます。

                       S1 <: T1  ...  Sn <: Tn 
                  ----------------------------------               (S_RcdDepth) 
                  {i1:S1...in:Sn} <: {i1:T1...in:Tn} 

例えば S_RcdDepthとS_RcdWidthを両方使って {y:Student, x:Nat} <: {y:Person}を示すことができます。

三つ目に、サブタイプとしてフィールドの並べ替えを可能にします。 例えば {name:String, gpa:Nat, age:Nat} <: Person であってほしいのです。 （これはまだ達成されていません。 S_RcdDepthとS_RcdWidthだけでは、レコード型の「後」からフィールドを落とすことしかできません。） そのため、次の規則が必要です。

         {i1:S1...in:Sn} is a permutation of {j1:T1...jn:Tn} 
         ---------------------------------------------------        (S_RcdPerm) 
                  {i1:S1...in:Sn} <: {j1:T1...jn:Tn} 

なお、本格的な言語ではこれらのサブタイプ規則のすべてを採用しているとは限らないことは注記しておくべきでしょう。 例えばJavaでは

• 各クラスのメンバー（フィールドまたはメソッド）は1つだけインデックスを持ち、サブクラスでメンバーが追加されるたびに新しいインデックスが「右に」追加されます （つまり、クラスには並び換えがありません）。
• クラスは複数のインターフェースを実装できます。 これはインターフェースの「多重継承(multiple inheritance)」と呼ばれます （つまり、インターフェースには並び換えがあります）。
• 昔のバージョンでは、サブクラスではスーパークラスのメソッドの引数または結果の型を変えることはできませんでした （つまり、depth subtypingまたは関数型サブタイプのいずれかができなかったということです。 どちらかは見方によります）。

練習問題: ★★, standard, recommended (arrow_sub_wrong)

関数型のサブタイプについて、誤って矢印の左右両方とも共変として定義してしまったとする。

                            S1 <: T1    S2 <: T2 
                            --------------------                (S_Arrow_wrong) 
                            S1 -> S2 <: T1 -> T2 

2つの関数fとgについて、以下の型
       f : Student -> Nat
       g : (Person -> Nat) -> Nat

を満たし、適用g fが実行時に行き詰まるような例を挙げなさい。 （非形式的な構文で構いません。 行き詰まることの形式的な証明を与える必要もありません。）

☐

Top

最後に、サブタイプ関係の最大要素を定めます。 他のすべての型のスーパータイプであり、すべての(型付けできる)値が属する型です。 このために言語に新しい一つの型定数Topを追加し、Topをサブタイプ関係の他のすべての型のスーパータイプとするサブタイプ規則を定めます:

                                   --------                             (S_Top) 
                                   S <: Top 

Top型はJavaやCにおける[Object]型に対応するものです。

Summary

In summary, we form the STLC with subtyping by starting with the pure STLC (over some set of base types) and then...

• adding a base type Top,
• adding the rule of subsumption
  Gamma |- t \in S S <: T
  • -------------------------- (T_Sub) Gamma |- t \in T
  to the typing relation, and
• defining a subtype relation as follows:
  S <: U U <: T
  • --------------- (S_Trans) S <: T
    • ----- (S_Refl)
    T <: T
    • ------- (S_Top)
    S <: Top
  S1 <: T1 S2 <: T2
  • ------------------- (S_Prod) S1 * S2 <: T1 * T2
  T1 <: S1 S2 <: T2
  • ------------------- (S_Arrow)
  S1 -> S2 <: T1 -> T2
  n > m
  • -------------------------------- (S_RcdWidth)
  {i1:T1...in:Tn} <: {i1:T1...im:Tm}
  S1 <: T1 ... Sn <: Tn
  • --------------------------------- (S_RcdDepth)
  {i1:S1...in:Sn} <: {i1:T1...in:Tn}
  {i1:S1...in:Sn} is a permutation of {j1:T1...jn:Tn}
  • -------------------------------------------------- (S_RcdPerm) {i1:S1...in:Sn} <: {j1:T1...jn:Tn}

Exercises

Exercise: 1 star, standard, optional (subtype_instances_tf_1)

Suppose we have types S, T, U, and V with S <: T and U <: V. Which of the following subtyping assertions are then true? Write true or false after each one. (A, B, and C here are base types like Bool, Nat, etc.)

• T->S <: T->S
• Top->U <: S->Top
• (C->C) -> (A*B) <: (C->C) -> (Top*B)
• T->T->U <: S->S->V
• (T->T)->U <: (S->S)->V
• ((T->S)->T)->U <: ((S->T)->S)->V
• S*V <: T*U

☐

Exercise: 2 stars, standard (subtype_order)

The following types happen to form a linear order with respect to subtyping:

• Top
• Top -> Student
• Student -> Person
• Student -> Top
• Person -> Student

Write these types in order from the most specific to the most general. Where does the type Top->Top->Student fit into this order? That is, state how Top -> (Top -> Student) compares with each of the five types above. It may be unrelated to some of them.

☐

Exercise: 1 star, standard (subtype_instances_tf_2)

Which of the following statements are true? Write true or false after each one. forall S T, S <: T -> S->S <: T->T forall S, S <: A->A -> exists T, S = T->T /\ T <: A forall S T1 T2, (S <: T1 -> T2) -> exists S1 S2, S = S1 -> S2 /\ T1 <: S1 /\ S2 <: T2 exists S, S <: S->S exists S, S->S <: S forall S T1 T2, S <: T1*T2 -> exists S1 S2, S = S1*S2 /\ S1 <: T1 /\ S2 <: T2

☐

Exercise: 1 star, standard (subtype_concepts_tf)

Which of the following statements are true, and which are false?

• There exists a type that is a supertype of every other type.
• There exists a type that is a subtype of every other type.
• There exists a pair type that is a supertype of every other pair type.
• There exists a pair type that is a subtype of every other pair type.
• There exists an arrow type that is a supertype of every other arrow type.
• There exists an arrow type that is a subtype of every other arrow type.
• There is an infinite descending chain of distinct types in the subtype relation---that is, an infinite sequence of types S0, S1, etc., such that all the Si's are different and each S(i+1) is a subtype of Si.
• There is an infinite ascending chain of distinct types in the subtype relation---that is, an infinite sequence of types S0, S1, etc., such that all the Si's are different and each S(i+1) is a supertype of Si.

☐

Exercise: 2 stars, standard (proper_subtypes)

Is the following statement true or false? Briefly explain your answer. (Here Base n stands for a base type, where n is a string standing for the name of the base type. See the Syntax section below.) forall T, ~(T = Bool \/ exists n, T = Base n) -> exists S, S <: T /\ S <> T

☐

Exercise: 2 stars, standard (small_large_1)

• What is the smallest type T ("smallest" in the subtype relation) that makes the following assertion true? (Assume we have Unit among the base types and unit as a constant of this type.)
  empty |- (\p:T*Top. p.fst) ((\z:A.z), unit) \in A->A
• What is the largest type T that makes the same assertion true?

☐

Exercise: 2 stars, standard (small_large_2)

• What is the smallest type T that makes the following assertion true?
  empty |- (\p:(A->A * B->B). p) ((\z:A.z), (\z:B.z)) \in T
• What is the largest type T that makes the same assertion true?

☐

Exercise: 2 stars, standard, optional (small_large_3)

• What is the smallest type T that makes the following assertion true?
  a:A |- (\p:(A*T). (p.snd) (p.fst)) (a, \z:A.z) \in A
• What is the largest type T that makes the same assertion true?
  ☐

Exercise: 2 stars, standard (small_large_4)

• What is the smallest type T that makes the following assertion true?
  exists S, empty |- (\p:(A*T). (p.snd) (p.fst)) \in S
• What is the largest type T that makes the same assertion true?

☐

Exercise: 2 stars, standard (smallest_1)

What is the smallest type T that makes the following assertion true? exists S t, empty |- (\x:T. x x) t \in S

☐

Exercise: 2 stars, standard (smallest_2)

What is the smallest type T that makes the following assertion true? empty |- (\x:Top. x) ((\z:A.z) , (\z:B.z)) \in T

☐

Exercise: 3 stars, standard, optional (count_supertypes)

How many supertypes does the record type {x:A, y:C->C} have? That is, how many different types T are there such that {x:A, y:C->C} <: T? (We consider two types to be different if they are written differently, even if each is a subtype of the other. For example, {x:A,y:B} and {y:B,x:A} are different.) ☐

Exercise: 2 stars, standard (pair_permutation)

The subtyping rule for product types S1 <: T1 S2 <: T2

---

(S_Prod) S1*S2 <: T1*T2 intuitively corresponds to the "depth" subtyping rule for records. Extending the analogy, we might consider adding a "permutation" rule

---

T1*T2 <: T2*T1 for products. Is this a good idea? Briefly explain why or why not.

☐

形式的定義

上記の議論で使った、形式化する定義のほとんど -- 特に言語の構文と操作的意味 -- は前の章で見たものと同じです。 ここで必要となるものは型付け規則の包括規則による拡張と、サブタイプ関係を表す帰納的定義の追加です。 最初に同じ部分をやってみましょう。

中核部の定義

構文

この章の残りでは、レコード型は省略して、基底型、ブール型、関数型、UnitとTopのみ形式化し、直積型は練習問題にします。 例をおもしろくするために、String、Floatのような、任意の基底型を許しています。 （これはあくまで例で用いるためだけなので、わざわざこれらへの操作を追加したりはしませんが、そうすることは簡単です。）

置換

置換の定義はSTLCと全く同じです。

簡約

value(値)の定義やstep関係の定義と同様です。

サブタイプ

ようやくおもしろい所にやって来ました。 サブタイプ関係の定義から始め、その重要な技術的性質を調べます。

サブタイプの定義は、動機付けの議論のところで概観した通りです。

なお、基底型（BoolとBase）について、特別な規則は何ら必要ありません。 基底型は自動的に(S_Reflより)自分自身のサブタイプであり、（S_Topより）Topのサブタイプでもあります。 そしてこれが必要な全てです。

練習問題: ★★, standard, optional (subtyping_judgements)

（この練習問題は、練習問題productsを通じて、言語定義の少なくともファイルのこの場所まで直積型を追加するまでAdmittedのまま放置しておいてください。） MoreStlcの章では、「レコードのエンコード」という節で、レコードを対によって表現しました。 この方法を使い、以下のレコード型を表す組型を定義しなさい。
    Person := { name : String }
    Student := { name : String ; gpa : Float }
    Employee := { name : String ; ssn : Integer }

それらの型を用いて、以下のサブタイプ関係を示しなさい。

☐

以下の事実のほとんどは、Coqで証明するのは簡単です。 練習問題の効果を十分に得るために、どうやって証明するか自分が理解していることを紙に証明を書いて確認しなさい。

練習問題: ★, standard, optional (subtyping_example_1)

☐

練習問題: ★, standard, optional (subtyping_example_2)

☐

型付け

型付け関係の変更は、包摂規則 T_Sub の追加だけです。

The following hints help auto and eauto construct typing derivations. They are only used in a few places, but they give a nice illustration of what auto can do with a bit more programming. See chapter UseAuto for more on hints.

以下の練習問題は言語に直積を追加した後に行いなさい。 それぞれの非形式的な型付けジャッジメントについて、Coqで形式的主張を記述し、それを証明しなさい。

練習問題: ★, standard, optional (typing_example_0)

練習問題: ★★, standard, optional (typing_example_1)

練習問題: ★★, standard, optional (typing_example_2)

性質

チェックしたいシステムの根本的性質はいつもと同じく、進行と保存です。 STLCに参照を拡張したもの（References章）とは違い、サブタイプを考慮しても、これらの主張を変化させる必要はありません。 ただし、それらの証明はもうちょっと複雑になります。

サブタイプの反転補題(Inversion Lemma)

型付け関係の性質を見る前に、サブタイプ関係の2つの重要な構造的性質を記しておかなければなりません:

• BoolはBoolの唯一のサブタイプです。
• 関数型のすべてのサブタイプはやはり関数型です。

これらは反転補題(inversion lemma)と呼ばれます。 これは、証明で組込みのinversionタクティックに似た役目をするためです。 つまり、サブタイプ関係の主張 S <: T の導出が存在するという仮定と、SやTの形についてのいくつかの制約が与えられたとき、それぞれの反転補題は、S <: T の導出がどのような形をしていなければならないか、を提示することで、S や T のより詳細な情報、および S <: T が（矛盾なく）存在することを述べます。

練習問題: ★★, standard, optional (sub_inversion_Bool)

☐

練習問題: ★★★, standard (sub_inversion_arrow)

☐

正準形(Canonical Forms)

進行定理（値でない型付け可能な項の計算は進められる）の証明はそれほど大きく変える必要はありません。 1つだけ小さなリファインメントが必要です。 問題となる項が関数適用 t1 t2 でt1とt2が両方とも値の場合を考えるとき、t1がラムダ抽象の形をしており、そのためST_AppAbs簡約規則が適用できることを確認する必要があります。 もともとのSTLCでは、これは明らかです。 t1が関数型T11->T12を持ち、また、関数型の値を与える規則が1つだけ、つまり規則T_Absだけであり、そしてこの規則の結論部の形から、t1は関数型にならざるを得ない、ということがわかります。 サブタイプを持つSTLCにおいては、この推論はそのままうまく行くわけではありません。 その理由は、値が関数型を持つことを示すのに使える規則がもう1つあるからです。 包摂規則です。 幸い、このことが大きな違いをもたらすことはありません。 もし Gamma |- t1 \in T11->T12 を示すのに使われた最後の規則が包摂規則だった場合、導出のその前の部分で、同様にt1が主部(項の部分)である導出があり、帰納法により一番最初にはT_Absが使われたことが推論できるからです。 推論のこの部分は次の補題にまとめられています。 この補題は、関数型の可能な「正準形(canonical forms、つまり値)」を示します。

練習問題: ★★★, standard, optional (canonical_forms_of_arrow_types)

☐

同様に、型Boolの正準形は定数truとflsです。

進行

進行性の証明は純粋なSTLCとほぼ同様に進みます。 ただ何箇所かで正準形補題を使うことを除けば...

「定理」（進行）: 任意の項tと型Tについて、もし empty |- t \in T ならばtは値であるか、ある項t'について t --> t' である。 「証明」:tとTが与えられ、empty |- t \in T とする。 型付けの導出についての帰納法で進める。 （最後の規則が）T_Abs、T_Unit、T_True、T_Falseのいずれかの場合は自明である。 なぜなら、関数抽象、unit、tru、flsは既に値だからである。 T_Varであることはありえない。 なぜなら、変数は空コンテキストで型付けできないからである。 残るのはより興味深い場合である:

• 型付け導出の最後のステップで規則T_Appが使われた場合、項t1、t2と型T1、T2が存在して t = t1 t2、T = T2、empty |- t1 \in T1 -> T2、empty |- t2 \in T1 となる。 さらに帰納法の仮定から、t1は値であるかステップを進めることができ、t2も値であるかステップを進めることができる。 このとき、3つの場合がある:
  • ある項 t1' について t1 --> t1' とする。このときST_App1より t1 t2 --> t1' t2 である。
  • t1が値であり、ある項t2'について t2 --> t2' とする。 このとき規則ST_App2より t1 t2 --> t1 t2' となる。 なぜならt1が値だからである。
  • 最後にt1とt2がどちらも値とする。 関数型に対する正準形補題より、t1はあるx、S1、s2について\x:S1.s2という形である。 しかしするとt2が値であることから、ST_AppAbsより (\x:S1.s2) t2 --> [t2/x]s2 となる。
• 導出の最後のステップで規則T_Testが使われた場合、項t1、t2、t3があって t = test t1 then t2 else t3 となり、 empty |- t1 \in Bool かつ empty |- t2 \in T かつ empty |- t3 \in T である。 さらに、帰納法の仮定よりt1は値であるかステップを進めることができる。
  • もしt1が値ならば、ブール値についての正準形補題より t1 = tru または t1 = fls である。 どちらの場合でも、規則ST_TestTrueまたはST_TestFalseを使うことによってtはステップを進めることができる。
  • もしt1がステップを進めることができるならば、規則ST_Testよりtもまたステップを進めることができる。
• 導出の最後のステップが規則T_Subによる場合、型Sがあって S <: T かつ empty |- t \in S となっている。 求める結果は型付け導出の帰納法の仮定そのものである。

形式的には：

型付けの反転補題

保存定理の証明はサブタイプを追加したことでやはり少し複雑になります。 その理由は、上述の「サブタイプの反転補題」と同様に、純粋なSTLCでは定義から明らかであった（形式的には、inversionタクティックからすぐに得られた）性質が、サブタイプの存在で本当の証明を必要とするようになったためです。 サブタイプがある場合、同じhas_typeの主張を導出するのに複数の方法があるのです。 以下の反転補題は、もし関数抽象の型付け主張 Gamma |- \x:S1.t2 \in T の導出があるならば、その導出の中に本体t2の型を与える部分が含まれている、ということを言うものです。

「補題」: もし Gamma |- \x:S1.t2 \in T ならば、型S2が存在して x|->S1; Gamma |- t2 \in S2 かつ S1 -> S2 <: T となる。 （この補題は「Tはそれ自身が関数型である」とは言っていないことに注意します。 そうしたいところですが、それは成立しません!） 「証明」:Gamma、x、S1、t2、Tを補題の主張に記述された通りとする。 Gamma |- \x:S1.t2 \in T の導出についての帰納法で証明する。 T_VarとT_Appの場合はあり得ない。 これらは構文的に関数抽象の形の項に型を与えることはできないからである。

• 導出の最後のステップ使われた規則がT_Absの場合、型T12が存在して T = S1 -> T12 かつ x:S1; Gamma |- t2 \in T12 である。 S2としてT12をとると、S_Reflより S1 -> T12 <: S1 -> T12 となり、求める性質が成立する。
• 導出の最後のステップ使われた規則がT_Subの場合、型Sが存在して S <: T かつ Gamma |- \x:S1.t2 \in S となる。 型付け導出の帰納仮定より、型S2が存在して S1 -> S2 <: S かつ Gamma, x:S1 |- t2 \in S2 である。 このS2を採用すれば、 S1 -> S2 <: T であるからS_Transより求める性質が成立する。

形式的には：

同様に...

型付けについての反転補題と関数型の間のサブタイプの反転補題は「結合補題(combination lemma)」としてまとめることができます。 この補題は以下で実際に必要になるものを示します。

コンテキスト不変性

コンテキスト不変性補題は、純粋なSTLCと同じパターンをとります。

置換

置換補題(substitution lemma)は純粋なSTLCと同じ流れで証明されます。 唯一の大きな変更点は、いくつかの場所で、 部分項が型を持つことについての仮定から構造的情報を抽出するために、 Coqのinversionタクティックを使う代わりに上で証明した反転補題を使う必要があることです。

保存

（型の）保存の証明は以前の章とほとんど同じです。 適切な場所で置換補題を使い、型付け仮定から構造的情報を抽出するために上述の反転補題をまた使います。

「定理」（保存）： t、t'が項でTが型であり、empty |- t \in T かつ t --> t' ならば、empty |- t' \in T である。 「証明」：t と T が empty |- t \in T であるとする。 証明は、t'を特化しないまま型付け導出の構造に関する帰納法で進める。 (最後の規則が)T_Abs、T_Unit、T_True、T_Falseの場合は考えなくて良い。 なぜなら関数抽象と定数はステップを進めないからである。 T_Varも考えなくて良い。なぜならコンテキストが空だからである。

• もし導出の最後のステップの規則がT_Appならば、項t1 t2 と型 T1 T2 が存在して、t = t1 t2、T = T2、 empty |- t1 \in T1 -> T2、empty |- t2 \in T1 である。
  ステップ関係の定義から、t1 t2 がステップする方法は3通りである。 ST_App1とST_App2の場合、型付け導出の帰納仮定とT_Appより求める結果がすぐに得られる。
  t1 t2 のステップが ST_AppAbs によるとする。 するとある型Sと項t12について t1 = \x:S.t12 であり、かつ t' = [t2/x]t12 である。
  補題abs_arrowより、T1 <: S かつ x:S1 |- s2 \in T2 となる。 すると置換補題（substitution_preserves_typing）より、 empty |- [t2/x]t12 \in T2 となるがこれが求める結果である。
  • もし導出の最後のステップで使う規則がT_Testならば、項t1、t2、t3が存在して t = test t1 then t2 else t3 かつ empty |- t1 \in Bool かつ empty |- t2 \in T かつ empty |- t3 \in Tとなる。 さらに帰納法の仮定より、もしt1がステップしてt1'に進むならば empty |- t1' \in Bool である。 t --> t' を示すために使われた規則によって、3つの場合がある。
    • t --> t' が規則ST_Testによる場合、 t' = test t1' then t2 else t3 かつ t1 --> t1' となる。 帰納法の仮定より empty |- t1' \in Bool となり、これからT_Testより empty |- t' \in T となる。
    • t --> t' が規則ST_TestTrueまたはST_TestFalseによる場合、 t' = t2 または t' = t3 であり、仮定から empty |- t' \in T となる。
• もし導出の最後のステップで使う規則がT_Subならば、型Sが存在して S <: T かつ empty |- t \in S となる。 型付け導出についての帰納法の仮定とT_Subの適用から結果がすぐに得られる。 ☐

Records, via Products and Top

This formalization of the STLC with subtyping omits record types for brevity. If we want to deal with them more seriously, we have two choices. First, we can treat them as part of the core language, writing down proper syntax, typing, and subtyping rules for them. Chapter RecordSub shows how this extension works. On the other hand, if we are treating them as a derived form that is desugared in the parser, then we shouldn't need any new rules: we should just check that the existing rules for subtyping product and Unit types give rise to reasonable rules for record subtyping via this encoding. To do this, we just need to make one small change to the encoding described earlier: instead of using Unit as the base case in the encoding of tuples and the "don't care" placeholder in the encoding of records, we use Top. So: {a:Nat, b:Nat} ----> {Nat,Nat} i.e., (Nat,(Nat,Top)) {c:Nat, a:Nat} ----> {Nat,Top,Nat} i.e., (Nat,(Top,(Nat,Top))) The encoding of record values doesn't change at all. It is easy (and instructive) to check that the subtyping rules above are validated by the encoding.

練習問題

練習問題: ★★, standard (variations)

この問題の各部分は、Unitとサブタイプを持つSTLCの定義を変更する別々の方法を導きます。 （これらの変更は累積的ではありません。各部分はいずれも元々の言語から始まります。） 各部分について、（進行、保存の）性質のうち偽になるものをリストアップしなさい。 偽になる性質について、反例を示しなさい。

• 次の型付け規則を追加する:

                             Gamma |- t \in S1->S2 
                      S1 <: T1     T1 <: S1      S2 <: T2 
                      -----------------------------------    (T_Funny1) 
                             Gamma |- t \in T1->T2 
  

• 次の簡約規則を追加する:

                               --------------------         (ST_Funny21) 
                               unit --> (\x:Top. x) 
  

• 次のサブタイプ規則を追加する:

                                 ----------------          (S_Funny3) 
                                 Unit <: Top->Top 
  

• 次のサブタイプ規則を追加する:

                                 ----------------          (S_Funny4) 
                                 Top->Top <: Unit 
  

• 次の評価規則を追加する:

                               ---------------------      (ST_Funny5) 
                               (unit t) --> (t unit) 
  

• 上と同じ評価規則と新たな型付け規則を追加する:

                               ---------------------       (ST_Funny5) 
                               (unit t) --> (t unit) 
   
                             --------------------------    (T_Funny6) 
                             empty |- unit \in Top->Top 
  

• 関数型のサブタイプ規則を次のものに変更する:

                            S1 <: T1 S2 <: T2 
                            -----------------              (S_Arrow') 
                            S1->S2 <: T1->T2 
  

☐

練習問題: 直積の追加

練習問題: ★★★★★, standard (products)

定義したシステムに対、射影、直積型を追加することは比較的簡単な問題です。 上の定義や証明を書き換える形でこの拡張を行いなさい:

• 対のコンストラクタ、第1射影、第2射影、直積型を ty と tm の定義に追加し、それに伴う以下の定義を（MoreSTLC章を参考に）拡張しなさい。
  • 値関係
  • 置換
  • 操作的意味
  • 型付け関係
• サブタイプ関係に次の規則を追加しなさい。

                          S1 <: T1    S2 <: T2 
                          --------------------   (S_Prod) 
                           S1 * S2 <: T1 * T2 
  

• 型付け関係に、MoreSTLCの章と同様の、対と射影の規則を拡張しなさい。
• 進行および保存、およびそのための補題の証明を、新しい構成要素を扱うように拡張しなさい。 （いくつか新しい補題を追加する必要もあるでしょう。）

☐