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

サブタイピングの概要

サブタイピングは、プログラミング言語における型のポリモーフィズムの一形式です。この概念は、上位型（supertype）と下位型（subtype）との間に形成される関係に基づいています。具体的には、上位型として定義された型を、下位型で置き換えることができ、かつ型安全性を維持することが求められています。この特性は、代入可能性（substitutability）と呼ばれ、一般的に「is-a」関係とも表現されます。サブタイピングの関係は、記号「<:」を用いて示され、たとえば「subtype <: supertype」といった表記がされます。

サブタイピングは、異なる文脈でいくつかの呼称を持ちます。例えば、上位型に基づく派生型（derived type）、基本型からの拡張型（extend type）といった用語が使われることもありますが、これらはサブタイピングに内包される概念です。各用語は、特定の性質や文脈に応じて使い分けられます。

サブタイピングの起源

サブタイピングという用語は、1980年に計算機科学者のジョン・レイナルドによって初めて提唱されました。この概念は、オブジェクト指向プログラミングの継承や仮想手続きから派生したものであり、さらに研究を重ねたルカ・カルデリらによって1985年に「インクルージョン多相」という形でまとめられました。特に1994年にはバーバラ・リスコフがリスコフの置換原則を提唱し、サブタイピングの重要性を一層強調しました。

サブタイピングは、単なる型理論だけでなく、オブジェクト指向言語における継承とメソッドのオーバーライドによるダイナミックディスパッチに根ざしています。そのため、サブタイピングは上位概念と下位概念（hypernymy・hyponymy）や全体概念・部分概念（holonymy・meronymy）に関連することがあります。

さらに、モジュラープログラミングに由来するインターフェース、ジェネリックプログラミングのタイプシステム、部分構造論に基づく部分構造型システムなども、サブタイピングに関連する概念です。さらには、オブジェクト指向プログラミングの一部を含むSystem F-サブという型理論も存在します。

サブタイピングの例

具体的な例として、UMLクラス図におけるサブタイピングの使い方を見てみましょう。ここでは「トリ」という基底型があり、「アヒル」や「カッコウ」、「ダチョウ」といった派生型があります。トリ型の変数に対して、派生した型のインスタンスを代入することができます。たとえば、下記のようにプログラムを書くことができます：

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

このように、関数`max`は数値型（Number）の引数を持ち、浮動小数点型（Float）や整数型（Integer）の値と共に計算を行います。こうした型付けは、サブタイプが上位型の特性を inheriting しているために可能になります。

性質と実装

型理論において部分型関係は「A <: B」という形式で表記されます。この場合、AがBの部分型であることを示しており、A型の式はすべてB型の式としても解釈できるという性質があります。これには、包摂（subsumption）という形式的な推論規則が適用されます。

部分型は、名前的型システムと構造的型システムの2つに分類されます。名前的型システムは、部分型として宣言されたものを部分型とするのに対し、構造的型システムは型の構造に基づいて部分型関係を評価します。オブジェクト指向言語の実装においては、通常、サブクラスによる型の派生が含まれています。

ほとんどの型システムでは部分型関係を設定しており、反射律と推移律を満たすように設計されています。これにより、型 Aが型 Bの部分型であれば、より複雑な型システムの中でも一貫してその関係が適用されることになります。

関連項目

• - ポリモーフィズム
• - 継承
• - オーバーライド
• - インターフェース

このようにサブタイピングはプログラミングの理論だけでなく、多くの実践的なアプローチにおいても重要な役割を果たしています。

もう一度検索