Wikipedia

サブタイピング (計算機科学)

（部分型から転送）

サブタイピング（英: subtyping）や部分型[1]とは、型のポリモーフィズムの形態であり、上位と定義された型を、その下位と定義された型で、型安全性に則って代替できるというプログラミング言語理論（英語版）の概念および実装を意味している。

スーパータイプは、そのサブタイプの数々によって代替/代入可能とされており、これは代入可能性（substitutability）と呼ばれる。そのスーパータイプとサブタイプの関係は、is-aとも言われる。記号<:を用いてsubtype <: supertypeと表記される。

スーパータイプ＋サブタイプの概念はその時の用法で、上位型(supertype)＋下位型(subtype)、基底型(base type)＋派生型(derived type)、基本型(basic type)＋拡張型(extend type)、上位型(supertype)＋部分型(subtype) などの別称に使い分けられており、それぞれの性質にも差異がある。

起源

編集

サブタイピング（subtyping）は、Simula67で登場した継承と仮想手続き（仮想関数）を分析した計算機科学者ジョン・レイナルド（英語版）によって1980年に考案された言葉である。それを更に研究したルカ・カルデリ（英語版）らが、1985年にインクルージョン多相という概念にまとめた。

サブタイピングは、型理論ではなく、オブジェクト指向言語の継承とメソッドオーバーライドによる動的ディスパッチ（英語版）のポリモーフィズムを由来にしている。1994年にバーバラ・リスコフが、オブジェクト指向の継承のサブタイピング用法を重視したリスコフの置換原則[1]を提唱している。サブタイピングは上位概念と下位概念（hypernymy・hyponymy）に言及されることがあり[要校閲]、また全体概念と部分概念（holonymy・meronymy）にも言及されることがある[要検証 – ノート]。

サブタイピングに関連付けられているその他の概念としては、モジュラープログラミング（英語版）発のインターフェース、ジェネリックプログラミングの総称型、部分構造論理由来の部分構造型システム（英語版）などがある。サブタイピングを型理論視点で解釈拡張したものにSystem F-サブ（英語版）がある。

関数型言語の型構築子には深さサブタイピング（depth subtyping）という別解釈が加えられている。関数型言語はレコード型の深さサブタイピングと幅サブタイピング（width subtyping）や、関数の型（英語版）の共変反変サブタイピングも取り入れている。

例

編集
 
UMLクラス図表現。トリは基底型。アヒル・カッコウ・ダチョウは派生型。

最初の例は、UMLクラス図のスーパークラスとサブクラスのサブタイピングである（右図参照）。ここでのsupertypeは基底型、subtypeは派生型と呼ばれやすい。

トリは基底型であり、アヒル/カッコウ/ダチョウは派生型である。トリ型の変数xには、トリ型のインスタンスだけでなく、アヒル/カッコウ/ダチョウ型のインスタンスをも代入できて、その際の変数xは、トリ型の派生（sub）で型付け（typing）されることになる。

二番目の例は、型の上位概念と下位概念に基づいた変数である。ここではsupertypeは上位型、subtypeは下位型と呼ばれやすい。

それぞれ数値型のNumber（総称的な数値）Float（浮動小数点）Integer（整数）があるとして、これらはサブタイプ記号<:でこのように表現できる。

  1. Integer <: Float <: Number
  2. Integer <: Number　と　Float <: Number

上の規則によって、Number型の変数xに、Float型とInteger型の値を代入できることになる。従って変数xは多相になる。

そのコード例はこのようになる。 

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

関数maxは、Number型の引数x,yを通して、Float値とInteger値を計算できる。その際の引数x,yは、Number型の下位（sub）で型付け（typing）されることになる。

性質

編集

型理論においては、部分型関係は <: と表記される。つまり、A <: B という表記は A は B の部分型であるという意味である。型理論における部分型は、A <: B ならば型 A を持つ式はどれでも型 B をも持つという事実によって特性付けられる。この形式的な推論規則は包摂（subsumption）[2]として知られている。

型理論の研究者は、部分型であると宣言されたもののみを部分型とする名前的型システム（英語版）と、2つの型の構造によって部分型関係にあるかが決まる構造的型システム（英語版）を区別する。上記のクラスベースオブジェクト指向言語の例は名前的型システムである。構造的型システムのオブジェクト指向言語では、型 A のオブジェクトが型 B のオブジェクトの処理できるメッセージすべてを処理できるなら（言い換えると、同じメソッドを実装していれば）、継承関係に関係なく、A は B の部分型となる。

部分型を持つプログラミング言語の実装は大きく2つに分類される。型 A の値の内部表現が型 B の値としての内部表現も兼ねるinclusive（包含的）な実装と、型 A の値が型 B の値に「自動的に変換」されることのあるcoercive（強制的）な実装である。オブジェクト指向言語のサブクラスによる型の派生はたいてい包含的である。前述の整数と浮動小数点数の派生型関係は、内部表現が異なっているので、強制的な例である。

ほぼすべての型システムでは部分型関係が定義されている。それは反射律（任意の型 A について、A <: A）と推移律（A <: B かつ B <: C ならば A <: C）を満たすものである。つまり前順序が成り立つ。

関連項目

編集

参考資料

編集

参照

編集
  1. ^ Benjamin C. Pierce「第Ⅲ部 部分型付け」『型システム入門 −プログラミング言語と型の理論−』オーム社、2013年3月26日。ISBN 978-4274069116。 
  2. ^ Benjamin C. Pierce「15.1 包摂」『型システム入門 −プログラミング言語と型の理論−』オーム社、2013年3月26日。ISBN 978-4274069116。 

外部リンク

編集
「https://ja.wikipedia.org/w/index.php?title=サブタイピング_(計算機科学)&oldid=97440877」から取得