部分型と変性

部分型 (subtyping) は「$\alpha$ が $\tau$ の部分型 ($\alpha <:\tau$) なら $\alpha$ の項は $\tau$ としても使える」という包含関係。オブジェクト指向では subclass で表すが、型理論ではレコード型で扱うことが多い。

規則

• Subsumption: $\frac{\Gamma ⊢t:\alpha \alpha <:\tau }{\Gamma ⊢t:\tau }$
• Refl ($\iota <:\iota$)、Trans（推移律）。
• レコード: width-wise（余分なフィールドを無視、{a:Int} <: {a:Int,b:Bool} の向き）と depth-wise（各フィールドが部分型）の2通り。
• 関数: $\frac{{\alpha }^{\prime }<:\alpha \tau <:{\tau }^{\prime }}{\alpha \to \tau <:{\alpha }^{\prime }\to {\tau }^{\prime }}$。引数で依存が逆転する＝反変。

構造的部分型

構造的部分型 (structural subtyping) は名前でなく構造（フィールド集合）で部分型を判定する（例: 言語 Tin、Haskell 製 toylang）。名前的部分型と対比される。

変性 (variance)

型構築子 I<_> がパラメータの部分型関係をどう保つか:

• 共変 (covariant): B <: A ⇒ I<B> <: I<A>
• 反変 (contravariant): B <: A ⇒ I<A> <: I<B>（関数の引数位置）

Rust はリージョン推論とともに変性を扱い、Kotlin は in/out キーワード、Scala は +/- で宣言する。素朴なAlgorithm Wは単一型のみで部分型に未対応。

関連

• 土台はtype-theory-lambda-cube、推論はhindley-milner-inference。
• 言語ごとの扱いはrust-lang。
• _moc-prog-lang