Repository navigation
Home
ChenQiFengChui edited this page Oct 8, 2026
·
6 revisions
把类型系统与程序逻辑融合的编程语言。Kotlin 手写编译器,零第三方依赖,源码直接编译为 JavaScript。
语言名取自物理现象「凝华」——气态不经液态直接成固态。正如本文的命题不经运行时、直接在编译期析出为程序的静态保证。
✅ v1.0 完成:全部 P0–P11 落盘,285 项测试全绿
- 上下文弥散(命题系统)——函数类型携带前置/后置命题,调用前必须满足什么、调用后能保证什么,写进类型本身。用户写普通代码,编译器自动推理。
-
目录即模块(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直接运行。
gradlew.bat fatJar # 构建 fat jar
java -jar build/libs/sublimation.jar check hello.subl
node out.js # 运行详见 快速上手。
| 页面 | 内容 |
|---|---|
| 简介 | 定位、语言立场、编译器分级、编译管线 |
| 快速上手 | 新人向心智模型、语法速览、报错怎么读 |
| 语言语法 | 详细文法、诊断码 |
| 模块系统 | P0 目录即模块、挂载、可见性 |
| 上下文系统 | 命题弥散、自动推理、与主流证明器对比 |
| 术语表 | 专门术语收拢(定义 → 出处) |
仓库完整文档见 https://github.com/inline-function/Sublimation/blob/main/doc/