LeanDB: 用 Lean 构建强类型 SQL 前端
文章介绍了 Theoric Labs 的 LeanDB 实验，旨在将形式化方法与 AI 智能体结合应用于数据库领域：用 Lean 语言描述数据及其属性，同时使用 SQL 数据库进行存储和查询。文章通过咖啡菜单示例系统讲解了 Lean 的类型系统，包括归纳类型（如 Temperature、MenuItem）、细化类型（如限制浓缩咖啡份数为 1-4 的 ShotCount 子类型）、依赖类型（杯型大小依赖于冷热温度的 CupSize 索引族），以及元类型（FieldSpec 宇宙设计模式，用数据描述类型）。作者认为，强类型能让编译器在运行前阻止非法数据写入，将验证结果显式化，从而构建无 bug 的软件系统。
