类型系统

当前树中的类型系统故事是宽广的，不是狭隘的。它不仅仅是关于原始类型或推断；它是效果、单位、知识、所有权、精化、特质、以及模式推理的交汇点。全面的视角需要展示这种广度，同时对当前工件所完全证明的内容保持诚实。

当前源图

• self-hosted/check/types.sio 和 self-hosted/check/infer.sio 是普通类型检查和推断的核心起点。
• self-hosted/check/effects.sio、units.sio、epistemic.sio、ownership.sio、traits.sio 和 refinement.sio 展示了检查器如何按关注点拆分。
• self-hosted/check/env.sio、defs.sio、patterns.sio、pat_decision.sio 和 exhaustiveness.sio 在理解上下文、声明和匹配推理时很重要。

公共文档可以安全声称的内容

• 被检查的工件宣布单位、精化类型、知识型态和代数效果是语言特性的一部分。
• 拒绝固定件和当前示例证明了至少部分更丰富的类型故事不是仅仅具有雄心壮志。
• 每个高级子系统的确切执行级别仍然取决于工件和您正在执行的特定代码路径。

小型已类型化的表面示例

fn safe_div(a: i32, b: i32) -> i32 with Panic {
    if b == 0 {
        panic("division by zero")
    }
    a / b
}

如何保持真实

• 使用 compile-fail 和 run-pass 固定件来声明关于强制行为的断言。
• 使用源图描述来声明关于检查器架构的广度。
• 不要将整个检查器压缩成一个简单的 Hindley-Milner 故事；当前仓库的结构已经比那更丰富了。