类型理论可视化实验室

通过交互式可视化探索类型系统的核心概念：从简单类型 λ 演算到 Curry-Howard 同构，覆盖 8 个关键主题。

λ-calculus Hindley-Milner Dependent Types Linear Types Subtyping Variance Effect Systems Curry-Howard
MODULE 01

简单类型 λ 演算Simply Typed λ-Calculus

Church 编码与类型推导树。每个 λ 项都有一个类型，通过 Var / Abs / App 规则构造推导。
类型推导树 / Type Derivation Tree
选择 λ 项
推导规则
MODULE 02

类型推导 — Hindley-MilnerAlgorithm W & Unification

算法 W 通过生成约束并逐步合一 (unification) 来推导表达式的最一般类型 (principal type)。
合一过程 / Unification Steps
表达式
进度
Step 0 / 0
算法 W 说明
MODULE 03

依赖类型 Π / ΣDependent Types

Π 类型（依赖函数）的返回类型依赖于输入值；Σ 类型（依赖对）的第二分量类型依赖于第一分量值。
依赖类型可视化 / Dependent Type Visualization
向量长度 n
3
概念解释
MODULE 04

线性类型Linear Types & Ownership

线性类型保证资源恰好使用一次。 a ⊸ b 表示消耗一个 a 产出 b，所有权随之转移。
资源流 / Resource Flow
使用模式
所有权语义
MODULE 05

子类型Subtyping

子类型关系 S <: T 允许在需要 T 的地方使用 S。包括宽度子类型（记录扩展）和深度子类型（字段协变）。
子类型格 / Subtype Lattice
选择类型
子类型规则
MODULE 06

泛型与变型Generics & Variance

协变 (covariant): S<:T ⇒ C<S><:C<T>；逆变 (contravariant): 方向反转；不变 (invariant): 无关系。函数类型在参数位置逆变、返回位置协变。
变型关系 / Variance Diagram
类型构造器
变型规则
MODULE 07

效应类型Effect Types & Monads

效应类型系统追踪计算中的副作用（IO、State、Exception 等），纯函数效应集为 ∅，效应通过组合传播。
效应传播 / Effect Propagation
程序片段
追踪效应
效应系统
MODULE 08

Curry-Howard 同构Propositions ↔ Types, Proofs ↔ Programs

命题即类型，证明即程序。每个逻辑连接词对应一个类型构造器，每个证明步骤对应一个程序构造。
逻辑 ↔ 类型 对应 / Correspondence
逻辑连接词
同构对照