网易首页 > 网易号 > 正文 申请入驻

Nix等了15年,这个20秒跑完的类型检查器终于来了

0
分享至

整个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是只羊驼——也许类型检查器的终极形态,就是凑个动物园。

特别声明:以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布,本平台仅提供信息存储服务。

Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.

相关推荐
热点推荐
趁你病,要你命!法国特种兵突袭11万吨油轮,乌军将轰炸西伯利亚

趁你病,要你命!法国特种兵突袭11万吨油轮,乌军将轰炸西伯利亚

李健政观察
2026-06-01 18:56:46
他汀药有7种,只有一种不影响血糖,早知道早收益!

他汀药有7种,只有一种不影响血糖,早知道早收益!

药师方健
2026-05-31 22:45:44
一只狐狸惊现四川一水库边,村干部称其已来数月!相关部门:暂不知是否野生,如受伤会救助

一只狐狸惊现四川一水库边,村干部称其已来数月!相关部门:暂不知是否野生,如受伤会救助

红星新闻
2026-06-01 18:16:23
电子眼抓拍有规律!记住7点,2026开车全年不扣分不被罚真的不难

电子眼抓拍有规律!记住7点,2026开车全年不扣分不被罚真的不难

沙雕小琳琳
2026-05-31 14:51:29
日本国歌只有28个字,将它翻译成汉语后,才知道日本人说的是什么

日本国歌只有28个字,将它翻译成汉语后,才知道日本人说的是什么

春秋砚
2026-06-01 10:15:08
WTI原油涨超7%

WTI原油涨超7%

界面新闻
2026-06-01 21:52:36
震惊!河南麦收“割分按亩”,网友调侃:不地道啊,坏了江湖规矩

震惊!河南麦收“割分按亩”,网友调侃:不地道啊,坏了江湖规矩

火山詩话
2026-06-01 06:43:31
3万砸到1.3万!常州武进楼市真相,为何本地富豪正扎堆退场

3万砸到1.3万!常州武进楼市真相,为何本地富豪正扎堆退场

说故事的阿袭
2026-06-01 14:09:40
Netflix王牌美剧,后劲太顶了

Netflix王牌美剧,后劲太顶了

来看美剧
2026-05-10 22:02:14
一位老股民的肺腑之言:不管是熊市还是牛市,我都坚持这样选股!

一位老股民的肺腑之言:不管是熊市还是牛市,我都坚持这样选股!

一方聊市
2026-05-25 21:41:49
要求实地查看!特朗普下令彻查金库

要求实地查看!特朗普下令彻查金库

看看新闻Knews
2026-06-02 01:04:36
胡锡进大赞华为韬定律:这是敲响美国科技霸权的丧钟

胡锡进大赞华为韬定律:这是敲响美国科技霸权的丧钟

映射生活的身影
2026-05-31 22:44:35
新冠后遗症的长期侵袭,无数人在不知不觉中深陷困境

新冠后遗症的长期侵袭,无数人在不知不觉中深陷困境

律法刑道
2026-04-01 10:15:47
沈阳鸟岛摩托艇甩尾将游客淋成“落汤鸡”,最新回应...

沈阳鸟岛摩托艇甩尾将游客淋成“落汤鸡”,最新回应...

沈阳公交网小林
2026-06-02 00:08:54
美媒:中国曝光处于原型阶段的新一代重型坦克,世界顶级装甲防护

美媒:中国曝光处于原型阶段的新一代重型坦克,世界顶级装甲防护

零度Military
2026-06-01 13:17:09
人不会无缘无故患糖尿病!研究发现:得糖尿病的人,离不开这5点

人不会无缘无故患糖尿病!研究发现:得糖尿病的人,离不开这5点

芹姐说生活
2026-06-01 19:10:38
普京访华未拿下天然气大单,俄经济压力逼出“停战讨论”

普京访华未拿下天然气大单,俄经济压力逼出“停战讨论”

桂系007
2026-06-02 04:21:23
74岁老人嫌杨絮碍事竟将其点燃,20辆新能源车被烧毁!已被采取刑事强制措施

74岁老人嫌杨絮碍事竟将其点燃,20辆新能源车被烧毁!已被采取刑事强制措施

环球网资讯
2026-05-31 18:13:21
夏天已至,医生叮嘱糖尿病患者:宁可吃西瓜,也别天天吃这3种物

夏天已至,医生叮嘱糖尿病患者:宁可吃西瓜,也别天天吃这3种物

垚垚分享健康
2026-06-01 08:54:30
医生:只要低密度脂蛋白没这个数,高血脂并发症风险就不用太焦虑

医生:只要低密度脂蛋白没这个数,高血脂并发症风险就不用太焦虑

健康科普365
2026-05-31 13:05:09
2026-06-02 05:35:00
摸鱼算法
摸鱼算法
致力于用最前沿的AI技术,换取更多发呆时间的三十岁青年。
4404文章数 45关注度
往期回顾 全部

科技要闻

黄仁勋演讲实录|40年来PC首次重设计!

头条要闻

伊朗计划彻底封锁霍尔木兹海峡 特朗普回应

头条要闻

伊朗计划彻底封锁霍尔木兹海峡 特朗普回应

体育要闻

杰威:如果我没受伤,我们能击败马刺

娱乐要闻

奚梦瑶婚礼现场图!一双儿女当花童

财经要闻

宇树过会,杭州赢麻了

汽车要闻

奇瑞集团5月销量24.8万辆 同比增长20.5% 出口18.2万辆再创新高

态度原创

艺术
健康
教育
旅游
游戏

艺术要闻

吴镇写竹,清清爽爽

干细胞临床研究向患者收费?别踩坑

教育要闻

我给她钱 换来的不是感激 而是她的谩骂

旅游要闻

世界旅游城市联合会“会员之家”在京揭牌

又一款经典RPG神作启动重制!不止高清 期待拉满

无障碍浏览 进入关怀版