サブタイプ分類

プログラミング言語理論において、サブタイピング（サブタイプ多相性または包含多相性とも呼ばれる）は、型多相性の一種である。サブタイプとは、何らかの置換可能性の概念によって別のデータ型（スーパータイプ）と関連付けられたデータ型であり、スーパータイプの要素を操作するように記述されたプログラム要素（通常はサブルーチンまたは関数）は、サブタイプの要素も操作できることを意味する。

S が T のサブタイプである場合、サブタイピング関係( S < : T、S ⊑ T、^{[ 1 ]}またはS ≤: Tと表記) は、型 T の項が期待されるあらゆるコンテキストで、型 S の任意の項を安全に使用できることを意味します。ここでのサブタイピングの正確な意味は、特定の型形式体系またはプログラミング言語によって「安全に使用できる」および「あらゆるコンテキスト」がどのように定義されているかの詳細に大きく依存します。プログラミング言語の型システムは、基本的に独自のサブタイピング関係を定義しますが、言語が変換メカニズムをまったく (またはほとんど) サポートしていない場合、それは自明である可能性があります。   

サブタイピング関係により、1つの用語が複数の型に属する場合があります。したがって、サブタイピングは型多相性の一形態です。オブジェクト指向プログラミングでは、「多相性」という用語は一般的にこのサブタイプ多相性のみを指すのに用いられ、パラメトリック多相性の手法はジェネリックプログラミングとみなされます。

関数型プログラミング言語では、レコードのサブタイピングがしばしば許可されます。したがって、レコード型で拡張された単純な型付きラムダ計算は、サブタイピングの有用な概念を定義し研究できる最も単純な理論的設定と言えるでしょう。 ^{[ 2 ]}結果として得られる計算では、項が複数の型を持つことが許されるため、もはや「単純な」型理論ではありません。関数型プログラミング言語は、定義上、レコードに格納できる関数リテラルをサポートしているため、サブタイピングを備えたレコード型は、オブジェクト指向プログラミングのいくつかの機能を提供します。通常、関数型プログラミング言語は、通常は制限された形式のパラメトリック多相性も提供します。理論的設定では、2 つの機能の相互作用を研究することが望ましいです。一般的な理論的設定は、システム F _{< :}です。オブジェクト指向プログラミングの理論的特性を捉えようとするさまざまな計算は、システム F _{< :}から派生することができます。

サブタイピングの概念は、言語学における下位概念と全体概念に関連しています。また、数理論理学における限定量化の概念にも関連しています（順序ソート論理を参照）。サブタイピングは、オブジェクト指向言語における（クラスまたはオブジェクトの）継承の概念と混同してはなりません。 ^{[ 3 ]}サブタイピングは型（オブジェクト指向の用語ではインターフェース）間の関係であるのに対し、継承は既存のオブジェクトから新しいオブジェクトを作成できる言語機能から生じる実装間の関係です。多くのオブジェクト指向言語では、サブタイピングはインターフェース継承と呼ばれ、継承は実装継承と呼ばれます。

プログラミング言語におけるサブタイピングの概念は1960年代に遡り、Simula派生言語で導入されました。サブタイピングの最初の形式的な扱いは、1980年にジョン・C・レイノルズが圏論を用いて暗黙の型変換を形式化し、またルカ・カルデッリ（1985年）によって行われました。^{[ 4 ]}

オブジェクト指向プログラミングが主流となるにつれ、サブタイピングの概念は注目を集めるようになり（一部ではポリモーフィズムと同義語として扱われることもある）、この文脈において、安全な置換の原則は、 1987年のオブジェクト指向プログラミングに関する会議での基調講演でこの原則を広めたバーバラ・リスコフにちなんで、リスコフ置換原則と呼ばれることが多い。リスコフとジャネット・ウィングによって定義された、振る舞いサブタイピングと呼ばれる理想的なサブタイピングの概念は、可変オブジェクトを考慮する必要があるため、型チェッカーで実装できるものよりもはるかに強力である。（詳細は下記の§関数型を参照。） 

サブタイプの簡単な実例を図に示します。「鳥」という型には、「アヒル」、「カッコウ」、「ダチョウ」という3つのサブタイプがあります。概念的には、これらはそれぞれ基本型「鳥」のバリエーションであり、「鳥」の多くの特性を受け継ぎつつ、いくつかの具体的な違いを持っ​​ています。この図ではUML表記法が用いられており、開いた矢印はスーパータイプとそのサブタイプ間の関係の方向とタイプを示しています。

より実用的な例として、言語によっては、浮動小数点値が期待される場所であればどこでも整数値の使用を許可したり（Integer< Float:）、汎用型を定義したりする場合があります。番号整数と実数の共通のスーパータイプとして。この2番目のケースでは、Integer<:NumberとFloat<:しかありませNumberんが、Integerと はFloat互いのサブタイプではありません。

プログラマーは、サブタイピングを利用することで、サブタイピングがない場合よりも抽象的な方法でコードを記述することができます。次の例を考えてみましょう。

function max ( x as Number , y as Number ) is if x < y then return y else return x end

整数と実数がどちらも のサブタイプでありNumber、任意の数値との比較演算子が両方の型に対して定義されている場合、どちらの型の値もこの関数に渡すことができます。ただし、そのような演算子を実装できる可能性自体が数値型を厳しく制限します (たとえば、整数と複素数を比較することはできません)。実際には、整数同士、実数同士を比較することだけが意味を持ちます。この関数を書き換えて、同じ型の 'x' と 'y' のみを受け入れるようにするには、境界付き多相性が必要です。

サブタイピングによって、特定の型を別の型または抽象概念に置き換えることが可能になります。サブタイピングは、言語のサポート状況に応じて、暗黙的または明示的に、サブタイプと既存の抽象概念との間に「 is-a」関係を確立すると言われています。継承をサブタイピングのメカニズムとしてサポートする言語では、この関係を継承によって明示的に表現できます。

class A { public : void methodOfA () const { // ... } };class B : public A { public : void methodOfB () const { // ... } };void functionOnA ( const A & a ) { a . methodOfA (); }int main () { B b ; functionOnA ( b ); // b は A に置き換えることができます。 }

class A : def method_of_a ( self ) -> None : passclass B ( A ): def method_of_b ( self ) -> None : passdef function_on_a ( a : A ) -> None : a . method_of_a ()if __name__ == "__main__" : b : B = B () function_on_a ( b ) # b は A の代わりに使用できます。

a = 0 print(type(a)) # 出力: <type 'int'> print(type(type(a))) # 出力: <type 'type'> print(type(type(type(a)))) # 出力: <type 'type'> print(type(type(type(type(a))))) # 出力: <type 'type'>

interface PayloadList < E , P > extends List < E > { void setPayload ( int index , P val ); ... }

PayloadList < String , String > PayloadList < String , Integer > PayloadList < String , Exception >

型理論では、包含関係の概念^{[ 7 ]} が、型Sが型Tのサブタイプであるかどうかを定義または評価するために使用されます。

型とは値の集合です。この集合は、すべての値を列挙することによって外延的に記述することも、可能な値のドメインに対する述語によって集合のメンバーシップを明示することによって内包的に記述することもできます。一般的なプログラミング言語では、列挙型は値を列挙することによって外延的に定義されます。レコード（構造体、インターフェース）やクラスなどのユーザー定義型は、明示的な型宣言によって、または型情報をエンコードした既存の値をコピーまたは拡張するプロトタイプとして使用することによって内包的に定義されます。

包含関係の概念を説明する際、型の値の集合は、その型名を数学的なイタリック体で表記することで示されます。T 。ドメイン上の述語として見なされる型は、その型名を太字で表記することで示されます。T 。慣例的な記号<:は「 のサブタイプである」という意味で、:>は「 のスーパータイプである」という意味です。

• 型T がSを包含するとは、 Tが定義する値の集合が集合Sのスーパーセットであり、 Sのすべての要素がTの要素でもある場合をいう。
• ある型は複数の型に包含されることがあります。S のスーパータイプはSで交差します。
• S <: T (したがってS ⊆ T )の場合、集合Tを囲む述語Tは、 Sを定義する述語S (同じドメイン上)の一部でなければなりません。
• SがTを包含し、TがSを包含する場合、2つの型は等しい（ただし、型システムが型を名前で区別する場合は、同じ型ではない可能性がある）。

情報の特異性という観点から見ると、サブタイプは上位のどのタイプよりも具体的であると言えます。なぜなら、サブタイプは上位のどのタイプよりも少なくとも同等の情報量を持っているからです。これにより、サブタイプの適用性、つまり関連性（受け入れられたり導入されたりする状況の数）は、より「一般的な」上位タイプと比較して高まる可能性があります。しかし、この詳細な情報を持つことの欠点は、サブタイプの普及率（サブタイプを生成または発生させることができる状況の数）を低下させるような選択肢が組み込まれていることです。

包含関係の文脈では、型定義はセット構築記法を用いて表現できます。この記法では、述語を用いてセットを定義します。述語は、ドメイン（可能な値の集合）D上で定義できます。述語は、値を選択基準と比較する部分関数です。例えば、「整数値は 100 以上 200 未満か？」といった具合です。値が基準に一致する場合、関数はその値を返します。一致しない場合は、値は選択されず、何も返されません。（リスト内包表記は、多くのプログラミング言語で使用されているこのパターンの一種です。）

述語が 2 つある場合、${\displaystyle P_{T}}$これはタイプTの選択基準を適用し、${\displaystyle P_{s}}$これはタイプSに追加の基準を適用するものであり、その後、2つのタイプのセットを定義できます。

${\displaystyle T=\{v\in D\mid \ P_{T}(v)\}}$

${\displaystyle S=\{v\in D\mid \ P_{T}(v){\text{ および }}P_{s}(v)\}}$

述語$\displaystyle \mathbf {T} =P_{T}}$と並行して適用されます${\displaystyle P_{s}}$Sを定義する複合述語Sの一部として。2 つの述語は結合されているため、値を選択するには両方とも真である必要があります。述語${\displaystyle \mathbf {S} =\mathbf {T} \land P_{s}=P_{T}\land P_{s}}$述語Tを包含するので、S <: Tとなります。

例えば、ネコ科にはFelinaeという亜科があり、これはFelidae科の一部です。イエネコ（Felis catus）が属するFelis属は、この亜科に属します。

${\displaystyle {\mathit {Felinae=\{cat\in Felidae\mid \ ofSubfamily(cat,felinaeSubfamilyName)\}}}}$

${\displaystyle {\mathit {Felis=\{ネコ科の猫\mid \ ofGenus(cat,felisGenusName)\}}}}$

ここでは、述語の結合は、最初の述語に適合する値の領域に2番目の述語を適用することによって表現されています。タイプとして見ると、Felis <: Felinae <: Felidaeとなります。

T がSを包含する場合( T  :> S )、値が与えられた手続き、関数、または式${\displaystyle s\in S}$オペランド（パラメータ値または項）として、型Tの 1 つとしてその値に対して操作を行うことができます。${\displaystyle s\in T}$上記の例では、Subfamily関数はFelidae、Felinae、Felisの 3 つのタイプの値すべてに適用できると予想されます。

型理論家は、特定の方法で宣言された型のみが互いのサブタイプになり得るという名目サブタイピングと、2つの型の構造によって一方が他方のサブタイプであるかどうかが決まるという構造サブタイピングを区別します。上記で説明したクラスベースのオブジェクト指向サブタイピングは名目サブタイピングです。オブジェクト指向言語の構造サブタイピング規則では、型Aのオブジェクトが型Bのオブジェクトが処理できるすべてのメッセージを処理できる場合（つまり、すべてのメソッドが同じ場合）、どちらが他方を継承しているかに関わらず、 AはBのサブタイプであると規定されるかもしれません。このいわゆるダックタイピングは、動的型付けのオブジェクト指向言語でよく見られます。オブジェクト型以外の型に対する健全な構造サブタイピング規則もよく知られています。

サブタイピングを備えたプログラミング言語の実装は、大きく分けて2つのクラスに分類されます。1つは包括的実装で、型Aの任意の値の表現は、A < : Bの場合、型Bの同じ値も表現します。もう1つは強制実装で、型Aの値は自動的に型Bの値に変換されます。オブジェクト指向言語におけるサブクラス化によって生じるサブタイピングは通常包括的です。表現方法が異なる整数と浮動小数点数を関連付けるサブタイピング関係は、通常強制的です。  

サブタイピング関係を定義するほとんどすべての型システムにおいて、それは反射的（任意の型Aに対してA < : Aが成り立つ）かつ推移的（A < : BかつB < : CならばA < : Cが成り立つ）である。このため、それは型上の順序関係となる。        

T ₁ → T ₂が関数型である場合、そのサブタイプは、T 1 <: S 1 かつ S 2 <: T 2_という性質を_持つ任意の関数_型S 1 _→ S 2_です。これは_、次の型付け規則を使用して要約できます。

$${\displaystyle {T_{1}\leq :S_{1}\quad S_{2}\leq :T_{2}} \over {S_{1}\rightarrow S_{2}\leq :T_{1}\rightarrow T_{2}}}$$

S ₁ → S ₂のパラメータ型は、サブタイピング関係が反転しているため反変であると言われますが、戻り値の型は共変です。非公式には、この反転は、洗練された型が受け入れる型に関しては「より自由」であり、返す型に関しては「より保守的」であるために起こります。これはまさにScalaで機能するものです。n項関数は内部的にはクラスであり、${\displaystyle {\mathtt {Function_{N}({-A_{1}},{-A_{2}},\dots ,{-A_{n}},{+B})}}}$特性（ Javaのような言語では一般的なインターフェースと見なすことができる）は、${\displaystyle {\mathtt {A_{1},A_{2},\dots ,A_{n}}}}$はパラメータの型であり、${\displaystyle {\mathtt {B}}}$は戻り値の型です。型の前の「−」は反変型を意味し、「+」は共変型を意味します。

副作用を許容する言語（ほとんどのオブジェクト指向言語など）では、サブタイピングは一般的に、ある関数が別の関数のコンテキストで安全に使用できることを保証するには不十分です。リスコフのこの分野の研究は、振る舞いサブタイピングに焦点を当てており、この記事で議論されている型システムの安全性に加えて、サブタイプが何らかの契約でスーパータイプによって保証されるすべての不変条件を保持することも要求します。^{[ 8 ]}このサブタイピングの定義は一般に決定不能であるため、型チェッカーで検証することはできません。

可変参照のサブタイピングは、パラメータ値と戻り値の扱いと似ています。書き込み専用参照（またはシンク）は、パラメータ値と同様に反変であり、読み取り専用参照（またはソース）は、戻り値と同様に共変です。ソースとシンクの両方の役割を果たす可変参照は不変です。

サブタイピングと継承は独立した（直交する）関係です。両者は一致することもありますが、どちらかが他方の特殊なケースということはありません。言い換えれば、2つの型SとTの間には、サブタイピングと継承のあらゆる組み合わせが可能です。

1. SはTのサブタイプでも派生タイプでもない。
2. Sはサブタイプであるが、 Tの派生タイプではない。
3. Sはサブタイプではなく、 Tの派生型である。
4. SはTのサブタイプであり、派生タイプでもある。

最初のケースは、やなどの独立した型によって示されBooleanますFloat。

Int322番目のケースは、 との関係で説明できますInt64。ほとんどのオブジェクト指向プログラミング言語では、Int64は と継承関係にありませんInt32。しかし、Int32は のサブタイプと考えることができますInt64。なぜなら、任意の32ビット整数値を64ビット整数値に昇格できるからです。

3 番目のケースは、関数サブタイピング入力の反変性の結果です。同じ型のオブジェクトを返すメソッドmを持つ型Tのスーパークラス (つまり、 mの型はT → Tであり、 mの最初のパラメータが this/self であることにも注意) と、 Tから派生したクラス型Sがあるとします。継承により、 S内のmの型はS → Sです。SがTのサブタイプである ためには、 S内のmの型がT内のmの型のサブタイプでなければなりません。つまり、S → S ≤: T → Tです。関数サブタイピング規則をボトムアップで適用すると、これはS ≤: TかつT ≤: Sを意味しますが、これはSとTが同じ場合にのみ可能です。継承は非反射的な関係であるため、S はTのサブタイプにはなれません。

派生型の継承されたすべてのフィールドとメソッドが、継承された型の対応するフィールドとメソッドのサブタイプである型を持つ場合、サブタイピングと継承は互換性があります。^{[ 3 ]}

強制型サブタイピングシステムでは、サブタイプはサブタイプからスーパータイプへの明示的な型変換関数によって定義されます。各サブタイピング関係 ( S <: T ) に対して、強制関数coerce : S → Tが提供され、型Sの任意のオブジェクトsは、型Tのオブジェクトcoerce _{S → T} ( s )とみなされます。強制関数は合成によって定義できます。S <: TかつT < : Uの場合、sは複合強制 ( coerce _{T → U} ∘ coerce _{S → T} ) の下で型uのオブジェクトとみなされます。型からそれ自身への型強制coerce _{T → T}は、恒等関数id _Tです。

レコードおよび非連結共用体サブタイプの型強制関数は、コンポーネントごとに定義できます。幅拡張レコードの場合、型強制はスーパータイプで定義されていないコンポーネントを単純に破棄します。関数タイプの型強制は、パラメータ値の反変性と戻り値の共変性を反映して、 f' ( t ) = coerce _{S 2 → T 2} ( f ( coerce _{T 1 → S 1} ( t )))で与えられます。

型変換関数は、サブタイプとスーパータイプが与えられた場合に一意に決定されます。したがって、複数のサブタイピング関係が定義されている場合は、すべての型変換が一貫していることを保証するように注意する必要があります。たとえば、2  : intのような整数を浮動小数点数 (たとえば 2.0  : float  ) に変換できる場合、2.1 : float を2  : intに変換することは許容されません。なぜなら_、coerce _{int → float} ∘ coerce _{float → int}で与えられる複合変換coerce _{float → float}は、同一変換id _floatとは異なるものになるからです。

• 共分散と反分散
• 円と楕円の問題（変数型を値型と同じ基準でサブタイピングすることの危険性について）
• クラスベースプログラミング
• トップタイプ
• 精製タイプ
• 行動サブタイプ分類

教科書

論文