类型系统规范

本文件定义 YaoXiang 编程语言的类型系统规范，包括基本类型、复合类型、泛型和 trait。

第零章：理论基础

0.1 Curry-Howard 同构

Curry-Howard 同构（Curry-Howard correspondence）是 YaoXiang 类型系统的理论基础。它揭示了编程语言的类型系统与数理逻辑之间的深层对应关系：

逻辑学	编程语言
命题 (P)	类型 `Type`
证明 (p: P)	程序 `x: T = ...`
蕴含 (P \rightarrow Q)	函数类型 `(P) -> Q`
合取 (P \wedge Q)	积类型 `{ a: P, b: Q }`
析取 (P \vee Q)	和类型 `{ a(P) \| b(Q) }`
全称量化 (\forall x:T. P(x))	泛型 `(T: Type) -> ...`
真 (\top)	`Void`（Unit，有默认值）
假 (\bot)	`Never`（零构造子，无任何值可居留）
类型宇宙 (Type_n : Type_{n+1})	宇宙分层（防 Russell 悖论）
case 分析	类型级 `match`

注意：类型级 match 是分类讨论（case analysis），不是数学归纳法。归纳法需要类型级递归函数 + 编译器终止性检查。

0.2 类型即命题，程序即证明

在 YaoXiang 中，这一对应关系是设计的一等原则：

终止的类型级计算对应正确的构造性证明。YaoXiang 的类型族（如 Add 在 Nat 上的 case 分析 + 递归调用）本质上是数学归纳法的类型级编码——前提是编译器能做终止性检查。
类型检查就是验证证明。当一个程序通过类型检查，相当于一个逻辑命题被构造性证明。

0.3 对语言设计的影响

Curry-Howard 同构在 YaoXiang 中的具体体现：

宇宙分层（RFC-010）：Type₀ : Type₁ : Type₂ … 避免 Type: Type 导致的逻辑悖论（Girard 悖论）
类型族（RFC-011）：自然数 Nat(Zero/Succ) 的类型级 case 分析 + 递归调用对应 Peano 公理——前提是编译器做终止性检查
条件类型（RFC-011）：If: (C: Bool, T: Type, E: Type) -> Type 对应逻辑中的 case 析取
值依赖类型（RFC-011）：Array: (T: Type, N: Int) -> Type 对应"对每个整数 N 存在一个类型"的有穷量化

第一章：类型分类

1.1 类型表达式

TypeExpr    ::= PrimitiveType
              | RecordType
              | InterfaceType
              | TupleType
              | FnType
              | GenericType
              | TypeRef
              | TypeUnion
              | TypeIntersection

设计说明：虽然 RFC-010 提出"一切皆赋值"的统一模型（name: type = value），但在语法层面，类型和值仍需区分。编译器实现中 Type 和 Expr 是两个独立的 AST 枚举（ast.rs:406 和 ast.rs:25），TypeExpr 作为 BNF 占位符对应实现中的 Type 枚举，表示"这个位置期望类型"。

第二章：基本类型

2.1 原类型

类型	逻辑对应	描述	默认大小
`Type`	—	元类型	0 字节
`Never`	⊥（假/空类型）	零构造子，无任何值。发散/panic 返回类型。`Never <: T` 对任意 T 成立。	0 字节
`Void`	⊤（真/Unit）	有默认 void 值，零字段积类型。`x: Void = <默认>` 合法。	0 字节
`Bool`	—	布尔值：`true` / `false`	1 字节
`Int`	—	有符号整数	8 字节
`Uint`	—	无符号整数	8 字节
`Float`	—	浮点数	8 字节
`String`	—	UTF-8 字符串	可变
`Char`	—	Unicode 字符	4 字节
`Bytes`	—	原始字节	可变

带位宽的整数：Int8, Int16, Int32, Int64, Int128 带位宽的浮点：Float32, Float64

2.2 Never 与 Void：⊥ 与 ⊤

Never 和 Void 是类型系统的逻辑基元——分别对应假（⊥）和真（⊤）。

Never（⊥，假/空类型） — 三条不可协商的性质：

零构造子：无任何字面量或表达式能产生 Never 类型的值。x: Never = ... 无右边可写。
爆炸原理：Never <: T 对任意类型 T 成立。assert(false) 返回 Never，之后代码可通过类型检查（虽然永不执行到）。
发散标记：f: (...) -> Never 表示 f 保证不返回。编译器据此做 dead code 分析和 match 分支合流。

Never 是内建类型名（与 Int/Bool 相同注册路径），不是关键字。

Void（⊤，真/Unit） — 恰好一个居留者（默认 void 值）。Void 是零字段积类型的幺元。x: Void = <默认> 合法。块的值由尾表达式给出（空块 {} 为 Void），详见 RFC-010a。

第三章：复合类型

3.1 记录类型

统一语法：Name: Type = { field1: Type1, field2: Type2, ... }

RecordType  ::= '{' FieldList? '}'
FieldList   ::= Field (',' Field)* ','?
Field       ::= Identifier ':' TypeExpr
            |  Identifier                 // 接口约束

yaoxiang

// 简单记录类型
Point: Type = { x: Float, y: Float }

// 空记录类型
Empty: Type = {}

// 带泛型的记录类型
Pair: (T: Type) -> Type = { first: T, second: T }

// 实现接口的记录类型
Point: Type = {
    x: Float,
    y: Float,
    Drawable,
    Serializable
}

规则：

记录类型使用花括号 {} 定义
字段名后直接跟冒号和类型
接口名写在类型体内表示实现该接口

命名空间归属：Type.name 前缀（如 Point.draw）表示函数属于 Point 的命名空间。它不触发任何隐式绑定。要让 p.draw() 这种 . 调用语法生效，必须显式绑定： Point.draw = draw[0]。详见 RFC-004 和 RFC-010。

3.1.1 字段默认值

类型字段可以指定默认值，构造时可选提供：

yaoxiang

// 有默认值的字段 - 构造时可选
Point: Type = {
    x: Float = 0,
    y: Float = 0
}

// 使用
Point()           // -> Point(x=0, y=0)
Point(x=1)       // -> Point(x=1, y=0)
Point(x=1, y=2) // -> Point(x=1, y=2)

// 无默认值的字段 - 构造时必填
Point2: Type = {
    x: Float,
    y: Float
}

// 使用
Point2(x=1, y=2) // 正确
Point2()          // 错误

规则：

field: Type = expression -> 有默认值，构造时可选
field: Type -> 无默认值，构造时必填

3.1.2 内置绑定

在类型定义体内可以直接绑定方法：

yaoxiang

// 方式1：引用外部函数绑定
distance: (a: Point, b: Point) -> Float = { ... }
Point: Type = {
    x: Float = 0,
    y: Float = 0,
    distance = distance[0]    // 绑定到位置0
}
// 调用：p1.distance(p2) -> distance(p1, p2)

// 方式2：匿名函数 + 位置绑定
Point: Type = {
    x: Float = 0,
    y: Float = 0,
    distance: ((a: Point, b: Point) -> Float)[0] = ((a, b) => {
        dx = a.x - b.x
        dy = a.y - b.y
        return (dx * dx + dy * dy).sqrt()
    })
}
// 语法：((params) => body)[position]
// 调用：p1.distance(p2) -> distance(p1, p2)

3.2 接口类型

InterfaceType ::= '{' FnField (',' FnField)* ','?
FnField       ::= Identifier ':' FnType
FnType        ::= '(' ParamTypes? ')' '->' TypeExpr

语法：接口是字段全为函数类型的记录类型

yaoxiang

// 接口定义
Drawable: Type = {
    draw: (Surface) -> Void,
    bounding_box: () -> Rect
}

Serializable: Type = {
    serialize: () -> String
}

// 空接口
EmptyInterface: Type = {}

接口实现：类型通过在定义末尾列出接口名来实现接口

yaoxiang

// 实现接口的类型
Point: Type = {
    x: Float,
    y: Float,
    Drawable,        // 实现 Drawable 接口
    Serializable     // 实现 Serializable 接口
}

接口直接赋值：具体类型可以直接赋值给接口类型变量（结构化子类型）

yaoxiang

// 直接赋值（编译期可确定具体类型 -> 零开销调用）
d: Drawable = Circle(1)
d.draw(screen)        // 编译后：直接调用 circle_draw，无 vtable

// 函数返回值（编译期无法确定 -> vtable 调用）
d: Drawable = get_shape()
d.draw(screen)        // 通过 vtable 查找方法

// 接口作为函数参数
process: (d: Drawable) -> Void = d.draw(screen)

编译期优化策略：

场景	推断结果	调用方式
直接赋值具体类型	具体类型可确定	直接调用（零开销）
函数返回值	未知	vtable
异构集合	多个类型	vtable

连贯性与孤儿规则（不适用，收口说明）：YaoXiang 的接口是结构化类型（接口 = 字段全为函数类型的记录），不是名义 trait——不存在跨 crate/模块的"谁可以为谁实现" 归属问题，Rust 式孤儿规则与连贯性检查没有适用对象（裁决记录见 RFC-011 §2.1）。结构化世界的对应保障是重复实现拒绝：同一方法签名在类型上重复定义编译报错（RFC-011a §3，禁止覆盖；重载合法）。

3.4 元组类型

TupleType   ::= '(' TypeList? ')'
TypeList    ::= TypeExpr (',' TypeExpr)* ','?

3.5 函数类型

FnType      ::= '(' ParamList? ')' '->' TypeExpr
ParamList   ::= TypeExpr (',' TypeExpr)*

第四章：泛型

4.1 泛型参数语法

泛型参数是函数类型的一部分，与普通参数统一使用 () 语法：

GenericType     ::= Identifier '(' TypeArgList ')'
TypeArgList     ::= TypeExpr (',' TypeExpr)* ','?
TypeBound       ::= Identifier
                 |  Identifier '+' Identifier ('+' Identifier)*

泛型类型定义中，(T: Type) 是类型构造器的参数签名，-> Type 表示返回类型：

yaoxiang

List: (T: Type) -> Type = { ... }
Map: (K: Type, V: Type) -> Type = { ... }

4.1.1 容器类型

容器类型是泛型类型构造器，不是内置原语——与用户自定义泛型同一待遇，经由统一的泛型实例化路径处理。长度信息的归属是三个容器概念的根本区别：

类型	长度	语义	底座
`Array(T, N)`	类型	定长数组（const 泛型 N）	核心原语（栈/内联优先）
`Vec(T)`	运行时值	运行时长度的原始缓冲，可增长	核心原语（堆上连续缓冲）
`List(T)`	运行时值	标准库类型（可增长列表）	库：`{ data: Vec(T), length: Int }`
`Dict(K, V)`	运行时值	键值映射	`HeapValue::Dict`

List(T) 是标准库类型，不是编译器原语：由 YaoXiang 自身在 std.list 中定义，与用户自定义泛型记录同一待遇。可增长语义的全部策略（何时扩容、扩多少、能否共享）都在库里，编译器不参与。 Vec(T) 是它依赖的最小地基原语。
Set(T) 已除名：无字面量、无运行时表示、无 std.set。需求出现时照 Dict 模式补全。

关键规则：

字面量落点由上下文决定：[...] 裸字面量与 List(T) 注解落可增长列表；Array(T, N) 注解直接作用于字面量时落定长数组。落点校验：元素个数 == N、元素类型兼容 T，不符编译期 E1002；N 为符号常量（const 参数）时个数校验推迟到精化类型阶段。
禁止隐式 List→Array 转换：定长性由类型层保证——push 只接受 List(A) receiver。
性能层次：由底向上性能递减、灵活性递增：Array > Vec > List。
索引失败契约（运行时报错为过渡态，目标态编译期精化覆盖，走值依赖类型，见 §8.4）：
- 索引越界（含负索引）→ E6003
- Dict 缺键 → E6008
membership in 谓词：返回 Bool 不报错，右操作数覆盖List/Array/Dict(键)/Tuple/String/Range。一等霍尔谓词，是精化类型编译期可证命题的基底。`

泛型函数中，类型参数同样在签名中声明，编译器自动从实参推断：

yaoxiang

map: (T: Type, R: Type) -> ((list: List(T), f: (T) -> R) -> List(R)) = ...

4.2 泛型类型定义

yaoxiang

// 基础泛型类型
Option: (T: Type) -> Type = {
    some: (T) -> Option(T),
    none: () -> Option(T)
}

Result: (T: Type, E: Type) -> Type = {
    ok: (T) -> Result(T, E),
    err: (E) -> Result(T, E)
}

List: (T: Type) -> Type = {
    data: Array(T),
    length: Int,
    push: (self: List(T), item: T) -> Void,   // self 只是约定名，不是关键字
    get: (self: List(T), index: Int) -> Option(T)
}

4.3 泛型构造调用与类型推导

泛型类型定义的字段列表自动生成构造函数：每个字段对应一个构造参数，字段名即参数名；有默认值的字段构造时可省略，无默认值的字段必填。函数类型字段（方法）不生成构造参数。

yaoxiang

// 类型定义
Container: (T: Type) -> Type = {
    value: T,        // 无默认值 → 构造参数必填
    extra: T,
}
// 自动展开的完整形式（编译器内部视图，不要求用户手写）：
// Container: (T: Type) -> (value: T, extra: T) -> Type = {
//     value: T = value,
//     extra: T = extra,
// }

// 调用：调用自动生成的构造函数
c  = Container(42, 43)            // 构造参数按字段顺序填；T 从元素自动解包 = Int
c2 = Container("a", "b")          // T = String
c3 = Container(Int)(42, 43)       // 显式类型参数 + 位置式构造参数
c4 = Container(Int)(extra=43, value=42)  // 字段名式，顺序任意
c5 = Container(Int)()             // 空构造：字段取默认值/零值（数据事后赋值）

// 字段默认值 → 构造参数可省略
Point: (T: Type) -> Type = { x: T = 0, y: T = 0 }
p  = Point(1.5, 2.5)              // T = Float，x←1.5, y←2.5
p2 = Point(Int)()                 // x=0, y=0

调用规则（单括号，按声明参数逐位匹配，自左向右）：

实参逐位尝试匹配类型声明参数：Type 位接受类型实参，编译期值参数位（如 Int）接受编译期常量。
若存在编译期值参数位匹配成功（部分匹配），按类型构造处理：逐位检查全部参数位，报错时按声明顺序先报第一个不匹配/缺失的参数。
若实参完全对应不上声明参数（全部是值、无编译期值参数位可匹配），按构造参数处理：位置式按字段顺序填，类型参数从元素类型自动解包。

yaoxiang

Matrix: (T: Type, Rows: Int, Cols: Int) -> Type = {
    _assert_rows: Assert(Rows > 0),
    data: Array(Array(T, Cols), Rows),
}

m: Matrix(Int, 3, 4)              // 类型位置：一层类型构造
m2 = Matrix(Int, 3, 4)(data=[[1,2,3,4],[5,6,7,8],[9,10,11,12]])  // 两层：类型 + 构造参数
m3 = Matrix(Int, 3, 4)()          // 空构造（RFC-011 §9.3 模式，数据事后赋值）

Matrix(42)    // ❌ 位0: T←42 不匹配（42 不是类型）；位1: Rows←42 匹配；
              //    位2: Cols 缺失 → 先报第一个错误：T 期望 Type，找到 42
Container(42) // ❌ 缺构造参数 extra
Container(42, 43, 44)  // ❌ 构造参数超数

类型推导：泛型类型构造器的类型参数从构造参数元素自动解包（Container(42, 43) → T=Int）；泛型函数的类型参数从实参类型自动解包（map(numbers, f) → T=Int, R=String，见 §4.1）。无法解包时必须显式填充。

第五章：类型约束

5.1 单一约束

ConstrainedType ::= '(' Identifier ':' TypeBound ')' TypeExpr

yaoxiang

// 接口类型定义（作为约束）
Clone: Type = {
    clone: () -> Clone
}

// 使用约束
clone: (T: Clone)(value: T) -> T = value.clone()

5.2 多重约束

约束的求解来源（RFC-011b）：运算符约束名（Add / Subtract / Multiply / Divide / Modulo / Equal / Index）的求解 = 查接口实现登记表—— T: Add ≜ 已登记 Add(T, T, T) 实例化；Equal 另有结构推导（全字段可比的记录自动可比）。Zero / One / PartialOrd 等名字尚未有定义来源，属悬空约束名。

yaoxiang

// 多重约束语法
combine: (T: Clone + Add)(a: T, b: T) -> T = {
    a.clone() + b
}

// 泛型容器的排序
sort: (T: Clone + PartialOrd)(list: List(T)) -> List(T) = {
    result = list.clone()
    quicksort(&mut result)
    return result
}

5.3 函数类型约束

yaoxiang

// 高阶函数约束
call_twice: (T: Type, F: () -> T)(f: F) -> (T, T) = (f(), f())

compose: (A: Type, B: Type, C: Type, F: (A) -> B, G: (B) -> C)(a: A, f: F, g: G) -> C = g(f(a))

第六章：关联类型

6.1 关联类型定义

AssociatedType ::= Identifier ':' TypeExpr

yaoxiang

// Iterator trait（使用记录类型语法）
Iterator: (T: Type) -> Type = {
    Item: T,                    // 关联类型
    next: () -> Option(T),
    has_next: () -> Bool
}

// 使用关联类型
collect: (T: Type, I: Iterator(T))(iter: I) -> List(T) = {
    result = List(T)()
    while iter.has_next() {
        if let Some(item) = iter.next() {
            result.push(item)
        }
    }
    return result
}

6.2 泛型关联类型（GAT）

yaoxiang

// 更复杂的关联类型
Container: (T: Type) -> Type = {
    Item: T,
    IteratorType: Iterator(T),  // 关联类型也是泛型的
    iter: () -> IteratorType
}

第七章：编译期泛型

7.1 编译期值参数

LiteralType   ::= Identifier ':' Int          // 编译期常量（候选）

判断依据是在类型位置被引用，而非「标注了具体类型」：add: (a: Int, b: Int) -> Int = a + b 中 a/b 是运行时值参数（二者未出现在任何类型位置）。

术语：标注非 Type 具体类型（如 Int）的泛型参数称为编译期值参数候选，是否成为编译期值参数取决于其值是否在类型位置被引用（值依赖）。无需 const 关键字 （实现内部曾用「const 泛型」指代，文档统一使用「编译期值参数」）。

判定规则（两步）：

形态粗筛：参数标注非 Type 的具体类型（Int/Bool/Float）→ 候选。
用途精筛：候选名出现在类型位置（类型体字段类型、内层 Fn 参数类型、 Assert 谓词、Array(T, N) 类型构造实参位）→ 真编译期值参数；否则运行时值参数。

写法	判定	原因
`add: (a: Int, b: Int) -> Int = a + b`	a/b 运行时值参数	仅在值位置出现
`Array: (T: Type, N: Int) -> Type = { data: Array(T, N) }`	N 编译期值参数	N 在类型构造实参位
`factorial: (N: Int) -> (k: N) -> Int`	N 编译期值参数	N 作内层参数 k 的类型
`Foo: (T: Type, N: Int) -> Type = { x: T }`	N 落空→运行时值参数	N 未在类型体引用

核心设计：用 (N: Int) 编译期值参数 + (k: N) 值参数，区分编译期常量与运行时值。落空候选（形态是候选、用途未命中）退化为运行时值参数——函数级与类型构造器路径均按此处理。

yaoxiang

// 编译期值参数：N 在类型位置（Array 长度槽）被引用
Measure: (T: Type, N: Int) -> Type = {
    data: Array(T, N),      // N 出现在类型构造实参位 → 编译期值参数
    length: N
}

// 使用方式：factorial(5) 在类型位置求值（编译期），结果 120 嵌入类型
arr: Measure(Int, factorial(5))  // 编译器在编译期计算 factorial(5) = 120

// 值依赖：N 作为内层参数 k 的类型
// N 是编译期值参数（出现在 (k: N) 的类型位）；
// k 是运行时值参数，其类型为字面量类型 N（单值类型）。
factorial: (N: Int) -> (k: N) -> Int = {
    match k {
        0 => 1,
        _ => k * factorial(k - 1)
    }
}

7.2 编译期常量数组

yaoxiang

// 矩阵类型使用
Matrix: (T: Type, Rows: Int, Cols: Int) -> Type = {
    data: Array(Array(T, Cols), Rows)
}

// 编译期维度验证
identity_matrix: (T: Add + Zero + One, N: Int)(size: N) -> Matrix(T, N, N) = {
    // ...
}

第八章：条件类型

8.1 If 条件类型

IfType        ::= 'If' '(' BoolExpr ',' TypeExpr ',' TypeExpr ')'

yaoxiang

// 类型级 If
If: (C: Bool, T: Type, E: Type) -> Type = match C {
    True => T,
    False => E
}

// 示例：编译期分支
NonEmpty: (T: Type) -> Type = If(T != Void, T, Never)
// IsTrue 桥接与 Assert 精化类型（详见 §8.3）
IsTrue: (b: Bool) -> Type = match b {
    true => Void,      // ⊤，程序继续
    false => Never,    // ⊥，发散/编译错误
}
Assert: (cond: Bool) -> Type = IsTrue(cond)

8.2 类型族

yaoxiang

// 编译期类型转换
AsString: (T: Type) -> Type = match T {
    Int => String,
    Float => String,
    Bool => String,
    _ => String
}

8.3 Assert 精化类型与 assert 断言

assert 和 Assert 是同一精化原语的两面——由 dispatch 分派管道按"谓词自由变量编译期是否可及"自动选择。

核心签名：assert: (cond: Bool, ?msg: String | Error) -> Assert(IsTrue(cond))

dispatch 分派规则：

判据	模式	行为
所有自由变量编译期已知（泛型参数、编译期常量）	CompileTime	进证明管道：true → 擦除为 Void，false → 编译错误（Never 不可居留）
存在运行时自由变量（函数参数、外部输入）	Runtime	插入运行时 Bool 检查，向流敏感假设集 Γ 注入精化事实

流敏感假设集 Γ：

编译器维护每个控制流点的已知命题集合：

yaoxiang

assert(x > 0)       // Γ = {x > 0}
y = x + 1           // Γ = {x > 0, y > 1}  ← SP 传播
mut x = x - 5       // Γ = {}  ← mut kill set：旧假设失效

mut 变量赋值后，涉及该变量的所有假设被移除（kill set）。分支合流时 Γ 取各分支交集。

8.4 Terminates：终止测度谓词

Terminates 是内置谓词，与 Int、Never 同属核心原语（内建名，不是关键字）。它把一个测度绑定到一段计算上，声明该计算终止，并给出终止的见证。

形态：两个元数，同一个谓词：

形态	锚点	用途
`Terminates(m)`	所在绑定的名字	默认形态——自递归函数、循环
`Terminates(FnType, m)`	显式函数类型	需显式指明测度归属时（测度定义在别处、同一测度服务多个计算）

yaoxiang

// 测度：普通函数，可单测、可复用，不参与运行时
gcd_measure: (a: Int, b: Int) -> Int = { b }

// 二元形态：测度定义在别处，显式指明归属
gcd: Terminates((a: Int, b: Int) -> Int, gcd_measure) = {
    if b == 0 { return a }
    return gcd(b, a % b)
}

// 一元形态：锚点即绑定名，测度是作用域内的表达式
loop: (n: Int) -> Int = {
    mut i = 0
    acc: Terminates(n - i) = while i < n {
        i = i + 1
    }
    return acc
}

语义：Terminates(m) 精化的就是它所在类型位所标注的那段计算的值类型。义务落在该计算上——函数落在每个递归调用点，循环落在回边——均为「下一状态的测度严格小于当前状态的测度」，并在该点的路径守卫下判定。

调用点的义务为 m(callee_args) < m(caller_args)；回边的义务为 m(下一轮) < m(本轮)。两者形式同一。

为何覆盖循环：循环是匿名构造，通常无法被指称。绑定名即是名字——acc: Terminates(n - i) = while ... 中的 acc 提供了锚点，循环因此可指称。这是 Terminates 一元形态作用于循环的理由。

测度：不限制返回类型（不强制自然数）；其上的「严格递减」由该类型上可用的适定序给出。测度是否良基（如返回 Int 时是否 >= 0）是一条独立的义务，与递减义务同样由编译期证明管道判定。

触发：终止检查由精化类型触发——类型一旦被精化即进验证模式。未被精化的普通类型（如裸 while 循环、无精化签名的函数）不进验证模式，不生成终止义务。

自动探索优先：编译器先自动探索测度（线性秩函数、谓词违反计数、有界递增递减、乘法缩放四个模板），探索不出时才需要显式给出 Terminates。

运行时表示：纯编译期实体，随 witness 擦除，不进运行时二进制。

完整设计见 RFC-027 §6.9（语义）与 RFC-027a（落地机制）。

第九章：类型联合与交集

9.1 类型联合

TypeUnion     ::= TypeExpr '|' TypeExpr

9.2 类型交集

TypeIntersection ::= TypeExpr '&' TypeExpr

语法：类型交集 A & B 表示同时满足 A 和 B 的类型

yaoxiang

// 接口组合 = 类型交集
DrawableSerializable: Type = Drawable & Serializable

// 使用交集类型
process: (T: Drawable & Serializable)(item: T, screen: Surface) -> String = {
    item.draw(screen)
    return item.serialize()
}

第十章：函数重载与特化

10.1 函数重载

yaoxiang

// 基本特化：使用函数重载（编译器自动选择）
sum: (arr: Array(Int)) -> Int = {
    return native_sum_int(arr.data, arr.length)
}

sum: (arr: Array(Float)) -> Float = {
    return simd_sum_float(arr.data, arr.length)
}

// 通用实现
sum: (T: Add)(arr: Array(T)) -> T = {
    result = Zero::zero()
    for item in arr {
        result = result + item
    }
    return result
}

10.2 平台特化

yaoxiang

// 平台类型枚举（标准库定义）
Platform: Type = { X86_64: () -> Platform, AArch64: () -> Platform, RISC_V: () -> Platform, ARM: () -> Platform, X86: () -> Platform }

// P 是预定义泛型参数名，代表当前编译平台
sum: (P: X86_64)(arr: Array(Float)) -> Float = {
    return avx2_sum(arr.data, arr.length)
}

sum: (P: AArch64)(arr: Array(Float)) -> Float = {
    return neon_sum(arr.data, arr.length)
}

第十一章：类型属性

YaoXiang 只有一种类型属性需要区分：线性 vs 可复制。由编译器自动推导。

11.1 Move（默认所有权转移）

所有类型默认遵循 Move 语义。赋值、传参、返回 = 所有权转移。

yaoxiang

p: Point = Point(1.0, 2.0)
q = p           // Move，p 不可再读

11.2 Dup（浅拷贝：复制句柄，共享数据）

Dup 属性用于引用/令牌类型。Dup 类型的赋值 = 浅拷贝——复制句柄/令牌，底层数据共享。多个持有者指向同一块数据。

类型	属性	说明
`&T`	Dup	零大小读取令牌，复制令牌 = 多个视角指向同一数据
`ref T`	Dup	Rc/Arc 复制 = 引用计数+1，共享堆数据
`&mut T`	Linear	零大小写入令牌，独占，不可复制
其他所有类型	Move	默认所有权转移

原语值类型（Int, Float, Bool, Char）是编译器内置的特殊处理：赋值时自动值复制，两个值完全独立。这是编译器的原生行为，不属于 Dup 类型属性。

yaoxiang

// &T: Dup，可自由别名
view: &Point = &p
view2 = view     // Dup：复制令牌，两者均有效
print(view.x)    // 可用
print(view2.x)   // 可用

// &mut T: Linear，不可复制
mut_ref: &mut Point = &mut p
// r2 = mut_ref  // ❌ &mut T 不是 Dup，不能复制

11.3 Clone（显式深复制）与 Dup 的关系

Clone 是显式深复制接口。所有类型都可以实现 Clone，提供 .clone() 方法。

yaoxiang

// Clone 接口定义（标准库）
Clone: Type = {
    clone: () -> Clone
}

// 使用
p: Point = Point(1.0, 2.0)
backup = p.clone()    // 深复制，p 仍然可用
p2 = p.clone()        // 可多次克隆

Dup 与 Clone 的区别：

	Dup	Clone
语义	浅拷贝：复制句柄/令牌，底层数据共享	深拷贝：创建完整独立副本
调用方式	隐式（赋值/传参自动）	显式（`.clone()`）
修改影响	互相影响（共享底层数据）	互不影响（独立副本）
适用类型	`&T` 令牌、`ref T`	任何实现 Clone 接口的类型
成本	零开销（令牌是零大小类型）	视类型而定

Dup 不蕴含 Clone，Clone 不蕴含 Dup——它们是两个正交的概念：

yaoxiang

// Dup 类型：复制令牌，底层数据共享
view: &Point = &p
view2 = view        // Dup：复制令牌，两者指向同一个 p
print(view.x)       // 可用
print(view2.x)      // 可用，看到的是同一份数据

// 原语值类型：编译器自动值复制（不是 Dup）
x: Int = 42
y = x               // 值复制，x 和 y 完全独立
print(x)            // 可用

// Clone：显式深拷贝，创建独立副本
p: Point = Point(1.0, 2.0)
q = p.clone()       // Clone：深复制，p 仍然可用
r = p               // Move：所有权转移，因为 Point 不是 Dup 也不是原语值类型

设计意图：

Dup 用于令牌/引用类型，解决"多个视角看同一份数据"的问题
Clone 用于需要独立副本的场景，显式调用让成本可见
原语值类型（Int/Float/Bool/Char）的复制是编译器内置行为，不属于 Dup
大多数自定义类型默认 Move，零拷贝高性能

第十二章：借用令牌类型

12.1 核心概念

&T 和 &mut T 是零大小的编译期令牌类型。它们不是"引用"，而是"访问权限的类型级证明"。

&T      →  零大小，冻结源数据（禁止 WriteToken 在此期间获取），
          冻结保证下多份只读安全 → Dup（可复制）
&mut T  →  零大小，独占读写（禁止任何其他令牌），
          独占访问下复制无意义 → Linear（非 Dup）

关键特性：

令牌是普通类型，遵循和所有其他类型一样的作用域规则
不需要生命周期标注 'a
不需要专用借用检查器——类型属性（Dup/Linear）自然推导权限
编译后完全消失，零运行时开销

12.2 基本使用

yaoxiang

// 方法端：声明参数类型，决定需要的权限
Point.print: (self: &Point) -> Void = {
    print(self.x)               // &Point 令牌授予读权限
    print(self.y)
}

Point.shift: (self: &mut Point, dx: Float, dy: Float) -> Void = {
    self.x = self.x + dx        // &mut Point 令牌授予写权限
    self.y = self.y + dy
}

// 调用端：编译器自动选择借用或 Move
p = Point(1.0, 2.0)
p.print()                       // 编译器自动创建 &Point 令牌
p.shift(1.0, 1.0)               // 编译器自动创建 &mut Point 令牌
p.print()                       // OK，上一个令牌已随 shift 调用结束而释放

// 多个 &T 令牌共存——Dup 类型允许自由复制
distance: (a: &Point, b: &Point) -> Float = {
    sqrt((a.x - b.x)**2 + (a.y - b.y)**2)
}
d = distance(p, p2)

12.3 令牌的作用域与传播

令牌是普通类型，因此支持所有普通类型的操作：

返回令牌——令牌随返回值一起传播：

yaoxiang

// ✅ 子令牌和父令牌一起返回
Point.get_x: (self: &Point) -> (&Float, &Point) = {
    return (&self.x, self)
}

p = Point(1.0, 2.0)
(px_ref, p) = p.get_x()        // 令牌返回给调用者
print(px_ref)                    // OK，令牌仍在作用域

存结构体——结构体可以携带令牌字段：

yaoxiang

// ✅ 结构体携带令牌作为字段
Window: Type = {
    target: Point,
    view: &Point,              // 令牌字段——持有对 target 的只读视图
}

闭包不捕获，上下文在创建点固化——闭包只吃自己的参数，需要外层数据时通过柯里化在创建点把值固化进闭包：

yaoxiang

// ✅ 上下文经柯里化固化：threshold 是参数，gt_point(threshold) 在创建点把值固化进闭包
gt_point: (t: Float) -> (p: Point) -> Bool = (p) => p.x > t
filter_by_threshold: (items: List(Point), threshold: Float) -> List(Point) = {
    items.filter(gt_point(threshold))
}

注：闭包（函数值）逃逸后其定义处作用域可能已死，故不得隐式捕获外层变量；但调用点（创建点）作用域必然存活，上下文在该点固化为值进入闭包是安全的。

12.4 自动借用选择

调用端编译器按以下优先级自动选择：

1. 如果实参后续还有使用 → 优先创建令牌（&T 或 &mut T，根据方法签名）
2. 如果实参后续不再使用 → Move
3. 优先匹配顺序：&T < &mut T < Move

yaoxiang

p = Point(1.0, 2.0)
p.print()          // print 的参数类型为 &Point → 编译器创建 &Point 令牌
p.shift(1.0, 1.0)  // shift 的参数类型为 &mut Point → 编译器创建 &mut Point 令牌
p2 = p             // 后续不再使用 → Move

方法接收者跟随签名语义（RFC-011a 接收者拼写约定同款）：接收者是 &T → 只读借用令牌；&mut T → 可变借用令牌；按值 → Move（消费接收者）。调用点产生的借用令牌随调用结束释放（transient，§12.5 区间语义）；接口的借用接收者由接口作者显式声明 &Self，impl 签名经 Self ↦ impl 类型 替换后须与接口完全一致（RFC-011a §3）。

12.5 令牌冲突检测

令牌冲突检测是借用霍尔命题（RFC-009a），不是独立的流敏感分析。编译器自动生成借用命题（borrow_conflict/use_after_move/use_after_drop/mut_violation）送入证明管道验证；令牌活性是区间 [created_at, last_use]（见 RFC-009a §反向 BFS 活性分析）：

yaoxiang

// ❌ &mut 和派生的 &T 不能同时活跃
bad_alias: (p: &mut Point) -> Void = {
    p.x = 10.0                   // ✅ 正常使用 WriteToken
    print(p.y)
}

// ✅ 令牌作用域结束后自动释放
good_seq: (p: &mut Point) -> Void = {
    {
        // 内部作用域
        print(p.x)               // 使用 &mut Point
    }
    // 内部作用域结束
    p.x = 10.0                   // ✅ WriteToken 仍可用
}

// ❌ 同一实参不能同时创建 &mut 令牌和其他令牌
alias_bad: (a: &mut Point, b: &Point) -> Void = { ... }
p = Point(1.0, 2.0)
alias_bad(p, p)                  // ❌ p 同时派生 &mut 和 & 令牌

12.6 编译器内部：品牌机制

用户从不接触品牌。编译器在内部为每个令牌分配编译期唯一标识：

用户看到的           编译器内部表示
────────────────────────────────────────
&Point         →  ReadToken(Point, #N)    // #N 是编译期唯一整数
&mut Point     →  WriteToken(Point, #M)   // #M 是编译期唯一整数

品牌的用途：

防伪造：令牌只能从所有者胶囊获得，不能凭空构造
关联追踪：字段访问派生的 &Float 携带派生品牌（#N.field_x），编译器可追踪到父令牌
冲突检测：同源 WriteToken 和派生 ReadToken 不能同时活跃

品牌在单态化和内联后完全消失，生成的机器码中不存在。零运行时开销。

12.7 令牌 Sum 类型

&BorrowToken ::= &T          // ReadToken（冻结源数据 → Dup 安全）
               | &mut T      // WriteToken（独占读写 → Linear）

12.8 借用令牌 vs ref

	`&T` / `&mut T`	`ref`
做什么	看一眼/原地改	共享持有
范围	随令牌值的作用域	跨作用域
成本	零开销（零大小类型，编译后消失）	Rc 或 Arc（编译器选）
逃逸	可（令牌随返回值/结构体传播）	本来就是用来逃逸的
跨任务	不可（令牌未实现跨任务传递）	可（编译器自动选 Arc）
环检测	不涉及	任务内静默，跨任务 lint

注（未定义）：ref 创建后如何读内容（解引用/方法/自动）尚未在规范中定义，实现现状 *a 报 E1052。待定义后补入本节。

附录：类型定义速查

A.1 类型定义

// === 记录类型（花括号） ===

// 记录类型
Point: Type = { x: Float, y: Float }

// 带变体的记录类型（使用函数字段）
Result: (T: Type, E: Type) -> Type = { ok: (T) -> Result(T, E), err: (E) -> Result(T, E) }

// === 接口类型（花括号，字段全为函数） ===

// 接口定义
Serializable: Type = { serialize: () -> String }

// 实现接口的类型
Point: Type = {
    x: Float,
    y: Float,
    Serializable    // 实现 Serializable 接口
}

// === 函数类型 ===

Adder: Type = (Int, Int) -> Int

// === 终止测度（内置谓词，见 §8.4） ===

// 一元：锚点即绑定名（自递归函数、循环）
loop: (n: Int) -> Int = {
    mut i = 0
    acc: Terminates(n - i) = while i < n { i = i + 1 }
    return acc
}

// 二元：显式指明测度归属（测度定义在别处）
gcd_measure: (a: Int, b: Int) -> Int = { b }
gcd: Terminates((a: Int, b: Int) -> Int, gcd_measure) = {
    if b == 0 { return a }
    return gcd(b, a % b)
}

A.2 泛型语法

// 泛型类型
List: (T: Type) -> Type = { data: Array(T), length: Int }
Result: (T: Type, E: Type) -> Type = { ok: (T) -> Result(T, E), err: (E) -> Result(T, E) }

// 泛型函数
map: (T: Type, R: Type)(list: List(T), f: (T) -> R) -> List(R) = { ... }

// 类型约束
clone: (T: Clone)(value: T) -> T = value.clone()
combine: (T: Clone + Add)(a: T, b: T) -> T = body

// 关联类型
Iterator: (T: Type) -> Type = { Item: T, next: () -> Option(T) }

// 编译期泛型：N 在类型位置 (k: N) 被引用 → 编译期值参数
factorial: (N: Int)(k: N) -> Int = { ... }
Measure: (T: Type, N: Int) -> Type = { data: Array(T, N), length: N }

// 条件类型
If: (C: Bool, T: Type, E: Type) -> Type = match C { True => T, False => E }

// 函数特化
sum: (arr: Array(Int)) -> Int = { ... }
sum: (arr: Array(Float)) -> Float = { ... }

A.3 类型属性速查

// === Move（默认） ===
// 所有类型默认 Move。赋值、传参、返回 = 所有权转移

// === 原语值类型（编译器内置） ===
Int, Float,     // 赋值时自动值复制，两个值完全独立
Bool, Char      // 不是 Dup，是编译器对原语的内置处理

// === Dup（浅拷贝：复制句柄，共享底层数据） ===
&T              // 零大小读取令牌，复制令牌 = 多个视角指向同一数据
ref T           // Rc/Arc 复制 = 引用计数+1，共享堆数据

// === Linear ===
&mut T          // 零大小写入令牌，Linear（独占，不可复制）

// === Clone（显式深复制） ===
value.clone()   // 创建独立副本，修改不影响原值

A.4 借用令牌速查

// === 借用令牌 ===
&T              // 零大小编译期读令牌，冻结源数据 → Dup（可复制）
&mut T          // 零大小编译期写令牌，独占读写 → Linear（不可复制）

// 调用端自动选择
// 1. 实参后续还有使用 → 创建令牌
// 2. 实参后续不再使用 → Move
// 3. 优先匹配：&T < &mut T < Move

// 令牌传播
// ✅ 可返回、可存结构体、可被闭包捕获
// ❌ 不可跨任务（令牌未实现跨任务传递）

类型系统规范 ​

第零章：理论基础 ​

0.1 Curry-Howard 同构 ​

0.2 类型即命题，程序即证明 ​

0.3 对语言设计的影响 ​

第一章：类型分类 ​

1.1 类型表达式 ​

第二章：基本类型 ​

2.1 原类型 ​

2.2 Never 与 Void：⊥ 与 ⊤ ​

第三章：复合类型 ​

3.1 记录类型 ​

3.1.1 字段默认值 ​

3.1.2 内置绑定 ​

3.2 接口类型 ​

3.4 元组类型 ​

3.5 函数类型 ​

第四章：泛型 ​

4.1 泛型参数语法 ​

4.1.1 容器类型 ​

4.2 泛型类型定义 ​

4.3 泛型构造调用与类型推导 ​

第五章：类型约束 ​

5.1 单一约束 ​

5.2 多重约束 ​

5.3 函数类型约束 ​

第六章：关联类型 ​

6.1 关联类型定义 ​

6.2 泛型关联类型（GAT） ​

第七章：编译期泛型 ​

7.1 编译期值参数 ​

7.2 编译期常量数组 ​

第八章：条件类型 ​

8.1 If 条件类型 ​

8.2 类型族 ​

8.3 Assert 精化类型与 assert 断言 ​

8.4 Terminates：终止测度谓词 ​

第九章：类型联合与交集 ​

9.1 类型联合 ​

9.2 类型交集 ​

第十章：函数重载与特化 ​

10.1 函数重载 ​

10.2 平台特化 ​

第十一章：类型属性 ​

11.1 Move（默认所有权转移） ​

11.2 Dup（浅拷贝：复制句柄，共享数据） ​

11.3 Clone（显式深复制）与 Dup 的关系 ​

第十二章：借用令牌类型 ​

12.1 核心概念 ​

12.2 基本使用 ​

12.3 令牌的作用域与传播 ​

12.4 自动借用选择 ​

12.5 令牌冲突检测 ​

12.6 编译器内部：品牌机制 ​

12.7 令牌 Sum 类型 ​

12.8 借用令牌 vs ref ​

附录：类型定义速查 ​

A.1 类型定义 ​

A.2 泛型语法 ​

A.3 类型属性速查 ​

A.4 借用令牌速查 ​

类型系统规范

第零章：理论基础

0.1 Curry-Howard 同构

0.2 类型即命题，程序即证明

0.3 对语言设计的影响

第一章：类型分类

1.1 类型表达式

第二章：基本类型

2.1 原类型

2.2 Never 与 Void：⊥ 与 ⊤

第三章：复合类型

3.1 记录类型

3.1.1 字段默认值

3.1.2 内置绑定

3.2 接口类型

3.4 元组类型

3.5 函数类型

第四章：泛型

4.1 泛型参数语法

4.1.1 容器类型

4.2 泛型类型定义

4.3 泛型构造调用与类型推导

第五章：类型约束

5.1 单一约束

5.2 多重约束

5.3 函数类型约束

第六章：关联类型

6.1 关联类型定义

6.2 泛型关联类型（GAT）

第七章：编译期泛型

7.1 编译期值参数

7.2 编译期常量数组

第八章：条件类型

8.1 If 条件类型

8.2 类型族

8.3 Assert 精化类型与 assert 断言

8.4 Terminates：终止测度谓词

第九章：类型联合与交集

9.1 类型联合

9.2 类型交集

第十章：函数重载与特化

10.1 函数重载

10.2 平台特化

第十一章：类型属性

11.1 Move（默认所有权转移）

11.2 Dup（浅拷贝：复制句柄，共享数据）

11.3 Clone（显式深复制）与 Dup 的关系

第十二章：借用令牌类型

12.1 核心概念

12.2 基本使用

12.3 令牌的作用域与传播

12.4 自动借用选择

12.5 令牌冲突检测

12.6 编译器内部：品牌机制

12.7 令牌 Sum 类型

12.8 借用令牌 vs ref

附录：类型定义速查

A.1 类型定义

A.2 泛型语法

A.3 类型属性速查

A.4 借用令牌速查