サブタイピング

ウィキペディアから、無料の百科事典
ナビゲーションにジャンプ 検索にジャンプ

プログラミング言語理論ではサブタイピングサブタイプポリモーフィズムまたは包含ポリモーフィズム)は、サブタイプが別のデータ型(スーパータイプ)に置換可能性の概念によって関連付けられているデータ型であるタイプポリモーフィズムの形式です。つまり、プログラム要素、通常はサブルーチンです。または、スーパータイプの要素を操作するように記述された関数は、サブタイプの要素も操作できます。SがTのサブタイプである場合、サブタイピング関係はしばしばS <:Tと記述されます。これは、タイプSの任意の項が次のようになることを意味します。タイプTの用語が予想される状況で安全に使用されます。サブタイピングの正確なセマンティクスは、特定のプログラミング言語で「どこで安全に使用されるか」が意味する内容の詳細に大きく依存しますプログラミング言語の型システムは、基本的に独自のサブタイピング関係を定義します。これは、言語が変換メカニズムをサポートしていない(またはほとんどサポートしていない)場合は、 些細なことかもしれません。

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

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

サブタイピングの概念は、下位概念と下位概念の言語概念に関連しています。また、数理論理学における有界量化の概念にも関連しています(順序ソートされた論理を参照)。サブタイピングは、オブジェクト指向言語からの(クラスまたはオブジェクト)継承の概念と混同しないでください。[2]サブタイピングはタイプ間の関係(オブジェクト指向用語でのインターフェース)ですが、継承は、既存のオブジェクトから新しいオブジェクトを作成できるようにする言語機能に由来する実装間の関係です。多くのオブジェクト指向言語では、サブタイピングはインターフェイス継承と呼ばれ、継承は次のように呼ばれます。実装の継承

起源

プログラミング言語でのサブタイピングの概念は1960年代にまでさかのぼります。Simula派生物で導入されました。サブタイピングの最初の正式な扱いは、1980年に圏論を使用して暗黙の変換を形式化したJohn C. ReynoldsLucaCardelli(1985)によって行われました。[3]

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

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

より実用的な例として、言語では、浮動小数点値が予想される場所(Integer< :)で整数値を使用できるFloat場合や、ジェネリック型を定義する場合があります。番号整数と実数の一般的なスーパータイプとして。この2番目のケースでは、Integer<:NumberFloat<:のみNumberIntegerありますが、Floatは相互のサブタイプではありません。

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

function  max  x  as  Number  y  as  Number  
     x  <  yの場合は y
        返し、 それ以外の場合はxendを返します。
    
         

整数と実数が両方とものサブタイプでありNumber、任意の数値との比較の演算子が両方のタイプに対して定義されている場合、どちらのタイプの値もこの関数に渡すことができます。ただし、このような演算子を実装する可能性は、数値タイプを非常に制約し(たとえば、整数と複素数を比較することはできません)、実際には整数と整数、および実数と実数を比較するだけで意味があります。同じ型の「x」と「y」のみを受け入れるようにこの関数を書き直すには、制限付きポリモーフィズムが必要です。

包摂

型理論では、包摂の概念[4]を使用して、タイプSがタイプTのサブタイプである かどうかを定義または評価します

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

包含の概念を説明する際に、型の値のセットは、その名前を数学的なイタリック体で書くことによって示されます:Tドメインの述語として表示されるタイプは、名前を太字で表記して示されます:T従来の記号<:は「のサブタイプ」を意味し、:>は「のスーパータイプ」を意味します。

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

経験則に従う:サブタイプは、そのスーパータイプの1つ(より制限されている)よりも「大きい/広い/深い」(その値はより多くの情報を保持する)および「少ない/小さい」(値のセットは小さい)である可能性があります情報、およびその値のセットはサブタイプの値のスーパーセットです)。

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

2つの述語がある場合、タイプT選択基準を適用します。タイプSに追加の基準を適用し、次に2つのタイプのセットを定義できます。

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

例:ネコ科と呼ばれる猫種の亜科があります。これはネコ科の一部です飼い猫の種であるFeliscatusが属するFelis、その亜科の一部です。

ここでは、述語の接続詞は、最初の述語に準拠する値のドメインに2番​​目の述語を適用することで表現されています。タイプとして表示される、Felis <:Felinae <:Felidae

TがSを包含している場合T:> S)、値が与えられたプロシージャ、関数、または式したがって、オペランド(入力引数または項)として、タイプTの1つとしてその値を操作できるようになります上記の例では、Subfamilyの関数は、ネコ科ネコ科、ネコ科の3つのタイプすべての値に適用できると期待できます

サブタイピングスキーム

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

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

サブタイピング関係を定義するほとんどすべての型システムでは、反射的(任意の型Aに対してA  <:  Aを意味する)および推移的(A  <:  BおよびB  <:  Cの場合はA  <:  Cを意味する)です。これにより、タイプの予約注文になります。

レコードタイプ

幅と奥行きのサブタイピング

レコードのタイプは、深さのサブタイピングの概念を生み出します。これらは、元のレコードタイプと同じ操作を可能にする新しいタイプのレコードを取得する2つの異なる方法を表します。

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

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

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

レコードのサブタイピングは、システムF <:で定義できます。これは、パラメトリックポリモーフィズムとレコードタイプのサブタイピングを組み合わせたものであり、両方の機能をサポートする 多くの関数型プログラミング言語の理論的基礎です。

一部のシステムは、ラベル付けされた非交和型(代数的データ型など)のサブタイピングもサポートしています。幅のサブタイピングの規則が逆になります。幅のサブタイプに表示されるすべてのタグは、幅のスーパータイプに表示される必要があります。

関数型

T1T2が関数型である場合、そのサブタイプは、T 1 < S1およびS2 < T2というプロパティを持つ任意の関数S1S2ですこれは、次の入力規則を使用して要約できます

S1S2の引数の型は、サブタイピングの関係が逆になっているため、反変あると言われますが、戻りの型は共変です。非公式には、この逆転は、洗練されたタイプが受け入れるタイプでは「よりリベラル」であり、返すタイプでは「より保守的」であるために発生します。これはScalaで正確に機能するものです:n -ary関数は、内部的には 特性Javaのような言語では一般的なインターフェースと見なすことができます)、ここではパラメータタイプであり、Bはその戻りタイプです。タイプの前の「-」はタイプが反変であることを意味し、「+」は共変であることを意味します。

ほとんどのオブジェクト指向言語のように、副作用を許容する言語では、サブタイピングは一般に、関数が別のコンテキストで安全に使用できることを保証するのに十分ではありません。この分野でのLiskovの作業は、振る舞いサブタイピングに焦点を当てていました。この記事で説明する型システムの安全性に加えて、サブタイプは、一部の契約でスーパータイプによって保証されるすべての不変条件を保持する必要があります。[5]このサブタイピングの定義は一般に決定不可能であるため、型チェッカーで検証することはできません

可変参照のサブタイピングは、関数の引数と戻り値の処理に似ています。書き込み専用の参照(またはシンク)は、関数の引数のように反変です。読み取り専用の参照(またはソース)は、戻り値のように共変です。ソースとシンクの両方として機能する可変参照は不変です。

相続との関係

サブタイピングと継承は、独立した(直交する)関係です。それらは一致する可能性がありますが、他の特殊なケースはありません。言い換えると、2つのタイプSTの間で、サブタイピングと継承のすべての組み合わせが可能です。

  1. SはTのサブタイプでも派生タイプでもありません
  2. Sはサブタイプですが、Tの派生タイプではありません
  3. Sはサブタイプではありませんが、 Tの派生型です
  4. STのサブタイプと派生タイプの両方です

Boolean最初のケースは、やなどの独立したタイプで示されていFloatます。

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

3番目のケースは、入力の反変性をサブタイピングする関数の結果です。同じタイプのオブジェクトを返すメソッドmを持つタイプTのスーパークラス(つまり、 mのタイプTTであり、 mの最初の引数はthis / selfであることに注意してください)とTから派生したクラスタイプSを想定します。 。継承により、SのmタイプSSです。SがTのサブタイプであるためにはSのmのタイプTのmタイプのサブタイプである必要があります。つまり、SS≤TTです。関数サブタイピングルールのボトムアップ適用により、これは次のことを意味します。S≤ :TおよびT≤:S。これは、ST同じある場合のみ可能です。継承は非反射的な関係であるため、SをTのサブタイプにすることはできません

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

強制

強制的なサブタイピングシステムでは、サブタイプは、サブタイプからスーパータイプへの暗黙の型変換関数によって定義されます。サブタイピング関係(S <:T)ごとに、強制関数coerceSTが提供され、タイプSのオブジェクトsは、タイプTのオブジェクト強制STs)と見なされます強圧的関数は、構成によって定義できます。S <:TおよびT <:Uの場合、s複合強制(強制TU∘強制ST )の下でタイプuのオブジェクト見なすことができます型からそれ自体へ強制強制TT恒等関数idTです

レコードおよび非交和サブタイプの強制関数は、コンポーネントごとに定義できます。幅が拡張されたレコードの場合、型強制は、スーパータイプで定義されていないコンポーネントを単に破棄します。関数型の型強制は、関数の引数の反変性戻り値の共分散を 反映して、 f 's)= coerce S2T2fc​​oerce T1 S1 t ))で与えられます。

強圧的関数は、サブタイプとスーパータイプが与えられると一意に決定されます。したがって、複数のサブタイピング関係が定義されている場合は、すべてのタイプの強制がコヒーレントであることを保証するように注意する必要があります。たとえば、2:intなどの整数を浮動小数点数(たとえば、2.0:float )に強制できる場合、複合強制強制floatfloatであるため、 2.1:floatを2:intに強制することはできません。 coerceint float∘coercefloatintは、アイデンティティの強制異なりますidfloat_

も参照してください

メモ

  1. ^ Cardelli、Luca。多重継承のセマンティクス。G. Kahn、D。MacQueen、およびG. Plotkinの編集者、データタイプのセマンティクス、コンピュータサイエンスのレクチャーノートの第173巻、51〜67ページ。Springer-Verlag、1984年。InformationandComputationのフルバージョン、76(2/3):138–164、1988年。
  2. ^ a b Cook、Hill&Canning1990
  3. ^ ピアス、ch。15ノート
  4. ^ ベンジャミンC.ピアス、タイプとプログラミング言語、MIT Press、2002、15.1「Subsumption」、p。181-182
  5. ^ Barbara Liskov、Jeannette Wing、サブタイピングの動作概念、プログラミング言語とシステムに関するACMトランザクション、第16巻、第6号(1994年11月)、1811〜1841ページ。更新されたバージョンがCMUテクニカルレポートとして表示されました: Liskov、Barbara ; ウィング、ジャネット(1999年7月)。「不変量と制約を使用した振る舞いサブタイピング」 PS2006年10月5日取得

参考文献

教科書

  • ベンジャミンC.ピアス、タイプとプログラミング言語、MIT Press、2002、ISBN 0-262-16209-1、第15章(レコードタイプのサブタイピング)、19.3(記名的型と構造型およびサブタイピング)、および23.2(ポリモーフィズムの多様性) )。 
  • C. Szyperski、D。Gruntz、S。Murer、コンポーネントソフトウェア:オブジェクト指向プログラミングを超えて、第2版、Pearson Education、2002年、ISBN 0-201-74572-0、93〜95ページ(高レベルのプレゼンテーションプログラミング言語ユーザーを対象としています) 

論文

クック、ウィリアムR。; ヒル、ウォルター; キャニング、ピーターS.(1990)。継承はサブタイピングではありませんProc。17番目のACMSIGPLAN-SIGACTSymp。プログラミング言語の原則(POPL)について。pp。125–135。CiteSeerX10.1.1.102.8635 _ 土井10.1145 /96709.96721ISBN 0-89791-343-4
  • Reynolds、JohnC。圏論を使用して暗黙の変換と一般的な演算子を設計します。NDジョーンズ、編集者、セマンティクスに向けられたコンパイラ生成に関するオーフスワークショップの議事録、コンピュータサイエンスのレクチャーノートの94番。Springer-Verlag、1980年1月。また、Carl A.GunterおよびJohnC。Mitchellの編集者、オブジェクト指向プログラミングの理論的側面:タイプ、セマンティクス、および言語設計(MIT Press、1994)。

さらに読む