サブタイプ

プログラミング言語理論では、サブタイピング(サブタイプ多態性または包含多態性とも呼ばれる) は、型多態性の一形態です。サブタイプとは、代替可能性の概念によって別のデータ型 (スーパータイプ)に関連付けられたデータ型です。つまり、スーパータイプの要素を操作するように記述されたプログラム要素 (通常はサブルーチンまたは関数) は、サブタイプの要素も操作できます。

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

サブタイプ関係により、用語は複数の型に属する場合があります。したがって、サブタイプは型ポリモーフィズムの一形態です。オブジェクト指向プログラミングでは、「ポリモーフィズム」という用語は、このサブタイプ ポリモーフィズムのみを指すのによく使用されますが、パラメトリック ポリモーフィズムの手法はジェネリック プログラミングと見なされます。

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

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

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

サブタイピングの概念は、オブジェクト指向プログラミングが主流に採用されるにつれて、注目されるようになりました (一部の界隈ではポリモーフィズムと同義です)。この文脈では、安全な置換の原則は、1987 年にオブジェクト指向プログラミングに関する会議の基調講演で普及させたBarbara Liskovにちなんで、Liskov 置換原則と呼ばれることがよくあります。Liskov とJeannette Wingによって定義されたサブタイピングの理想的な概念は、動作サブタイピングと呼ばれ、可変オブジェクトを考慮する必要があるため、型チェッカーで実装できるものよりもかなり強力です。(詳細については、以下の § 関数型を参照してください。)

サブタイプの簡単な実例を図に示します。タイプ「鳥」には、「アヒル」、「カッコウ」、「ダチョウ」の 3 つのサブタイプがあります。概念的には、これらはそれぞれ基本タイプ「鳥」の変種であり、「鳥」の多くの特性を継承していますが、特定の違いがあります。この図ではUML表記法が使用されており、開いた矢印はスーパータイプとそのサブタイプの関係の方向とタイプを示しています。

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

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

関数max ( x as Number , y as Number )は、 x < yの場合はyを返し、そうでない場合はx を返すというものです。        
        
         
    
         

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

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

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

包含の概念について議論する場合、型の値の集合は数学的なイタリック体でその名前を記述して示されます: T 。ドメイン上の述語として見られる型は、その名前を太字で記述して示されます: T。慣例的な記号<: は「サブタイプである」ことを意味し、:> は「スーパータイプである」ことを意味します。^{[引用が必要]}

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

情報の特異性という点では、サブタイプは、そのスーパータイプのいずれよりも特異であると見なされます。なぜなら、サブタイプは、少なくとも各スーパータイプと同じ量の情報を保持しているからです。これにより、サブタイプの適用性、つまり関連性(サブタイプが受け入れられたり導入されたりできる状況の数) が、その「より一般的な」スーパータイプと比較して高くなる可能性があります。このより詳細な情報を持つことの欠点は、組み込まれた選択肢を表し、サブタイプの普及率(サブタイプを生成または生産できる状況の数) が減少することです。

包含のコンテキストでは、型定義は、述語を使用してセットを定義するセットビルダー表記法を使用して表現できます。述語は、ドメイン (可能な値のセット) Dに対して定義できます。述語は、値を選択基準と比較する部分関数です。たとえば、「整数値は 100 以上 200 未満ですか?」などです。値が基準に一致する場合、関数はその値を返します。そうでない場合、値は選択されず、何も返されません。(リストの理解は、多くのプログラミング言語で使用されるこのパターンの形式です。)

型Tに選択基準を適用する述語と、型Sに追加の基準を適用する述語の 2 つがある場合、2 つの型のセットを定義できます。 ${\displaystyle P_{T}}$${\displaystyle P_{s}}$

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

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

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

たとえば、ネコ科にはFelinaeと呼ばれるネコ科の亜科があります。飼いネコの種であるFelis catusが属するFelis属も、この亜科の一部です。

${\displaystyle {\mathit {ネコ科=\{cat\in ネコ科\mid \ ofSubfamily(cat,felinaeSubfamilyName)\}}}}$

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

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

T がS を包含する場合( T :> S )、オペランド (パラメーター値または項) として値を与えられたプロシージャ、関数、または式は、その値をT型の 1 つとして操作できます。これは、 のためです。上記の例では、関数ofSubfamily がFelidae、Felinae、Felis の3 つの型すべての値に適用可能であることが期待できます。 ${\displaystyle s\in S}$${\displaystyle s\in T}$

型理論家は、特定の方法で宣言された型のみが互いのサブタイプになる名目上のサブタイプ化と、2 つの型の構造によって一方が他方のサブタイプであるかどうかが決定される構造上のサブタイプ化を区別しています。上記のクラスベースのオブジェクト指向サブタイプ化は名目上のものです。オブジェクト指向言語の構造上のサブタイプ化ルールでは、型Aのオブジェクトが型Bのオブジェクトが処理できるすべてのメッセージを処理できる場合(つまり、同じメソッドをすべて定義する場合)、どちらかが他方から継承しているかどうかに関係なく、 AはBのサブタイプであるとされています。このいわゆるダック タイピングは、動的型付けオブジェクト指向言語では一般的です。オブジェクト型以外の型に対する適切な構造上のサブタイプ化ルールもよく知られています。^{[引用が必要]}

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

サブタイプ関係を定義するほとんどすべての型システムでは、サブタイプ関係は反射的（任意の型Aに対してA  <:  Aであることを意味する）かつ推移的（A  <:  BかつB  <:  Cの場合、A  <:  Cであることを意味する）です。これにより、サブタイプ関係は型の事前順序になります。

レコードの種類によって、幅と深さのサブタイプの概念が生まれます。これらは、元のレコードの種類と同じ操作を可能にする新しい種類のレコードを取得する 2 つの異なる方法を表します。

レコードは (名前付きの) フィールドのコレクションであることを思い出してください。サブタイプは元のタイプで許可されているすべての操作を許可するタイプであるため、レコードのサブタイプは元のタイプがサポートしていたのと同じフィールド操作をサポートする必要があります。

このようなサポートを実現する方法の 1 つは、幅のサブタイプ化と呼ばれ、レコードにフィールドを追加します。より正式には、幅のスーパータイプに表示されるすべての (名前付き) フィールドが幅のサブタイプに表示されます。したがって、スーパータイプで実行可能なすべての操作がサブタイプによってサポートされます。

2 番目の方法は、深さサブタイプ化と呼ばれ、さまざまなフィールドをそのサブタイプに置き換えます。つまり、サブタイプのフィールドは、スーパータイプのフィールドのサブタイプです。スーパータイプのフィールドでサポートされている操作は、そのサブタイプでもサポートされているため、レコード スーパータイプで実行可能な操作は、レコード サブタイプでもサポートされます。深さサブタイプ化は、不変レコードに対してのみ意味を持ちます。たとえば、実数ポイント (2 つの実数フィールドを持つレコード) の 'x' フィールドに 1.5 を割り当てることはできますが、整数ポイント (ただし、実数ポイント タイプの深いサブタイプ) の 'x' フィールドに同じことを行うことはできません。これは、1.5 が整数ではないためです ( 「分散」を参照)。

レコードのサブタイプはSystem F _<:で定義できます。これは、パラメトリック多態性とレコード型のサブタイプを組み合わせたもので、両方の機能をサポートする多くの関数型プログラミング言語の理論的基礎となっています。

一部のシステムでは、ラベル付けされた分離ユニオン型 (代数データ型など) のサブタイプもサポートされています。幅のサブタイプのルールは逆になります。幅のサブタイプに出現するすべてのタグは、幅のスーパータイプにも出現する必要があります。

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

$${\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項関数は、内部的には特性( Javaのような言語の一般的なインターフェースとして見ることができます)を継承するクラスであり、はパラメータ型、は戻り値の型です。型の前の「-」は型が反変であることを意味し、「+」は共変であることを意味します。 ${\displaystyle {\mathtt {Function_{N}({-A_{1}},{-A_{2}},\dots ,{-A_{n}},{+B})}}}$ ${\displaystyle {\mathtt {A_{1},A_{2},\dots ,A_{n}}}}$${\displaystyle {\mathtt {B}}}$

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

可変参照のサブタイプ化は、パラメータ値と戻り値の扱いに似ています。書き込み専用参照 (またはシンク) は、パラメータ値のように反変です。読み取り専用参照 (またはソース) は、戻り値のように共変です。ソースとシンクの両方として機能する可変参照は不変です。

サブタイプ化と継承は独立した（直交する）関係です。 それらは同時に起こることもありますが、どちらかが他方の特別なケースになることはありません。 言い換えると、2 つの型SとTの間では、サブタイプ化と継承のすべての組み合わせが可能です。

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

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

Int322 番目のケースは、との関係によって説明できますInt64。ほとんどのオブジェクト指向プログラミング言語では、Int64は と継承によって関連付けられていませんInt32。ただし、任意の 32 ビット整数値は 64 ビット整数値に昇格できるため、Int32は のサブタイプと見なすことができますInt64。

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の場合、複合強制 ( coerce _{T → U} ∘ coerce _{S → T} ) の下でs は型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とは異なるためです。

ウィキブックAdaプログラミングには、サブタイプに関するページがあります。

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

教科書

論文