语言样式规范 - inline-function/Sublimation GitHub Wiki

语言样式规范

写出让同事（和三个月后的自己）一眼就懂的 Sublimation 代码。

核心原则：多用语法糖

凝华提供了丰富的语法糖，它们不仅更短，可读性也更好。不要为了"显式"而拒绝糖。

1. 表达式的首选写法

✅ 推荐 ❌ 不推荐 说明
xs.map({ v -> v + 1 }) 手写递归 函数式链式调用
xs.filter({ v -> v > 0 }) 手写 when 过滤 用容器方法
x?.field when(x) { Some(v) -> v.field; None -> None } 安全调用糖
getOrElse(x, 0) 手写解构/默认 Optional 方法
"Hello, ${name}" "Hello, " + name 字符串插值

2. when 穷尽性

把区间判断放进 when(n in _) 让编译器自动证明覆盖：

// ✅ 推荐：编译器自动证明区间覆盖 (0..30)
+∵ n ∈ (0..30)
when (n in _) {
    (0 .. 10)  -> print("低")
    (11 .. 20) -> print("中")
    (21 .. 30) -> print("高")
}

// ❌ 不推荐：if-else 链，编译器帮不了你
if (n <= 10) { print("低") }
else if (n <= 20) { print("中") }
else { print("高") }

3. 前置条件放类型里，不作防御检查

// ✅ 推荐：类型写明 n ≤ 100，调用方自动证明
fun capped(n: Nat)<n <= 100>: Nat = n

// ❌ 不推荐：运行时 if 检查
fun capped(n: Nat): Nat {
    if (n > 100) { return 100 }
    return n
}

4. Optional 解构用 when 或方法糖

// ✅ 推荐：when 解构一目了然
when (maybe) {
    Some(v) -> doSomething(v)
    None    -> doDefault()
}

// ✅ 也可以：链式方法
var result = maybe.map({ v -> v + 1 }).getOrElse(0)

5. 伴生命题：把约束写进结构体本身

// ✅ 推荐：struct 自己声明约束，构造时证明
struct PosPoint(x: Nat, y: Nat)<x > 0, y > 0>

// ❌ 不推荐：约束靠注释或运行时检查
struct Point(x: Nat, y: Nat)  // 没有约束

三种调用法

凝华有三种调用写法，按可读性灵活选用：

尾随调用法

函数末尾的 lambda 可以挪到括号外（尾随 lambda）：

xs.map({ v -> v + 1 })              // 常规写法
xs.map { v -> v + 1 }               // 尾随调用法（推荐）

xs.fold(0, { (a, v) -> a + v })     // 常规
xs.fold(0) { (a, v) -> a + v }      // 尾随

中缀调用法

二元函数都能写中缀：a f b 等价于 f(a, b)。运算符本身就是函数：

1 + 2            // 即 +(1, 2)
xs append ys     // 即 append(xs, ys)，也可写成 xs.append(ys)

扩展调用法

自由函数 f(o, …) 的第一个参数是对象时，可写成方法糖 o.f(…)：

size(xs)         // 自由函数调用
xs.size()        // 扩展调用法（等价，推荐）

get(m, "a")      // 自由函数
m.get("a")       // 扩展调用法（等价）

o.f(…参数) 的解析顺序：先找自由函数/扩展方法 f(o, …参数)；没有再看类型类字典里的 f。

命名规范

项目 规范 示例
函数名 小驼峰 getUser calcScore
变量名 小驼峰 userName totalCount
类型参数 大写字母 List[T] Map[K, V]
命题参数 @小写 @p @q
结构体/类型类 大驼峰 User Collection
impl 块 类型无特殊命名 impl Show for User
定理函数 描述性名称 rangeLowerBound leqTrans

模块组织

MY_PROJECT/
  main.subl                ← 入口（必须有 fun main()）
  MY_PROJECT.settings      ← 模块声明（mount 依赖）
  stdlib/                  ← 标准库（有则自动挂载）
  users/                   ← 子模块目录
    users.subl
    users.settings

注释与文档

// 这是单行注释——解释为什么这样做，而不是做了什么

// --- 块注释风格：用 --- 分隔逻辑段落 ---

// TODO: 这是一条待办（编译器不解析，给人看的）

检查清单

在你提交代码前，确认：

  • 表达式链够短（单行完成的事不分三行）
  • 前置条件用类型（伴生命题/函数上文），不靠 if 防御
  • when 穷尽性交给编译器（区间用 when(n in _)）
  • Optional 不裸 if/else——用 when 或链式方法
⚠️ **GitHub.com Fallback** ⚠️