サブタイピング (計算機科学)
型理論においては、部分型関係は <: と表記される。つまり、A <: B という表記は A は B の部分型であるという意味である。型理論における部分型は、A <: B ならば型 A を持つ式はどれでも型 B をも持つという事実によって特性付けられる。この形式的な推論規則は包摂(subsumption)として知られている。
型理論の研究者は、部分型であると宣言されたもののみを部分型とする名前的型システム(英語版)と、2つの型の構造によって部分型関係にあるかが決まる構造的型システム(英語版)を区別する。上記のクラスベースオブジェクト指向言語の例は名前的型システムである。構造的型システムのオブジェクト指向言語では、型 A のオブジェクトが型 B のオブジェクトの処理できるメッセージすべてを処理できるなら(言い換えると、同じメソッドを実装していれば)、継承関係に関係なく、A は B の部分型となる。
部分型を持つプログラミング言語の実装は大きく2つに分類される。型 A の値の内部表現が型 B の値としての内部表現も兼ねるinclusive(包含的)な実装と、型 A の値が型 B の値に「自動的に変換」されることのあるcoercive(強制的)な実装である。オブジェクト指向言語のサブクラスによる型の派生はたいてい包含的である。前述の整数と浮動小数点数の派生型関係は、内部表現が異なっているので、強制的な例である。
ほぼすべての型システムでは部分型関係が定義されている。それは反射律(任意の型 A について、A <: A)と推移律(A <: B かつ B <: C ならば A <: C)を満たすものである。つまり前順序が成り立つ。