整个nixpkgs仓库的类型检查，20秒跑完。这个速度放在Nix生态里，相当于在老爷车上装了涡轮增压。
开发者Anders Christiansen Sørby花了两年时间，把一个叫Tix的类型检查器/LSP（语言服务器协议，Language Server Protocol）塞进了Nix世界。他的目标很明确：让Nix拥有TypeScript级别的开发体验——能推断的尽量推断，实在恶心的地方再手写类型标注。
Nix的痛点从来不是"能跑"，而是"怎么跑明白的"
Nix作为纯函数式包管理器，配置文件就是代码，代码就是构建脚本。这种设计带来一个副作用：你的系统配置可能藏着几百个隐式依赖，改一行代码，整个系统的构建图谱都可能变天。
现有的Nil和Nixd已经能解决基础的跳转定义和自动补全。但Sørby的假设是，一个真正的类型检查器能走得更远——它不仅能告诉你"这里错了"，还能在错误发生前就把选项收窄到合理的子集。
TypeNix选择了另一条路：把Nix的AST（抽象语法树，Abstract Syntax Tree）翻译成TypeScript的AST，直接复用微软的类型检查器。Sørby承认这"真的很酷"，TypeNix对overrides的支持目前也比Tix好。但他的直觉是，为Nix量身定做的类型系统，长期来看更容易调校。
从Hindley-Milner到SimpleSub：一场类型系统的"改装"
Sørby最初实现的是Damas-Hindley-Milner类型系统——函数式语言的老朋友，Haskell、ML家族都在用。它的核心卖点是"完备性"：不给任何类型标注，也能推断出程序最一般的类型。
但HM有个硬伤：处理联合类型（union types）时，它只能把两个未知类型等同起来，没有子类型关系。其他语言靠"标签联合"（tagged unions）绕过去，可Sørby不想改动Nix核心语法。
SimpleSub的出现解决了这个死锁。它保留了HM"遍历AST生成约束"的大框架，但把"统一"（unification）换成了"子类型编码"。
举个例子：在let y = foo b里，HM会说"b必须和foo的参数类型完全相同"，SimpleSub则允许"b是foo参数类型的子类型"。这种松弛让联合类型自然涌现——类型变量在求解过程中积累上下界，这些边界最终变成推断类型里的交集和并集。
如果一个值在某个分支是字符串，另一个分支是整数，这不是类型错误，而是string | int
SimpleSub搞定后，真正的硬仗才开始：如何把联合类型收窄到有用的子集。Sørby举了个例子：
let foo = {name ? null}: if name != null then "hello ${name}" else "world"in foo {} # 这里name是null，但返回类型应该是string，不是string | string这种精细化处理，决定了LSP的补全列表是贴心还是添堵。
20秒背后的取舍：快，但还能更快
Tix目前的性能数据：nixpkgs全量检查约20秒，个人NixOS配置5秒左右。Sørby说"有些想法能让这更快"——但没展开。
这个速度在类型检查器里算中等偏上。作为对比，TypeScript对大型代码库的首次检查通常以分钟计，但后续增量检查能做到毫秒级。Tix的挑战在于，Nix的惰性求值和动态导入让"增量"的定义变得模糊。
另一个隐性成本是Negation类型——Tix的另一块理论基石。它允许表达"不是某类型"的约束，这对Nix这种配置语言很实用（比如"这个参数不能是null"）。但Negation类型的求解复杂度是出了名的难搞，Sørby的实现能跑多稳，还需要更多实战检验。
生态位之争：Tix、TypeNix，还是等官方？
Nix社区对类型系统的呼声已经持续十多年。2018年的Nix 2.0曾讨论过内置类型检查，最终不了了之。2022年的Nixpkgs架构团队把"更好的开发者工具"列为优先级，但具体路线至今模糊。
这种真空催生了民间解决方案的爆发：Nil走实用主义路线，用启发式规则补全；Nixd绑定C++实现追求性能；TypeNix借TypeScript的东风；Tix则押注学术派的SimpleSub+Negation。
Sørby的赌注是：为Nix量身定做的类型系统，比"翻译到别的语言"更能触及Nix的 peculiarities——那些让Nix既强大又折磨人的特性，比如属性集的懒加载、路径类型的特殊处理、以及builtins的混沌宇宙。
Tix目前支持的功能包括：类型推断、错误诊断、跳转到定义、自动补全、以及基于类型的重构建议
但overrides的支持确实不如TypeNix——这是Sørby自己认的。在Nix世界，override是包定制的核心机制，这个短板可能挡住一部分重度用户。
项目托管在GitHub，许可证是MIT。Sørby在README里留了句话：「欢迎试用，欢迎骂，但最好是带着用例来骂。」
最后一个细节：Tix的Logo是只猫。Sørby没解释为什么，但Nix的Logo是只羊驼——也许类型检查器的终极形态，就是凑个动物园。
热门跟贴