Quartz 5

型理論とλキューブ

Properties1
tagstype-theory, lambda-cube, system-f, dependent-types, adt, hkt

2 min read

型理論とλキューブ

型理論 (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）。
  • 部分型・変性はsubtyping-variance、型推論はhindley-milner-inferenceへ。

関連

Graph View

Backlinks