サブタイピング (計算機科学)
| 型システム |
|---|
| 主要カテゴリ |
|
静的型付け vs 動的型付け 強い vs 弱い 明示的 vs 型推論 名前的 vs 構造的 ダックタイピング |
| マイナーカテゴリ |
|
部分型 再帰型 部分構造型 依存型 漸進的型付け フロータイピング 潜在的型付け |
| 型理論のコンセプト |
|
直積型 - 直和型 交差型 - 共用型 単一型 - 選択型 帰納型 - 精製型 トップ型 - ボトム型 函数型 - 商型 全称型 - 存在型 一意型 - 線形型 |
サブタイピング（英: 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クラス図のスーパークラスとサブクラスのサブタイピングである（右図参照）。ここでのsupertypeは基底型、subtypeは派生型と呼ばれやすい。
トリは基底型であり、アヒル/カッコウ/ダチョウは派生型である。トリ型の変数xには、トリ型のインスタンスだけでなく、アヒル/カッコウ/ダチョウ型のインスタンスをも代入できて、その際の変数xは、トリ型の派生（sub）で型付け（typing）されることになる。
二番目の例は、型の上位概念と下位概念に基づいた変数である。ここではsupertypeは上位型、subtypeは下位型と呼ばれやすい。
それぞれ数値型のNumber（総称的な数値）Float（浮動小数点）Integer（整数）があるとして、これらはサブタイプ記号<:でこのように表現できる。
Integer <: Float <: NumberInteger <: 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）を満たすものである。つまり前順序が成り立つ。
関連項目
[編集]参考資料
[編集]- Meyer, Bertrand (2000年). Object-Oriented Software Construction. Prentice Hall. ISBN 0136291554
- 邦訳『オブジェクト指向入門 第2版』 ISBN 4798111112
- “The Liskov Substitution Principle” (PDF) (英語). 2006年12月26日閲覧。
- “リスコフの置換原則” (PDF). 2006年12月26日閲覧。
参照
[編集]- ^ Benjamin C. Pierce「第Ⅲ部 部分型付け」『型システム入門 −プログラミング言語と型の理論−』オーム社、2013年3月26日。ISBN 978-4274069116。
- ^ Benjamin C. Pierce「15.1 包摂」『型システム入門 −プログラミング言語と型の理論−』オーム社、2013年3月26日。ISBN 978-4274069116。