型理論とλキューブ

型理論 (type theory) はλ計算に型を載せた体系群。型は項の安全性を保証し、Curry-Howard 対応により命題＝型・証明＝項として証明支援系の基盤にもなる。参考書は TaPL（『Types and Programming Languages』）。

λキューブ

Barendregt の λキューブ (lambda cube) は3軸で型システムを整理する:

• 右（項 → 型の依存）= 依存型 (dependent types)
• 上（型 → 項の多相）= パラメトリック多相
• 奥（型 → 型）= 型オペレータ / 高階の型

各頂点:

• STLC (Simply Typed Lambda Calculus): 一階命題論理に対応。
• System F (λ2): パラメトリック多相、二階命題論理。
• Calculus of Constructions (CoC): 3軸すべてを含み、高階述語論理に対応。Lean/Coq の内部言語。

型の抽象度（カインド）

カインド (kind) は型の型。Int : *、List : * -> *、Map : * -> * -> *。型パラメータを取る型を受け取る型が 高カインド型 (Higher-kinded types, HKT)（例 Functor f の f : * -> *）。TypeScript 等では HKT encoding で模倣する。

代表的な型機能

• 代数的データ型 (ADT) と一般化版 GADT。
• 存在型 (Existential Type)、RankNTypes（多相の階数）。
• 篩型 (refinement type): 述語で型に制約をかける extrinsic 機能（コントラクト）。
• 幽霊型 (phantom type): 値を持たない型パラメータで不変条件を表す。
• 多相バリアント（OCaml）、多段階計算（MetaOCaml）。
• 部分型・変性はtype-theory-lambda-cube、型推論はtype-theory-lambda-cubeへ。

関連

• 推論アルゴリズムはtype-theory-lambda-cube、部分型はtype-theory-lambda-cube。
• 実装言語はhaskell-ghc・rust-lang、証明系はproof-assistants。
• _moc-lang-compilers

存在型とそのエンコーディング

「型は未知だが何らかの具体型が存在する」ことを表す型。全称量化 (パラメトリック多相, ∀T) が「呼び出し側が型を選ぶ」のに対し、存在量化 (∃T) は「中身が型を知っているが外からは隠蔽されている」関係を表す。Tagged Union のパターンマッチを汎用関数化する際に必要になり、TypeScript には存在型が無いため回避テクニックを使う、という文脈で現れる (ts-discriminated-union-match)。

なぜ必要になるか

判別共用体 U = A | B | ... の各タグに対応する処理を持つ matchers を、match(item, key, matchers) という汎用関数で呼びたい。item: T extends U は共用体 全体 を表す型だが、matchers[item[key]] の引数は共用体の ある具体型 を要求する。両者が一致せず型エラーになる。

本来これは「item の実体は U のどれか1つの型 T である (その T が何かは静的には不明)」という 存在型 で表すべき状況。∃T. (item: T, matcher: T => void) のように、同じ未知の T で値と処理を束ねられれば安全に呼び出せる。

カプセル化によるエンコーディング

TypeScript の型システムに存在型は無いので、クロージャ (カプセル化) で隠蔽 して回避する (uhyo「カプセル化で我慢しよう」)。T を関数シグネチャの外に直接露出させず、getMatcher の内側に閉じ込める。

const getMatcher = <T extends U, U extends Record<K, string>, K extends Key>(
    item: T, key: K, matchers: Matchers<U, K>
): (item: T) => void => (item) => matchers[item[key]];
 
const match = <T extends U, U extends Record<K, string>, K extends Key>(
    item: T, key: K, matchers: Matchers<U, K>
) => getMatcher(item, key, matchers)(item);

T が結果型に現れない形にすることで、コンパイラに具体化を強制せず型エラーを解消できる。これは存在型を「ある型を内部に閉じ込めた抽象データ」として実現する古典的手法 (存在型 ≒ 情報隠蔽・モジュール) の TypeScript 版にあたる。

一般論

• 存在型は OCaml の first-class modules、Haskell の forall を伴う data Showable = forall a. Show a => MkShowable a、Rust の dyn Trait/impl Trait などで提供される。これらはいずれも「中身の型を隠して、それに対する操作だけを公開する」点で共通。
• 全称 ↔ 存在の双対性: (∃x. P(x)) → Q は ∀x. (P(x) → Q) と同型 (継続渡し/CPS によるエンコード)。上記のカプセル化も、この同型を使って存在型を全称型 (普通のジェネリック関数) に変換していると見なせる。

関連

• ts-discriminated-union-match、typeclass-monoid-intro (パラメトリック多相)、type-theory-lambda-cube、type-theory-lambda-cube。

部分型と変性

部分型 (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、推論はtype-theory-lambda-cube。
• 言語ごとの扱いはrust-lang。
• _moc-lang-compilers

Hindley-Milner型推論

Hindley-Milner (HM) 型推論は、明示的な型注釈なしに完全な型無しλ項へ主要型 (principal type) を割り当てる型推論。let多相 (let-polymorphism) を実現する型システム上で動く。

アルゴリズム

• Algorithm W: top-down なアプローチ。単一化 (unification) を使いながら型変数の代入を求める。TaPL 22章のものとは異なり型注釈を許さず、完全な型無し項に主要型を付ける。
• Algorithm M: bottom-up なアプローチ。期待型を伝播させながら推論する。
• 派生として Algorithm DW もある。
• 部分型 (subtyping) には素朴な HM は対応せず、$F_{<:}$ 等の拡張が要る。

実装

• Haskell 実装（STRef で単一化）、Julia 実装（MinCaml の型推論段）、Rust 実装 (type-theory-rs) などで写経されている。MinCaml ではこの型推論を入れるとレイトレが書ける。

関連

• 載せる型システムはtype-theory-lambda-cube、部分型拡張はtype-theory-lambda-cube。
• λ項の表現はlambda-calculus。
• _moc-lang-compilers