Skip to content

Home

Jump to bottom
ChenQiFengChui edited this page Oct 10, 2026 · 6 revisions

Sublimation（凝华）

把类型系统与程序逻辑融合的编程语言。Kotlin 手写编译器，零第三方依赖，源码直接编译为 JavaScript。

语言名取自物理现象「凝华」——气态不经液态直接成固态。正如本文的命题不经运行时、直接在编译期析出为程序的静态保证。

✅ v2.0 完成：空安全 / 可变性控制 / 异步 + HKT 高阶类型，350 项测试全绿

核心特性

  • 上下文弥散（命题系统）——函数类型携带前置/后置命题，调用前必须满足什么、调用后能保证什么，写进类型本身。用户写普通代码，编译器自动推理。
  • 目录即模块（P0）——一个目录 = 一个模块，<模块名>.settings 显式挂载；根目录下的 stdlib/ 隐式挂载给所有模块。
  • 类型类——Haskell 的拼写、Rust 的机制：class Show[T] { fun show(): Str } + impl Show for Grade { ... }。
  • 真模式匹配 when——解构、嵌套构造子、守卫、穷尽性判定（Java 式 switch 已全盘废弃）。
  • 纯度受控——函数默认且只能为纯；禁止调用非纯内建、禁止写外部变量，除非用 unchecked 逃逸。
  • 一切运算符皆函数——1 + 1 等价于 +(1,1)，二元函数即可中缀；支持自定义运算符。
  • 数值类型——Nat（自然数）/ Int（整数）/ Rat（有理数）。
  • 零运行时库——源到源生成纯 JavaScript，node 直接运行。
  • 空安全（v2.0）——T? 可空类型 + ?: Elvis + ?T 类型测 + is T 智能转换自动收窄。
  • 可变性控制（v2.0）——@mut 显式可变 + immutable<T> 不可变命题 + untouch<param> 形参只读保证。
  • 异步（v2.0）——@async 函数 + Task 并发 + Channel 通信 + 自动 await 挂起点；main 天然 async。
  • 高阶类型 HKT（v2.0）——[F[_]] kind 形参、impl Functor for List[a] 字典占位、kind 合一 F[A]~List[Nat]。

快速开始

gradlew.bat fatJar                       # 构建 fat jar
java -jar build/libs/sublimation.jar check hello.subl
node out.js                              # 运行

详见 快速上手。

文档导航

页面 内容
简介 定位、语言立场、编译器分级、编译管线
快速上手 新人向心智模型、语法速览、报错怎么读
语言语法 详细文法、诊断码
模块系统 P0 目录即模块、挂载、可见性
上下文系统 命题弥散、自动推理、与主流证明器对比
空安全系统 v2.0 空安全（T?/?:/>:/?T 智能转换）
副作用与可变性控制 纯度规范、@mut/immutable/untouch
异步 v2.0 异步（@async/Task/Channel）
高阶类型 v2.0 HKT（kind/字典分发/kind 合一）
术语表 专门术语收拢（定义 → 出处）

仓库完整文档见 https://github.com/inline-function/Sublimation/blob/main/doc/

首页

Clone this wiki locally