🐰 MoonBit Community [index]
- MoonBit community weekly, blog, and knowledge base
- Powered by Kodama
🐰 MoonBit Community [index]
- MoonBit community weekly, blog, and knowledge base
- Powered by Kodama
MoonBit Community Blog 是由 Lampese 发起并负责、由 PLCT J139 小队主要运营、接受社区贡献的 MoonBit 非官方社区网站,旨在拉近社区交流,同步社区动态,为更多人介绍 MoonBit,促进 MoonBit 语言发展。 我们非常需要社区成员的帮助来维护和完善 Community-Blog,具体贡献方式和标准可见 Contribution Guide 。 网站目前分为以下部分: 且版权目前归属于中国科学院软件研究所。 1. Overview [overview]
1.1. Bodies [overview/bodies]
1.2. Roadmap [overview/roadmap]
1.3. Copyright [overview/copyright]
除特别注明外,项目中除了代码部分均采用(Creative Commons BY-NC-SA 4.0) 知识共享署名 - 相同方式共享 4.0 国际许可协议 进行许可。
Community-Blog 基于 Kodama 0.2.7 框架编写,
同时支持 markdown 与 typst 语言,并且有类 forest 结构。
关于该框架的具体使用方法可以参见原框架的教程,
在 Community-Blog 中,我们认为大部分情况下您只需要拥有基本的 markdown 编写知识和排版经验即可。
若有复杂的图表制作需求,优先推荐使用 Typst 进行绘制。
向 Community-Blog 贡献的方式非常简单,
只需直接在我们的 Github 仓库发起 Pull Request 即可,写作规范将在后文中介绍。 若是文件粒度的微小更改,可以在 Github 直接编辑文件。
如果涉及多文件等复杂情况,您可能需要在本地部署工具进行预览。
下面是将 Community-Blog 克隆到本地的命令 (我们这里使用了一些 git 子模块,比通常的 确保你安装了 Rust 和 Node.js 环境,在项目根目录下运行如下指令安装 Kodama 与 Node.js 依赖: 实时预览只需运行 在提交之前我们推荐您运行 下面是一些关于排版的简单要求,适用于 Community-Blog 中的全部文章: 另外,对于发出的 PR,我们希望 PR 标题可以符合 约定式提交 的要求,并且可以标注贡献的部分,比如: 社区成员可以自由贡献一些博客文章,可以是 MoonBit 的教学、杂谈、开发日记等等。
直接发起 PR 在 trees/blog 文件夹中添加文章即可,因为文章分节会需要包含多个文件,
建议写作者单独开一个文件夹来存放文章,并用一个主文件来包含其他的文件。
文章的头部需要包含一些元信息: 举个例子: 周报暂定每两周更新一次,由当期负责人撰写和编辑。 社区成员可以对未正式发布的周报 PR,添加条目与修改当前的条目均可。
当期负责人每天会按时 Code Review。 贡献标准待定。 2. Contribution Guide [contribution]
2.1. Basic [contribution/basic]
2.2. Tools [contribution/tools]
git clone
多一个步骤):git clone git@github.com:moonbit-community/community-blog.git
cd community-blog
git submodule update --init --recursive
cargo install --git https://github.com/kokic/kodama.git --rev 323f97cf023c8a605f9ef986aba2fc34888abeed
npm i
npm run dev
,在浏览器访问 localhost:5173
即可。typos
、zhlint
和 autocorrect --fix
命令来检查和修复拼写错误。
其安装可以参考下面的链接: 2.3. Requirements [contribution/requirement]
trees
文件夹为根目录。例如本文件的路径是 /contribution/requirement.md
。community-blog/trees
目录,可以使用跳转和补全功能。feat: add a new community information for weekly
fix: fix typo for knowledge base
refactor: refactor the doc structure
2.4. Blog [contribution/blog]
author
:作者的名字date
:文章的日期,格式为 YYYY-MM-DDtitle
:文章的标题taxon
:文章的分类,通常都是 Blog
---
author: CAIMEOX
date: 2025-04-01
title: MoonBit 开发日记
taxon: Blog
---
2.5. Weekly [contribution/weekly]
2.6. Knowledge Base [contribution/knowledge]
这里是 2025/3/24 ~ 2025/4/6 的社区周报,为双周周报。 在过去的两周中,MoonBit 官方在深圳举办了 OJ 编程大赛和 2025 年第一次 Meetup 活动。社区贡献数量显著增长,有很多质量较高、来自社区的包涌现,基本着眼于基础设施方面。同时,Community-Blog 正式建立,发出第一次 Weekly 周报。(每个 title 下都有大量内容,点击标题即可展开) Meetup 3 月 30 日,MoonBit 举办了 2025 年首期技术以AI 时代下的基础软件为主题的 Meetup,吸引了 40 余位场开发者和近 300 名线上观众参与。 活动中,四位 MoonBit 核心工程师带来了精彩技术分享: 此外,特邀嘉宾 ShowmeBug & Clacky CEO 李亚飞则带来了 LL3 AI Coding 发展趋势的前沿洞察和实战案例。 本次活动不仅展示了 MoonBit 的最新技术进展,也为社区员提供了深入交流的平台,
现场观众提出的精准问题引发了广泛讨论,促进了开发者社区的活跃互动与技术共享。 OJ 竞赛 3 月 30 日,在技术分享的热烈讨论之后,迎来了 MoonBit OJ 编程竞技赛决赛颁奖典礼新年首场 Meetup 暨 OJ 编程竞技赛颁奖典礼。 MoonBit OJ 编程竞技赛自启动以来,吸引了众多开发者的积极参与,共有 300 多名开发者报名,经过激烈的初赛和选拔赛,最终有 200 名选手脱颖而出,9 位顶尖选手在决赛中进行了巅峰对决。 在决赛中,选手们在 3 小时内完成了 8 道高难度的编程题目,展现了他们在算法设计、逻辑推理和代码实现方面的卓越能力。经过紧张而激烈的角逐,最终确定了冠亚季军。 以下是本次比赛的获奖名单 MoonBit OJ 编程竞技赛不仅展示了开发者们的技术实力,也激发了他们对国产基础软件的热情。MoonBit 将继续为开发者们提供高质量的交流和竞技平台,推动技术生态的持续发展。
我们期待在下一次的社区活动中,看到更多开发者的精彩表现,共同见证 MoonBit 生态的不断进步和发展。 最佳硬科技前沿创新奖 3 月 29 日,第十二届开源操作系统年度技术大会(OS2ATC)在北京航空航天大学成功举办。OS2ATC 汇聚了来自清华大学、北京大学、蚂蚁集团、腾讯云、国家智能网联汽车创新中心、中移物联等一线高校、企业和科研机构的顶尖专家学者和行业领军人物。 MoonBit 以硬核技术突破重塑编程语言生态: 通过技术实践验证了硬科技“从学术走到产业”的标杆价值,为云原生与智能计算时代打造核心基石,荣获最佳硬科技前沿创新奖! WASM I/O 2025 本周,MoonBit 亮相巴塞罗那 WASM I/O 大会,并进行技术分享。本次为中国开发者平台首次登上这一国际技术峰会,展示了本土开源力量在 WASM 生态的创新成果。活动中,MoonBit 负责人张宏波 发表了主题演讲 《MoonBit & WebAssembly》。社区对 MoonBit 的表现给予了高度评价:Kotlin/Wasm 作者 Zalim 在社交媒体上表示:“MoonBit 在 WebAssembly 平台实现了精彩的成果”,对 MoonBit 在 WASM 方向的技术成果给予认可。ZivergeTech & Golem Cloud 公司 CEO John A De Goes 也表示:“与张宏波在 WASM I/O 见面后,我对 MoonBit 未来更加充满期待!” Mooncakes 开源 由 MoonBit 官方的 Yoorkin 领头,Lampese 东灯 参与建设新版 mooncakes.io 网站已经开源在 moonbitlang 组织内。该网站采用纯 MoonBit 基于 rabbit-tea 框架与 Tailwind CSS 构建,是采用 MoonBit 开发多网页应用的一个优秀示例。而且官方的 mooncakes.io 已经更换了这一版的实现。 值得注意的是这次的新版 mooncakes.io 采用了来自社区的两个仓库 fuzz-match 与 lazy,分别用于搜索和惰性求值。 这里是 2025/4/7 ~ 2025/4/13 的社区周报,为单周周报。 本周社区的贡献相对平淡,但可以肯定的是生态在逐渐稳固,并且应用层的项目越来越多。(每个 title 下都有大量内容,点击标题即可展开) 本周 illusory0x0 猗露 在 Community-Blog 编写了 MoonBit 实现树的先序遍历,MoonBit 实现外部迭代器和 MoonBit 实现内部迭代器三篇文章。第一篇文章作为前置,后两篇文章作为正文,从头开始介绍迭代器并且阐述了两种迭代器的区别,还分别用 MoonBit 实现了算法和两种迭代器。 本周 CAIMEOX 在 Community-Blog 编写了一篇文章 Derive Iteration from Recursion,从例子入手详细探讨了 defunctionalize 的概念及其在 MoonBit 的实现。 这里是 2025/4/14 ~ 2025/4/27 的社区周报,为双周周报。 过去的两周之内社区涌现了大量的项目和包,基础设施建设趋近完善。 Meetup 成都站 4 月 26 日,MoonBit 成功在四川成都集火实验室举办 Meetup!本次活动聚焦AI 时代下的基础软件,邀请了多位行业专家,共同探讨前沿技术与发展趋势。 活动议程精彩纷呈,四位专家带来了精彩的技术分享: 本次活动不仅展示了 MoonBit 的最新技术进展,也为社区成员提供了深入交流的平台,现场观众提出的精准问题引发了广泛讨论,促进了开发者社区的活跃互动与技术共享。 MoonBit 官方在 4.21 发布了一次官方周报,主要聚焦在语言更新方面: 在前端开发领域,MoonBit 语言正掀起一股革新浪潮。受 Elm 纯函数式架构启发,MoonBit 打造出 Rabbit-TEA 前端框架,凭借单向数据流与强类型检查,彻底告别运行时异常,让 Web 应用开发既简洁又健壮。 MoonBit 凭借模式匹配、不可变变量等特性,大幅优化编码体验。与 JavaScript 对比,MoonBit 代码精简且逻辑清晰,尤其在复杂业务处理时优势尽显。其编译器支持多后端输出,涵盖 JavaScript、WebAssembly 及 native,应用前景广阔。 Rabbit-TEA 采用经典 TEA 架构(Model、View、Update),通过消息驱动应用状态更新。开发计数器应用只需定义状态模型、消息类型和更新逻辑,框架自动处理视图更新,开发效率成倍提升。其 HTML EDSL 通过类型提示避免字符串滥用,减少潜在错误。 在副作用管理上,Rabbit-TEA 借鉴 Elm 的 Cmd 类型封装外部交互操作,确保运行时状态一致性。无论是 HTTP 请求还是浏览器 API 调用,都能通过 Cmd 安全管理。 得益于 MoonBit 的全局 DCE 优化,Rabbit-TEA 应用体积极小,计数器应用仅 33KB,性能优于主流框架。MoonBit 团队已用其重写包管理网站 mooncakes.io,并持续探索更多前沿特性,如服务端渲染与时间旅行调试。 Web 开发新时代已至,MoonBit 与 Rabbit-TEA 为前端开发注入全新活力! 这里是 2025/4/28 ~ 2025/5/11 的社区周报,为双周周报。 这里是 2025/5/12 ~ 2025/6/15 的社区周报,为四周周报。 Moonbit 官方在 5 月 19 号发布了一次官方周报,主要进行了语法更新和工具链更新: MoonBit 插件双更新!
MoonBit 编程语言实现重大突破,现已全面支持 JetBrains 开发环境与 LeetCode 答题平台,打通了从工程实战到算法训练的学习与实用闭环。 MoonBit 推出虚拟包特性,开发灵活性大幅提升!
MoonBit 编程语言又添新特性 —— virtual package!通过将包声明为虚拟包,用户可选择具体实现,若不指定则使用默认实现,极大地分离了接口与实现,开发灵活性直线上升。 MoonBit 官方开启了新活动 Pearls 征稿活动,具体可以查看活动链接。而且已经发出了第一篇 Pearls 文章 使用 MoonBit 编写 Pratt 解析器。文章内容在 Github 仓库 moonBit-pearls 中同样可以查看。 MoonBit 亮相美国,发表主旨演讲!🌍
2025 年 6 月 13 号,Moonbit 在国际顶级编程大会 LambdaConf 发表了关于异步编程的主旨演讲,更将与 Jai 编程语言创始人、独立游戏大师 Jonathon Blow 等技术大咖同台交流。 特别值得一提的是:GolemCloud 创始人 John A De Goes 在 WASM I/O 上盛赞 MoonBit,并表示将在即将到来的 LambdaConf 黑客松中亲自使用 MoonBit! MoonBit 创始人张宏波老师在 Github 开源了演讲的相关内容 moonbit-lambdaconf 仓库中。 这里是 2025/6/16 ~ 2025/6/22 的社区周报,为一周周报。在本周中 MoonBit 语言正式进入了 Beta 版本,是一个巨大的里程碑。 Moonbit 官方在 6 月 16 号发布了一次官方周报,本次是 beta 版本之前的最后修改,意味着语法即将进入稳定阶段。更新内容有: 用于表示错误的 定义错误类型的语法 对于函数, typealias/traitalias 语法更新:改用 废弃多参数 显式实现特征(Trait)新规:即使有默认方法也需 废弃外部类型 虚拟包支持抽象类型:接口声明,多实现可自定义类型。 新增保留字警告:未来可能成为关键字。 新增了箭头函数语法 矩阵函数功能被废弃,以精简语法。形如 之前,可以使用 对于一些比较模糊/不够广为人知的运算符优先级组合,例如 新引入了 等号右手侧只能是函数形式的值,比如匿名函数或者箭头函数,之前使用 利用新的错误多态功能,标准库中的许多高阶函数如 MoonBit 在 2025 年 6 月 13 日至 15 日,分别先后亮相两大重量级科技盛会:香港科技大学(广州)主办的第三届 INNOTECH 创科嘉年华,以及 msup(麦思博)主办的第十二届 GIAC 全球互联网架构大会。在 GIAC 大会上,IDEA 研究院基础软件中心首席科学家、MoonBit 平台负责人张宏波在本次大会中带来了《AI 编程在 MoonBit 上的垂直整合》主题演讲。 2025 年 6 月 18 日,CSDN 官方公众号发表了一篇题为《20 年磨一剑,国内首个工业级编程语言进入 Beta 版本》的文章,介绍了 MoonBit 的最新进展。同时也标志着 MoonBit 正式进入 Beta 版本。 MoonBit 官方的 Pearls 系列文章更新了第二篇文章 《MoonBit Pearls Vol.02:MoonBit 中的面向对象编程》,由 MoonBit 官方同学刘子悦执笔,通过一个生动的 RPG 游戏开发的例子,带领读者探索了 MoonBit 中的面向对象编程。 这里是 2025/6/23 ~ 2025/6/29 的社区周报,为一周周报。 MoonBit 官方开源了官网 moonbitlang.cn 的源代码 website,未来社区成员可以参与 MoonBit 官网的建设了。 MoonBit 官方创建了一个新仓库 moonbit-evolution,后续 MoonBit 所有用户可见的改动,都会在仓库中说明,使得 MoonBit 的发展更加透明,用户可追踪。用户也可以在仓库中讨论和提出提案,象征着 MoonBit 的社区写作文进入新阶段。 MoonBit 官方在 6.24 发布对 MoonBit 编程语言创始人张宏波的访谈,围绕 MoonBit 的设计理念、发展历程、核心特点及行业思考展开,核心内容如下: MoonBit 简介 “AI 原生”的体现及设计决策 与 AI Coding 工具的对比及团队 AI 使用情况 MoonBit Beta 版及生态策略 生态冷启动策略:通过支持编译到 C 代码,实现与 Python 生态的复用,可直接调用 Python 成熟库,提供渐进式迁移路径。 创始人张宏波的技术历程 对行业的思考与建议 这里是 2025/6/30 ~ 2025/7/13 的社区周报,为双周周报。 MoonBit 官方开源了使用 MoonBit 编写的编译器前端 parser,基于 moonlex 与moonyacc。证明 MoonBit 当前的编译器前端已经完成了自举,也证明了 MoonBit 在符号计算相关领域的优势。 MoonBit 官方开源了异步基础设施 async,目前可以确保在 Linux/macOS 的 Native/LLVM 后端上正常运行。库的功能非常完善,支持结构化并发、优秀的错误传播和任务取消。未来将会支持比如 Windows 支持之类的更多功能。 MoonBit 官方开源了使用 WasmOfOCaml 编译的跨平台 MoonBit 编译器 moonc_wasm,采用 Wasm 文件发行,可以解决很多小众平台的 MoonBit 发行问题。 MoonBit 官方的 Pearls 系列文章更新了第三、四篇文章《MoonBit Pearls Vol.03:算法竞赛经典:背包问题》、《MoonBit Pearls Vol.04:用 MoonBit 探索协同式编程(上)》,分别讨论了 MoonBit 与动态规划和协同式编程的的话题。 MoonBit 官方在 Beta 阶段的双周报正式改为月报,7 月 15 日发布了一次月报,有以下内容: 这里是 2025/7/14 ~ 2025/7/20 的社区周报,为单周周报。 7 月 19 日,MoonBit 举办了一次与蚂蚁开源的 Meetup,主题为“AI 时代下的基础软件”。 活动中,来自 MoonBit 官方与蚂蚁开源的老师带来了精彩技术分享: 这里是 2025/7/21 ~ 2025/8/3 的社区周报,为双周周报。 这里是 2025/8/4 ~ 2025/8/17 的社区周报,为双周周报。 3. Weekly [weekly]
3.1. Weekly1 社区周报 2025/3/24 ~ 2025/4/6 [weekly/weekly1]
3.1.1. 本周官方重要动态 [weekly/weekly1/official]
参赛者名称 正确题数 总用时 (分钟) Dawn Magnet 8 960 Hao Zhang 6 514 Luyao LYU 5 310 xunyoyo 5 415 refinedheart 5 470 wangnianyi 4 369 liuly 3 70 zhristophe 3 301 Zhehao 0xFF 1 27
3.1.2. 本周社区新增优质项目 [weekly/weekly1/projects]
3.1.3. 本周社区新增优质包 [weekly/weekly1/packages]
3.1.4. 本周社区项目维护动态(只会写相对重要的内容) [weekly/weekly1/community]
3.2. Weekly2 社区周报 2025/4/7 ~ 2025/4/13 [weekly/weekly2]
3.2.1. 本周官方重要动态 [weekly/weekly2/official]
3.2.2. 本周社区新增优质项目 [weekly/weekly2/projects]
3.2.3. 本周社区新增优质包 [weekly/weekly2/packages]
3.2.4. 本周社区动态 [weekly/weekly2/community]
3.3. Weekly3 社区周报 2025/4/14 ~ 2025/4/27 [weekly/weekly3]
3.3.1. 本周官方重要动态 [weekly/weekly3/official]
async
函数采用新语法 f!(..)
,原 f!!(..)
将触发警告。trait
,旧方法仍可用但会收到编译器警告,迁移仅需将 op_xxx
改为对应 trait
的 impl
。trait
方法默认实现:新增 = _
标记,提升源码可读性。String
类型转换:现支持隐式转为 @string.View
,并恢复 [:]
取完整 view。Core API
改动:@string
包参数类型迁至 @string.View
,返回值类型相应调整。.mbt.md
文件 debug 断点设置,moon.mod.json
新增构建脚本字段。 3.3.2. 本周社区新增优质项目 [weekly/weekly3/projects]
3.3.3. 本周社区新增优质包 [weekly/weekly3/packages]
3.3.4. 本周社区动态 [weekly/weekly3/community]
3.4. Weekly4 社区周报 2025/4/28 ~ 2025/5/11 [weekly/weekly4]
3.4.1. 本周官方重要动态 [weekly/weekly4/official]
Trait
的实现方式将只支持通过 impl T for A ...
对类型 A
显式实现 trait T
;_
作为待定参数占位符以简化匿名函数的创建;fnalias
支持给类型和 trait
的方法创建别名;#internal
attribute,用于为 public API 的外部用户提供警告;loop
中可能产生歧义的 loop argument 的使用方式新增了警告;Array
到 ArrayView
类型、Bytes
到 @bytes.View
类型的隐式类型转换;moon
支持 bench
子命令,用于执行基准性能测试。
3.4.2. 本周社区新增优质项目 [weekly/weekly4/projects]
3.4.3. 本周社区新增优质包 [weekly/weekly4/packages]
3.4.4. 本周社区动态 [weekly/weekly4/community]
3.5. Weekly5 社区周报 2025/5/12 ~ 2025/6/15 [weekly/weekly5]
3.5.1. 本周官方重要动态 [weekly/weekly5/official]
..
调用链末尾自动丢弃值语义变更:在 .
/..
调用链末尾的最后一个 ..
以后会自动丢弃它的值,但这也意味着直接使用 x..f()
的值的用法将会被废弃,需要显式保存 x
。@bytes.View
和 @string.View
在 C 和 wasm1 后端现在会被编译成值类型,减少内存分配,性能有较大提升。
3.5.2. 本周社区新增优质项目 [weekly/weekly5/projects]
3.5.3. 本周社区新增优质包 [weekly/weekly5/packages]
str.format
的设计。 3.5.4. 本周社区动态 [weekly/weekly5/community]
3.6. Weekly6 社区周报 2025/6/16 ~ 2025/6/22 [weekly/weekly6]
3.6.1. 本周官方重要动态 [weekly/weekly6/official]
!
语法被替换为关键字 raise
,用于表示错误。type! T ..
改为 suberror T ..
,通过格式化工具可以自动完成迁移。f!(..)/f?(..)
的语法即将被废弃,函数的类型参数语法也从 fn f[..](..)
改为 fn[..] f(..)
。as
替代 =
,这一改动也可以通过格式化工具自动完成迁移。loop
,改用元组参数以保持与 match
一致。类似多参数的 loop
需求应该替换为元组,该改动保证了模式匹配的一致性。impl
。如果没有需要提供自定义实现的方法,可以用 impl Trait for Type 来表示 “给 Type 实现 Trait,但所有方法都用默认实现”。impl
的点调用,改用本地方法扩展。该改动比较复杂,我们引用周报原文:
之前,给外部类型的 impl
可以在当前包内用 .
调用。但这一功能是不重构安全的:上游新增方法会改变下游代码的行为。因此,我们决定废弃这一行为。作为替代,MoonBit 支持了局部地给外部类型定义新方法的功能,语法和普通的方法定义一样。这些给外部类型定义的方法有如下特点:
pub
的。这是为了保证跨包协作时不会产生冲突。x.f(..)
的解析规则变为(优先级从高到低):x
的类型所在的包的方法x
的类型所在的包的 impl
Json
字面量自动调用 ToJson::to_json
,编写更便捷。let x = 42
// 之前
let _ : Json = { "x": x.to_json() }
// 现在
let _ : Json = { "x": x }
(..) => expr
,能极大简化简单匿名函数:test {
let arr = [ 1, 2, 3 ]
arr
.map(x => x + 1) // 只有一个参数时可以省略括号
.iter2()
.each((i, x) => println("\{i}: \{x}"))
}
fn { .. => expr }
的矩阵函数可以改为箭头函数,其他矩阵函数应改为显式的 fn
和 match
。xx._
语法来将 new type 转化为其实际表示。但这一语法和 partial application 语法(_.f(..)
)过于相似,有视觉歧义。因此,xx._
语法被废弃,相应的,编译器会给每个 new type 自动生成一个 .inner()
方法,代替原本的 ._
。这一改动可以通过格式化代码自动完成迁移。<<
和 +
,MoonBit 现在会产生警告。手动或者通过格式化代码加上括号来明确计算顺序即可消除警告。letrec
和 and
关键字用于声明 local 互递归函数,比如:fn main {
letrec even = fn (x: Int) { ... } // anonymous function
and odd = x => ... // arrow function
}
fn
声明的隐式互递归写法会被 deprecated,不过自递归函数依然可以用 fn
进行声明。fnalias
不再能用于创建非函数值的别名。对于非函数类型的值,可以用 let 来创建别名。Array::each
现在可以接受带错误的回调函数了。main
包测试支持:moon test
运行测试,moon run
执行主程序(此前 main
包中禁止编写测试)。IDE codelens
支持运行文档中的测试。moon test
和 moon check
现在默认会包含文档中的测试。 3.6.2. 本周社区新增优质项目 [weekly/weekly6/projects]
3.6.3. 本周社区新增优质包 [weekly/weekly6/packages]
3.6.4. 本周社区动态 [weekly/weekly6/community]
3.7. Weekly7 社区周报 2025/6/23 ~ 2025/6/29 [weekly/weekly7]
3.7.1. 本周官方重要动态 [weekly/weekly7/official]
let x = 3
而非类似 Go 语言的x := 3
,let
关键字为 AI 提供明确的“新变量声明”信号,减少歧义。
3.7.2. 本周社区新增优质项目 [weekly/weekly7/projects]
3.7.3. 本周社区新增优质包 [weekly/weekly7/packages]
3.7.4. 本周社区动态 [weekly/weekly7/community]
3.8. Weekly8 社区周报 2025/6/30 ~ 2025/7/13 [weekly/weekly8]
3.8.1. 本周官方重要动态 [weekly/weekly8/official]
!expr
语法。对布尔表达式取反现在可以直接使用 !
符号,不一定要使用 not
函数。try .. catch .. else ..
语法中的 else
关键字被替换为 noraise
,原因是 try .. catch .. else ..
中的else
后是模式匹配而非代码块,和其他地方的 else
不一致。旧的写法将被废弃,编译器会提出警告。noraise
,一方面可以使类型签名中提供更清晰的文档信息,另一方可以用于防止在一些情况下编译器自动插入 raise
标记,比如:fn h(f: () -> Int raise) -> Int { ... }
fn init {
let _ = h(fn () { 42 }) // ok
let _ = h(fn () noraise { 42 }) // not ok
}
3.8.2. 本周社区新增优质项目 [weekly/weekly8/projects]
trait impl
,用于给 core 的开发者提供 review 支持。 3.8.3. 本周社区新增优质包 [weekly/weekly8/packages]
camelCase
、PascalCase
、snake_case
等等多种命名格式中转换。ArrayView[Byte]
形式读写的支持库 binaryPrimitives,该库受启发自 C# 语言的 System.Buffers.Binary.BinaryPrimitives
。目前的完成度较高。 3.8.4. 本周社区动态 [weekly/weekly8/community]
3.9. Weekly9 社区周报 2025/7/14 ~ 2025/7/20 [weekly/weekly9]
3.9.1. 本周官方重要动态 [weekly/weekly9/official]
3.9.2. 本周社区新增优质项目 [weekly/weekly9/projects]
3.9.3. 本周社区新增优质包 [weekly/weekly9/packages]
char::compose()
。 3.9.4. 本周社区动态 [weekly/weekly9/community]
3.10. Weekly10 社区周报 2025/7/21 ~ 2025/8/3 [weekly/weekly10]
3.10.1. 本周官方重要动态 [weekly/weekly10/official]
3.10.2. 本周社区新增优质项目 [weekly/weekly10/projects]
.mbt
文件类型和 moon.mod.json
项目根目录识别。
3.10.3. 本周社区新增优质包 [weekly/weekly10/packages]
3.10.4. 本周社区动态 [weekly/weekly10/community]
3.11. (未发布)Weekly11 社区周报 2025/8/4 ~ 2025/8/17 [weekly/weekly11]
3.11.1. 本周官方重要动态 [weekly/weekly11/official]
3.11.2. 本周社区新增优质项目 [weekly/weekly11/projects]
mbt_symbols
、mbt_bp
、mbt_bps
等命令,支持 MoonBit 符号列表查看、断点设置和断点管理功能。 3.11.3. 本周社区新增优质包 [weekly/weekly11/packages]
3.11.4. 本周社区动态 [weekly/weekly11/community]
二叉树的定义 先序遍历一棵树 我们把 下面的部分是用来测试系统栈版本和手动控制栈版本的一致性。 目前 MoonBit 社区有两个外部迭代器的实现,
Yu-zh/iterator 和
FlammeShadow/iter。 本文提供一个由浅入深的教程,来帮助读者学习外部迭代器。 Moonbit 标准库的 所以无法实现 也无法实现 不可变外部迭代器可以很自然的实现 可变外部迭代器可以实现 不可变外部迭代器没有内部可变状态可以迭代多次。 可变外部迭代器只能迭代一次,虽然无法实现 调用 可变外部迭代器,可以不断获取下一个元素的值,内部有一个可变的状态。 比如 Moonbit 标准库的 所以无法实现 也无法实现 不可变外部迭代器可以很自然的实现 可变外部迭代器可以实现 我们可以实现 接下来我们来实现不可变外部迭代器 不可变外部迭代器可以返回第一个元素和剩余的迭代过程 这里从 测试一下迭代过程 二叉树的定义 先序遍历一棵树 我们把 下面的部分是用来测试系统栈版本和手动控制栈版本的一致性。 这里使用不可变单向链表作为栈,每次返回一个 可变外部迭代器并不会保存,只能运行一次 不可变外部迭代器可以运行多次,但是需要额外保存迭代上下文 这里测试一下,不可变外部迭代器和 preorder 的一致性 接下来我们来实现 本文实现的内部迭代器参考 OCaml iter。 这里的 为了在迭代过程中停止循环,MoonBit 引入了 我们比较 把 MoonBit 标准库中的 我们来看 Moonbit 标准库的 所以无法实现 也无法实现 不可变外部迭代器可以很自然的实现 可变外部迭代器可以实现 递归和迭代是编程中两种基础的重复执行模式,它们在实现方式上有所不同,但计算能力上是等价的。
递归通过函数调用自身来分解问题,通常表达简洁,符合数学 (结构) 归纳法的思维模式;而迭代则借助循环结构 (如 既然两者各有优劣,是否存在一种通用方法,能够自动或半自动地将递归逻辑转换为等价的迭代实现?答案是肯定的,而这正是本文的核心概念——去函数化 (defunctionalization),即将递归的函数调用关系转换为显式的栈管理结构,从而在保持正确性的同时提升运行效率。 让我们以循序渐进的方式展开论述。
作为切入点,不妨考察一个具有典型性的基础案例:设想需要实现 此处 最直观的解决思路莫过于穷举法——将所有可能用到的谓词函数进行枚举编码。以下示例展示了针对整数的几种基本谓词: 借此定义,可重构出经过去函数化处理的过滤函数: 然而此方案存在明显局限性。
诚然,高阶谓词函数的集合实为不可数无穷集,这使得完备枚举在理论上即不可行。
但通过代数数据类型的参数化特性,我们可获得某种程度上的扩展能力。
例如将 更富启发性的是引入复合逻辑结构。
通过增加 经过这般层层抽象,我们所构建的 但必须指出,这种基于代数数据类型的方案存在固有的封闭性缺陷——每新增一个枚举成员都需要修改所有相关的模式匹配逻辑 (本案例中的 通过前文的讨论,读者应对去函数化的核心思想建立了基本认知。
本节将运用该技术解决更具挑战性的问题——二叉树遍历优化。首先给出二叉树的规范定义: 考虑基础的前序遍历实现: 在该函数的设计实现中,我们采用递归算法对树形数据结构进行系统性遍历,
这种方法虽能确保每个节点都受到函数 面对这个看似棘手的控制流问题,我们稍作停顿。
考虑引入“延续” (continuation) 这一关键概念——其本质是对程序剩余计算过程的抽象建模。
具体而言,对于表达式 $1 + 2 * 3 + 4$ 的求值过程:当计算 $2 * 3$ 时,其延续即为带洞表达式 $1 + \square + 4$ 所表征的后续计算。
形式化地,我们可以将延续定义为高阶函数 $\lambda x. 1 + x + 4$,
该函数接收当前计算结果并执行剩余计算过程。 延续传递形式 (Continuation-Passing Style,CPS) 的核心范式在于:
所有函数均不直接返回结果,而是通过将中间值传递给延续函数来实现控制流转移。
以树的前序遍历为例,当第一个 通过严格的 CPS 变换,程序的控制流获得了显式的过程化表征。
基于此,我们可进一步实施延续的去函数化,即将高阶函数表示转化为数据结构表示。
观察到延续包含两种形态:递归处理函数 重构后的实现将函数调用转化为对延续结构的模式匹配,引入辅助函数 为实现彻底的命令式转换,我们先将尾递归形式改写为显式循环结构。
通过 MoonBit 的 loop 语法,控制流的跳转关系得到直观呈现: 此时,向传统循环的转换已水到渠成。通过引入可变状态变量,我们获得完全命令式的实现: 经仔细分析可见,延续结构 这项系统性的转换工程清晰展现了从高阶函数到数据结构,
从递归到迭代,从隐式控制流到显式状态管理的完整范式迁移路径。 $$ \text{CPS} \to \text{Defunctionalization} \to \text{Inlining} \to \text{Tail Call Elimination} $$ 让我们对这一系列精妙的程序转换过程进行系统性的理论总结。
整个改造工程可分解为四个阶段: 第 Ⅰ 阶段:控制流显式化 (CPS 变换):
通过引入延续传递形式,我们将原本隐含在语言运行时中的执行上下文显式提升为可操作的一等公民。
这一关键转换使递归调用点的控制流转移过程浮出水面,为后续的机械化改造奠定了基础。 第 Ⅱ 阶段:去函数化:
基于 Reynolds 提出的去函数化理论,
我们将高阶的延续函数降维为具体的代数数据类型 第 Ⅲ 阶段:内联与尾递归化:
通过将辅助函数 第 Ⅳ 阶段:迭代式转换:
最终阶段将尾递归结构转换为基于可变状态和循环命令的迭代实现。
这一转换过程严格对应现代编译器对尾调用的优化策略:
将递归调用点改写为带状态更新的循环跳转,将延续对象转换为显式的栈数据结构。
值得注意的是,从 “去函数化”的确是精妙的程序转换技术,
若读者在看完本文仍意犹未尽,
希望能够深入了解其背后的理论基础和更多实现细节,
可以参考以下资源: LunaFlow 是一个基于 MoonBit 的科学计算框架,
旨在为用户提供高效、灵活的计算能力。
该框架在设计理念上有许多独到之处,
尤其体现在数据抽象与泛型算法的实现。
然而遗憾的是,未有技术文档详尽阐释这些核心设计背后的理论依据与实践权衡。 作为 LunaFlow 的架构者之一,笔者撰写本文的目的在于:
其一,系统性地剖析 LunaFlow 的顶层设计哲学,揭示其主要设计原则与实现细节。
其二,通过具体用例的实证分析,展示如何利用该框架构建高效的数值计算流程。
希望读者不仅能够领悟到此种抽象设计在工程实践中的精妙之处,
还能将这种范式迁移至自身的项目开发之中,提升代码的表达力与泛用性。 LunaFlow 采用分层模块化架构,
通过严格的抽象层级将系统组件进行逻辑划分。
其架构可组织为树形结构:
位于根基位置的是 Luna-Generic 核心模块,
该模块借助 MoonBit 的 trait 系统实现了对基础数学结构的代码描述。
在此基础上,作为首要叶子节点的 Luna-Utils 模块承担了通用工具函数的实现,
而诸如 Complex 与 Quaternion
等基础数据结构包则构成了更为细化的叶节点。 高阶数学工具包被置于抽象体系的更上层级,
当前主力模块包括 Calculus Numerical、
Linear Algebra 及 Polynomial 等,
这些模块通过显式的依赖关系调用底层服务,展现出清晰的依赖倒置原则(Dependence Inversion Principle)。
尤为精妙的是,LunaFlow 的架构设计允许用户在 程序设计语言中抽象机制的一个根本目标,
在于对行为模式进行精确的形式化描述并实现有效的代码复用。
在此语境下,代数结构因其严谨的数学内涵,
恰好为这类抽象提供了坚实的理论基础。
MoonBit 语言设计的 trait 系统,通过精妙的类型约束与组合机制,
构建了一套完整的代数结构表达体系。
该系统允许开发者以类型安全的方式,将半群(Semigroup)到半环(Semiring),乃至更复杂的环(Ring)等代数结构进行层级化建模。 在抽象代数中,一个半环(Semiring)是一个集合 $R$,
配备了两个二元运算:加法 $+$ 和乘法 $*$,且满足下面的性质: 除此之外,还满足下面两条性质: 从数学定义出发,半环结构实际上包含两个相互关联的代数组成部分:
其一是具有交换性质的加法幺半群,
其二是乘法幺半群。
在 MoonBit 的类型系统中,
这两个基本结构分别对应着 trait 需要特别说明的是,
当前 MoonBit 的 trait 机制尚无法在类型层面强制保证代数公理的成立 ——
包括但不限于结合律、分配律等基本性质的正确性。
这种限制本质上源于类型系统的表达能力边界:
若要严格验证代数公理,必须借助依赖类型等高级类型理论工具,
而这与 MoonBit 作为工业级语言的设计目标有所偏离。
对这一话题感兴趣的读者,可进一步研读 Lean 或 Coq 等定理证明器的相关文献,
这些语言可通过精密的类型机制表达更为复杂的数学约束。
下面是一个在 Lean 中定义半群的示例: 此类抽象机制的核心价值在于实现真正基于代数性质的通用编程范式。
譬如,撰写矩阵乘法算法时,开发者只需约束类型参数满足 从软件工程的角度审视,代数结构的层级化抽象完美体现了关注点分离(Separation of Concerns)的设计哲学。
数学上,群(Group)在幺半群基础上引入逆元概念,
而环(Ring)又要求加法构成交换群。
这些递进关系在 MoonBit 中表现为 trait 的组合:
每个新特征只需声明其扩展的代数运算,无需重复定义底层运算。这种设计不仅消除了代码冗余,
更重要的是建立了数学理论与程序实现之间的严格对应,
使得抽象层次之间的关系如抽丝剥茧般清晰可见。 对于代数结构公理的验证,我们并非束手无策。
虽然从完备性角度无法穷尽所有可能的验证场景,
但通过精心构建的测试用例集合,
我们能够对公理在特定实例上的有效性进行系统化验证。
借助 QuickCheck 这一强大的属性测试框架,
我们得以实现从抽象代数公理转化为可执行规范(Executable Specifications)的范式转变。这一过程中,代数结构的基本公理恰成为指导属性编写的理论基石,配合自动生成的测试数据,能够对类型实现进行统计学上的验证。 简单来说,QuickCheck 的本质是通过随机采样对程序行为进行统计验证。
用户可以制定待测试程序具有的属性,
通常可以视为是 简单来说,QuickCheck 是一种基于随机采样对程序行为进行统计验证的测试框架。其核心工作机制可解构为以下几个的骤: 在 QuickCheck 测试系统中,属性构造居于核心地位。
对于代数结构而言,其公理体系天然具备可检验性特质:
我们可以通过将数学公理直接映射为测试属性,在具体实现中建立严格的验证机制。
以 Linear-Algebra 代码库中的典型案例进行说明:
当定义表示向量的 $$
\begin{align*}
\vec{u} + \vec{v} &= \vec{v} + \vec{u} \quad \text{(交换律)} \\
\vec{u} + (\vec{v} + \vec{w}) &= (\vec{u} + \vec{v}) + \vec{w} \quad \text{(结合律)}
\end{align*}
$$ 在实现层面,我们可将其转化为如下测试验证(注:此处假定 这种将数学公理机械性地转化为可执行验证机制的范式,
使得 LunaFlow 得以利用数学上的公理体系,
为实现的正确性提供强有力的测试保障。 本文译自 Brent Yorgey 的 Functional Pearl 论文 You could have invented Fenwick trees,并做了一些解释补充、错误修正,以及将原文的 Haskell 代码都翻译到了 MoonBit 代码。 芬威克树(Fenwick trees),亦称二叉索引树(binary indexed trees),是一种精巧的数据结构,旨在解决这样一个问题:如何在维护一个数值序列的同时,支持在亚线性时间内完成更新操作与区间查询。其实现简洁高效,然亦颇为费解,多由一些针对索引的、不甚直观的位运算构成。本文将从线段树(segment trees)入手——这是一种更为直接、易于验证的纯函数式解法——并运用等式推理,阐释芬威克树的实现乃是一种优化变体,此过程将借助一个 MoonBit 嵌入式领域特定语言(EDSL)来处理无限二进制补码数。 假设我们拥有一个包含 $n$ 个整数的序列 $a_1, a_2, \ldots, a_n$,并希望能够任意交错执行以下两种操作,如图 1 所示: 注意,更新操作表述为将现有值增加 $v$;我们亦可通过增加 $v - u$ (其中 $u$ 为旧值) 来将给定索引处的值设为一个新值 $v$。 倘若我们仅将整数存储于一个可变数组中,那么更新操作可在常数时间内完成,但区间查询则需要与区间大小成线性关系的时间,因其必须遍历整个区间 $[i, j]$ 以累加其值。 为改善区间查询的运行时效,我们或可尝试缓存(至少部分)区间和。然则,此举必须审慎为之,因为在更新某个索引处的值时,相关的缓存和亦须保持同步更新。例如,一种直截了当的方法是使用一个数组 $P$,其中 $P_i$ 存储前缀和 $a_1 + \cdots + a_i$;$P$ 可通过一次扫描在常数时间内预计算得出。如此一来,区间查询便十分快捷:我们可通过计算 $P_j - P_{i-1}$ 在常数时间内获得 $a_i + \cdots + a_j$(为方便起见,我们设 $P_0 = 0$,如此该式即便在 $i=1$ 时亦能成立)。不幸的是,此时更新操作却需要线性时间,因为改变 $a_i$ 将导致对所有 $j \ge i$ 的 $P_j$ 进行更新。 是否存在一种数据结构,能够使这两种操作均在亚线性时间内完成?(在继续阅读下一段之前,您不妨稍作停顿,思考一番!)这并非仅仅是一个学术问题:该问题最初是在算术编码(Rissanen & Langdon, 1979; Bird & Gibbons, 2002)的背景下被提出的。算术编码是一类将消息转换为比特序列以供存储或传输的技术。为最大限度地减少所需的比特数,通常需要为出现频率较高的字符分配较短的比特序列,反之亦然;这就引出了维护一个动态字符频率表的需求。每当处理一个新字符时,我们就更新该表;而为了将单位区间细分为与各字符频率成比例的连续段,我们需要查询该表以获取累积频率(Ryabko, 1989; Fenwick, 1994)。 那么,我们能否使两种操作都在亚线性时间内完成呢?答案自然是肯定的。一种简单的技巧是将序列划分为 $\sqrt{n}$ 个桶,每个桶的大小为 $\sqrt{n}$,并创建一个大小为 $\sqrt{n}$ 的附加数组来缓存每个桶的和。更新操作仍然保持在 $O(1)$ 时间内,因为我们只需更新给定索引处的值以及相应桶的和。区间查询现在则可在 $O(\sqrt{n})$ 时间内完成:为求和 $a_i + \cdots + a_j$,我们手动累加从 $a_i$ 到其所在桶末尾的值,以及从 $a_j$ 所在桶开头到 $a_j$ 的值;对于所有介于两者之间的桶,我们则可以直接查找它们的和。 我们可以通过引入额外的缓存层级,以略微增加更新操作的开销为代价,进一步加快区间查询的速度。例如,我们可以将序列划分为 $\sqrt[3]{n}$ 个“大桶”,然后将每个大桶进一步细分为 $\sqrt[3]{n}$ 个“小桶”,每个小桶包含 $\sqrt[3]{n}$ 个值。每个桶的和都被缓存;现在每次更新需要修改三个值,而区间查询则在 $O(\sqrt[3]{n})$ 时间内完成。 以此类推,我们最终会得到一种基于二分治策略的区间和缓存方法,使得更新和区间查询操作的时间复杂度均为2 $O(\log n)$ 。具体而言,我们可以构建一棵完全二叉树3,其叶节点存储序列本身,而每个内部节点则存储其子节点的和。(这对于许多函数式程序员而言应是一个耳熟能详的概念;例如,手指树(finger trees)(Hinze & Paterson, 2006; Apfelmus, 2009)便采用了类似的缓存机制。)由此产生的数据结构通常被称为线段树,4 大抵是因为每个内部节点最终都缓存了底层序列的一个(连续)段的和。 图 2 展示了一棵基于长度为 $n=16$ 的示例数组构建的线段树(为简化起见,我们假设 $n$ 是 2 的幂,尽管将其推广到非 2 的幂的情况亦不难)。树的每个叶节点对应数组中的一个元素;每个内部节点都带有一个灰色条块,显示其所代表的底层数组段。 我们来看如何利用线段树来实现前面所述的两种操作,并使其均能在对数时间内完成。 图 4 阐释了计算区间 $[4 \ldots 11]$ 之和的过程。蓝色节点是我们递归遍历的节点;绿色节点是其范围完全包含在查询范围内、无需进一步递归而直接返回其值的节点;灰色节点则与查询范围不相交,返回零。本例中的最终结果是绿色节点值的总和,$1 + 1 + 5 + (-2) = 5$(不难验证,这确实是区间 $[4 \ldots 11]$ 内的值的和)。 在这个小例子中,看似我们访问了相当大比例的节点,但一般而言,我们访问的节点数量不会超过大约 $4 \log n$ 个。图 5 更清晰地展示了这一点。整棵树中最多只有一个蓝色节点可以拥有两个蓝色子节点,因此,树的每一层最多包含两个蓝色节点和两个非蓝色节点。我们实际上执行了两次二分查找,一次用于寻找查询区间的左端点,另一次用于寻找右端点。 线段树是解决该问题的一种颇为优良的方案:正如我们将在第 2 节中看到的那样,它们与函数式语言契合良好;同时它们也易于进行强大的泛化,例如支持惰性传播的区间更新以及通过共享不可变结构实现持久化更新历史(Ivanov, 2011b)。 芬威克树,或称二叉索引树(Fenwick, 1994; Ivanov, 2011a),是该问题的另一种解决方案。它们在通用性上有所欠缺,但在内存占用方面却极其精简——除了存储树中值的数组之外,几乎不需要任何额外空间——并且实现速度极快。换言之,它们非常适用于诸如底层编码/解码例程之类的应用场景,这些场景不需要线段树所能提供的任何高级特性,但却追求极致的性能。 本节展示了一个典型的 Java 语言芬威克树实现。可见,其实现异常简洁,大体由若干小型循环构成,每个循环迭代仅执行少量的算术与位运算。然而,这段代码究竟在做什么、其工作原理为何,却不甚明了!稍加审视, 我们的目标,并非为此已解决的问题编写优雅的函数式代码。相反,我们的目标在于运用一种函数式的领域特定语言来处理位串,并结合等式推理,从第一性原理出发,推导并阐释这段令人费解的命令式代码——展示函数式思维与等式推理之力,即便用于理解以其他非函数式语言编写之代码亦能奏效。在对线段树(第 2 节)建立更深入的直觉之后,我们将看到芬威克树如何能被视为线段树的一种变体(第 3 节)。随后,我们将绕道探讨二进制补码表示法,开发一个适宜的位操作 DSL,并解释 值得注意的是,本文及后续部分均采用基于 1 的索引方式,即序列中的首个元素索引为 1。此选择之缘由,后文将予以阐明。 本文的 $\log$ 表示以 2 为底的对数,原文使用 $\lg$。 原文是 balanced binary tree,翻译为平衡二叉树或有歧义,此处使用完全二叉树以避免歧义。 此处术语的使用存在一些混淆。截至本文撰写之时,维基百科关于线段树(Wikipedia Contributors, 2024)的条目讨论的是一种用于计算几何的区间数据结构。然而,谷歌搜索“segment tree”的大部分结果都来自算法竞赛领域,其中它指的是本文所讨论的数据结构(例如,参见 Halim et al., 2020, Section 2.8 或 Ivanov, 2011b)。这两种数据结构基本上是不相关的。 下面代码展示了一个在 MoonBit 中实现的简单线段树,其中使用了一些处理索引范围的工具函数,如图 8 所示。我们将线段树存储为一个递归的代数数据类型。
并使用与前一节中递归描述直接对应的代码实现了 区间工具函数: 尽管此实现简单且相对易于理解,但与仅将值序列存储于数组中相比,它引入了相当大的开销。我们可以通过将线段树的所有节点存储在一个数组中,采用如图 9 所示的标准从左至右、广度优先的索引方案,来更巧妙地利用空间(例如,这种方案或其类似方案常用于实现二叉堆)。根节点标号为 1;每当我们向下移动一层,我们就在现有二进制表示后追加一位:向左子节点移动时追加 0,向右子节点移动时追加 1。 因此,每个节点以二进制表示的索引记录了从根节点到达该节点的路径上左右选择的序列。从一个节点移动到其子节点,只需执行一次左位移并视情况加 1 即可;从一个节点移动到其父节点,则执行一次右位移。这便定义了一个从正自然数到无限二叉树节点的双射。若我们将线段树数组标记为 $s_1 \ldots s_{2n-1}$,那么 $s_1$ 存储所有 $a_i$ 的和,$s_2$ 存储 $a_i$ 前半部分的和,$s_3$ 存储后半部分的和,依此类推。$a_1 \ldots a_n$ 本身则存储为 $s_n \ldots s_{2n-1}$。 关键在于,既然沿树递归下降对应于对索引的简单操作,我们所讨论的所有算法都可以直接转换为处理(可变)数组的代码:例如,我们不再存储指向当前子树的引用,而是存储一个整数索引;每当需要向左或向右下降时,我们只需将当前索引乘以 2,或者乘以 2 再加 1。以数组存储树节点还带来了额外的可能性:我们不必总是从根节点开始向下递归,而是可以从某个感兴趣的特定索引出发,反向沿树向上移动。 那么,我们如何从线段树过渡到芬威克树呢?我们从一个看似无关紧要的观察开始:并非所有存储在线段树中的值都是必需的。当然,从某种意义上说,所有非叶节点都是“不必要的”,因为它们代表的是可以轻易从原始序列重新计算出来的缓存区间和。这正是线段树的核心思想:缓存这些“冗余”的和,以空间换时间,使我们能够快速执行任意的更新和区间查询,代价是将所需的存储空间加倍。 但这并非我所指!实际上,存在另一组我们可以舍弃的值,并且这样做仍然能够保持更新和区间查询的对数运行时效。舍弃哪些值呢?很简单:只需舍弃每个右子节点中的数据即可。图 10 展示了我们一直在使用的示例树,但其中每个右子节点的数据已被删除。注意,“每个右子节点”既包括叶节点也包括内部节点:我们舍弃与其父节点关系为右子节点的所有节点相关联的数据。我们将数据被丢弃的节点称为非活跃(inactive)节点,其余节点(即左子节点和根节点)称为活跃(active)节点。我们亦称,以这种方式使其所有右子节点都变为非活跃状态的树为疏树(thinned trees)。 更新一棵疏树颇为容易:只需像以前一样更新相同的节点,忽略对非活跃节点的任何更新即可。但我们如何应答区间查询呢?不难看出,剩余的信息足以重构被丢弃的信息(您或许愿意尝试说服自己这一点:能否在不参考任何先前图示的情况下,推断出图 10 中灰色节点应有的值?)。然而,仅此观察本身并不能为我们提供一个良好的计算区间和的算法。 关键在于考虑前缀和。正如我们在引言以及 2.1 中 给定一棵疏树,原始数组的任意前缀和(并由此引申出任意区间和)均可在对数时间内计算得出,且仅需使用活跃节点的值。 证明 出人意料的是,在处理前缀查询这种特殊情况时,第 1 节中描述并在 2.1 中实现的原始区间查询算法竟能原封不动地奏效!也就是说,当遇到当前节点的范围完全包含在查询范围内的基准情形时——此时我们会返回当前节点的值——这种情况只会在活跃节点上发生。 首先,根节点本身是活跃的,因此查询整个范围是有效的。接下来,考虑我们在某个节点上并递归到其两个子节点的情形。左子节点总是活跃的,因此我们只需考虑递归到右子节点的情况。右子节点的范围不可能完全包含在查询范围内:由于查询范围总是形如 $[1, j]$ 的前缀,若右子节点的范围完全包含在 $[1, j]$ 内,那么左子节点的范围也必定如此——这意味着父节点的范围(即其子节点范围的并集)也必定完全包含在查询范围内。但在那种情况下,我们会直接返回父节点的值,而不会递归到右子节点。因此,当我们确实递归到一个右子节点时,我们最终可能会返回 0,或者可能进一步递归到它的两个孙子节点,但无论如何,我们绝不会尝试去查看右子节点本身的值。 图 11 阐释了在线段树上执行前缀查询的过程。注意,被访问的右子节点要么是蓝色要么是灰色;唯一的绿色节点都是左子节点。 我们应如何在内存中实际存储一棵删减后的线段树?如果我们仔细观察图 10,一种策略便显而易见:只需将每个活跃节点“向下滑动”并向右移动,直至其落入底层数组的一个空位中,如图 12 所示。这在活跃节点与范围 $1 \ldots n$ 内的索引之间建立了一一对应的关系。理解这种索引方案的另一种方式是使用树的后序遍历,跳过非活跃节点,并为遍历过程中遇到的活跃节点赋予连续的索引。我们也可以通过以“右倾”风格绘制树来可视化这一结果(图 13),将每个活跃节点与其存储位置所在的数组槽垂直对齐。 这种将删减后线段树中的活跃节点存储在数组中的方法,正是所谓的芬威克树。有时我也会称其为芬威克数组,意在特别强调其底层的数组数据结构。 诚然,这是一种巧妙的空间利用方式,但关键问题在于如何实现更新和区间查询操作。我们为线段树实现的这些操作,无论是直接在递归数据结构上操作,还是在树存储于数组中时通过对索引进行简单操作,都是通过递归地沿树向下遍历来完成的。然而,当将删减后树的活跃节点存储在芬威克数组中时,哪些数组索引上的操作能够对应于在树中移动,这并非先验可知。为攻克此难题,我们首先需要绕道进入一个用于处理二进制补码数值的领域特定语言。 通常用于实现芬威克树的位技巧依赖于二进制数的二进制补码表示法,该表示法允许以统一的方式表示正数和负数;例如,一个全由 1 组成的位串表示 -1。因此,我们现在转向开发一个嵌入 MoonBit 的领域特定语言,用于操作二进制补码表示。 首先,我们定义一个位 (Bit) 的类型,附带用于求反、逻辑与和逻辑或的函数(注:还有 接下来,我们必须定义位串,即位的序列。与其固定一个特定的位宽,不如使用无限位串会更加优雅1。使用 Lazy List 来表示潜在的无限位串似乎颇具诱惑力,但这会导致一系列问题。例如,无限列表的相等性是不可判定的,而且通常没有办法将一个无限的位列表转换回一个 实际上,我们想要的位串是那些最终恒定的串,即那些最终趋于无限长的全零尾部(代表非负整数)或全一尾部(代表负整数)的串。每个这样的串都有一个有限的表示,因此在 MoonBit 中直接编码最终恒定的位串,不仅能去除垃圾,还能辅助编写一些优雅且停机的算法。 尽管我们已经消除了垃圾值,但仍存在一个问题:同一个值可能存在多个不同的表示。例如, 使用 让我们从一些用于在 trait 让我们用 QuickCheck 来测试一下,验证我们的转换函数: 现在我们可以开始在 一个位序列的最低有效位(Least Significant Bit, LSB)可以定义如下: 注意,我们为 按位逻辑与可以直截了当地定义。注意,我们只需要两种情况;如果输入的有限部分长度不同,与 按位取反同样显然: 上述函数遵循熟悉的模式。我们可以很容易地将它们推广到作用于任意元素类型的最终恒定流,然后用泛型的 我们用通常的进位传播算法来实现加法,并附带一些针对 不难发现这个加法定义是能够停机并产生正确结果的;但我们也可以通过用 QuickCheck 来尝试一下,从而获得相当的信心: 最后,下面这个求反的定义对于任何学过二进制补码算术的人来说可能都很熟悉;我将其留作一个练习,供感兴趣的读者证明对于所有 现在我们拥有了揭开芬威克树实现中第一个谜团的工具。 $$ \forall x : \text{Bits}. \quad \text{lsb}(x) = \text{and}(x, \text{neg}(x)) $$ 证明 通过对 $x$ 进行归纳(译者注:为了便利证明书写,我们将 最后,为了表达我们将在下一节中开发的索引转换函数,我们的 DSL 中还需要一些其他东西。首先是一些用于设置和清除单个位以及测试特定位是否已设置的函数: 我们还需要的是左移和右移,以及一个通用的 部分读者或许能认出无限二进制补码位串即为二进数,也即 p 进数在特定情况 $p=2$ 时的形式,但我们的论述并不依赖于理解此关联。 在推导我们的索引转换函数之前,我们必须处理一个略显棘手的事实。在传统的二叉树索引方案中,如图 9 所示,根节点的索引为 1,每个左子节点的索引是其父节点的两倍,每个右子节点的索引是其父节点的两倍加一。回想一下,在一棵删减后的线段树中,根节点和每个左子节点都是活跃的,而所有右子节点都是非活跃的。这使得根节点成为一个尴尬的特例——所有活跃节点都有偶数索引,除了索引为 1 的根节点。这使得检查我们是否处于一个活跃节点变得更加困难——仅仅查看最低有效位是不够的。 解决这个问题的一个简单方法是直接给根节点赋予索引 2,然后继续使用相同的方案标记其余节点——每个左子节点是其父节点的两倍,每个右子节点是其父节点的两倍加一。这导致了如图 14 所示的索引方式,就好像我们只是取了以 1 为根的树的左子树,并忽略了右子树。当然,这意味着大约一半的可能索引被省略了——但这不成问题,因为我们只会将这些索引作为中间步骤使用,最终会被融合掉。 图 15 展示了一棵二叉树,其中节点以两种不同的方式编号:每个节点的左侧显示其二叉树索引(根节点索引为 2)。每个节点的右侧显示其在芬威克数组中的索引,如果它有的话(非活跃节点右半部分简单地灰色显示)。下方的表格显示了从芬威克数组索引(顶行)到二叉树索引(底行)的映射。作为一个更大的例子,图 16 在更深一层的二叉树上展示了同样的事情。 我们的目标是找到一种方法来计算给定芬威克索引对应的二叉树索引,反之亦然。仔细观察图 16 中的表格,有个模式非常突出。首先,底行的所有数字都是偶数,这恰恰是因为二叉树的编号方式使得所有活跃节点都有偶数索引。其次,我们可以看到偶数 $32, 34 \ldots 46$ 按顺序出现在所有奇数位置上。这些正是树的叶节点,实际上,芬威克数组中每隔一个节点就是来自原始树的叶节点。与它们交替出现的,在偶数位置上的,是数字 $16, 8, 18, 4, \ldots$,它们对应于所有非叶节点;但这些恰好是图 15 中表格底行的二叉树索引序列——因为高度为 4 的树中的内部节点本身构成了一个高度为 3 的树,且节点以相同的顺序出现。 这些观察引出了 5.1 中所示的递推关系,用于计算存储在长度为 $2^n$ 的芬威克数组中的节点的二叉树索引序列 $b_n$:$b_0$ 就是单元素序列 $[2]$,否则 $b_n$ 就是偶数 $2^{n+1}, 2^{n+1} + 2, \ldots, 2^{n+1} + 2^n - 2$ 与 $b_{n-1}$ 交错排列的结果(译者注:代码实现中使用位运算代替乘方运算,在数学推理中,也将 我们可以检验这确实重现了 $n=4$ 时观察到的序列: 令 $s ! k$ 表示列表 $s$ 中的第 $k$ 项(从 1 开始计数),在代码中记为 有了这些准备,我们可以将芬威克到二叉树的索引转换函数定义为
$$ \text{f2b}(n, k) = b_n ! k. $$ 当然,由于 $b_n$ 的长度为 $2^n$,这个函数仅在范围 $[1, 2^n]$ 内有定义。 我们现在可以简化 $$
\begin{align*}
& \text{f2b}(n, (2 \cdot j)) \\
= & b_n ! (2 \cdot j) & \{ \text{f2b} \} \\
= & (\text{interleave}(\text{map}((2 \cdot), [2^n \ldots 2^n + 2^{n-1} - 1]), b_{n-1})) ! (2 \cdot j) & \{ \text{b} \} \\
= & b_{n-1} ! j & \{ \text{interleave-!} \text{ 引理 } \} \\
= & \text{f2b}((n - 1), j). & \{ \text{f2b} \}
\end{align*}
$$ 其中 $(2\cdot)$ 是函数 $$
\begin{align*}
& \text{f2b}(n, (2 \cdot j - 1)) \\
= & b_n ! (2 \cdot j - 1) & \{ \text{f2b} \} \\
= & (\text{interleave}(\text{map}((2 \cdot), [2^n \ldots 2^n + 2^{n-1} - 1]), b_{n-1})) ! (2 \cdot j - 1) & \{ \text{b} \} \\
= & \text{map}((2 \cdot), [2^n \ldots 2^n + 2^{n-1} - 1]) ! j & \{ \text{interleave-!} \text{ 引理 } \} \\
= & 2 \cdot (2^n + j - 1) & \{ \text{map, 代数} \} \\
= & 2^{n+1} + 2j - 2 & \{ \text{代数} \}
\end{align*}
$$ 因此,我们有 $$
\text{f2b}(n, k) =
\begin{cases}
\text{f2b}(n - 1,k / 2) & k \text{ 为偶数} \\
2^{n+1} + k - 1 & k \text{ 为奇数}
\end{cases}
$$ 注意,当 $n = 0$ 时,我们必须有 $k = 1$,因此 $\text{f2b}(0, 1) = 2^{0+1} + 1 - 1 = 2$,(译者注:原文写的 Note that when n = 0, we must have k = 1, and hence, f2b 0 1 = $2^{0+1} + 1 - 1 = 1$, as required, so this definition is valid for all n ≥ 0. 计算有误。根据推导,$f2b(0, 1) = 2 \neq 1$,等于 2 才能对应上我们新的根节点假设)所以这个定义对所有 $n \ge 0$ 都有效。现在将 $k$ 唯一地分解为 $2^a \cdot b$,其中 $b$ 是奇数。那么通过归纳我们可以看到 $$ \text{f2b} (n, 2^a \cdot b) = \text{f2b}(n - a, b) = 2^{(n-a)+1} + b - 1. $$ 换句话说,计算 容易使用 QuickCheck 验证这在范围 $[1, 2^4]$ 上产生与原始的 现在我们转向推导 $$ \text{b2f} (n, 2^c + d) = 2^{n-c+1} \cdot (d + 1). $$ 换句话说,给定输入 $2^c + d$,我们减去最高位 $2^c$,加 1,然后左移 $n - c + 1$ 次。同样,存在一个更简单的方法:我们可以先加 1(注意因为 $d \lt 2^{c-1}$,加 1 不会干扰 $2^c$ 处的位),然后左移足够多次,使最左边的位移到位置 $n + 1$,最后移除它。即: 验证: 我们现在终于可以推导出在芬威克数组索引上移动所需的运算了,方法是从二叉索引树上的操作开始,并通过与芬威克索引的转换进行变换。首先,为了融合掉由此产生的转换,我们需要几个引理。 对于所有为奇数(即以 I 结尾)的 $bs : \text{Bits}$, 证明 两者均由定义直接可得。 以下两条定理对所有 Bits 值均成立: 证明 简单的 最后,我们需要一个关于将零位移入和移出值右侧的引理。 对于所有 $0 \lt x \lt 2^{n+2}$, $$ \text{while}(\text{not}(\text{test}(\cdot, n + 1)), \text{shl}, \text{while}(\text{even}, \text{shr}, x)) = \text{while}(\text{not}(\text{test}(\cdot, n + 1)), \text{shl}, x) $$ (注:$\text{test}$ 在代码中是 证明 直观上,这表明如果我们先移出所有零位,然后左移直到第 $n+1$ 位被设置,这可以通过完全忘记右移来获得相同的结果;移出零位然后再将它们移回来应该是恒等操作。 形式上,证明通过对 $x$ 进行归纳。如果 $x = xs : \text{I}$ 为奇数,等式立即成立,因为 $\text{while}(\text{even}, \text{shr}, x) = x$。否则,如果 $x = xs : \text{O}$,在左侧,O 会被 $\text{shr}$ 立即丢弃,而在右侧,$xs : \text{O} = \text{shl}(xs)$,并且由于 $xs \lt 2^{n+1}$,额外的 $\text{shl}$ 可以被吸收到 $\text{while}$ 循环中。剩下的就是归纳假设。 有了这些引理在手,让我们看看如何在芬威克数组中移动以实现 让我们看看如何推导出这种行为。
要在二叉索引方案下找到一个节点的最近活跃父节点,我们首先向上移动到直接父节点(通过将索引除以二,即执行一次右位移);然后只要当前节点是右子节点(即索引为奇数),就继续向上移动到下一个直接父节点。这产生了如下定义: 这就是为什么我们使用了根节点索引为 2 的略显奇怪的索引方案——否则这个定义对于任何活跃父节点是根节点的节点都不起作用! 现在,要推导出芬威克索引上的相应操作,我们通过与芬威克索引的转换进行共轭,计算如下。为了使计算更易读,每一步中被重写的部分都用下划线标出。 $$
\begin{align*}
& \underline{\text{b2f}(n, \text{activeParentBinary}(\text{f2b}(n, \cdot)))} \\ & \{ \text{展开定义} \} \\
= & \text{unshift}(n + 1, \underline{\text{inc}(\text{while}(\text{odd}, \text{shr}}, \text{shr}(\text{dec}(\text{shift}(n + 1, \cdot)))))) \\ & \{ \text{引理 (while-inc-dec)} \} \\
= & \text{unshift}(n + 1, \text{while}(\text{even}, \text{shr}, \text{inc}(\underline{\text{shr}(\text{dec}}(\text{shift}(n + 1, \cdot)))))) \\ & \{ \text{引理 (shr-inc-dec); shift(n+1, x) 总是奇数} \} \\
= & \text{unshift}(n + 1, \text{while}(\text{even}, \text{shr}, \underline{\text{inc}(\text{shr}}(\text{shift}(n + 1, \text{dec}(\cdot)))))) \\ & \{ \text{引理 (shr-inc-dec)} \} \\
= & \text{unshift}(n + 1, \underline{\text{while}(\text{even}, \text{shr}, \text{shr}}(\text{inc}(\text{shift}(n + 1, \cdot))))) \\ & \{ \text{while(even, shr, shr(x)) = while(even, shr, x) 在偶数输入上} \} \\
= & \underline{\text{unshift}(n + 1}, \text{while}(\text{even}, \text{shr}, \text{inc}(\text{shift}(n + 1, \cdot)))) \\ & \{ \text{unshift} \} \\
= & \text{clear}(n + 1, \underline{\text{while}(\text{not}(\text{test}(n + 1, \cdot)), \text{shl}, \text{while}(\text{even}, \text{shr}}, \text{inc}(\underline{\text{shift}(n + 1, \cdot)})))) \\ & \{ \text{引理 (shl-shr); shift} \} \\
= & \text{clear}(n + 1, \text{while}(\text{not}(\text{test}(n + 1, \cdot)), \text{shl}, \text{inc}(\text{while}(\text{even}, \text{shr}, \text{set}(n + 1, \cdot))))) \\
\end{align*}
$$ 在最后一步中,由于输入 $x$ 满足 $x \le 2^n$,我们有 $\text{inc}(\text{shift}(n + 1, x)) \lt 2^{n+2}$,因此引理 shl-shr 适用。 从右到左阅读,我们刚刚计算出的流水线执行以下步骤: 直观地说,这看起来很像加上 LSB!一般来说,要找到 LSB,必须移过连续的 0 位,直到找到第一个 1;问题是如何跟踪移过了多少个 0 位。 为了使这一点更形式化,我们首先定义一个辅助函数 对于所有 $x : \text{Bits}$, $\text{add}(x, \text{lsb}(x)) = \text{atLSB}(\text{inc}, x)$ 且 $\text{subtract}(x, \text{lsb}(x)) = \text{atLSB}(\text{dec}, x)$。 (注:代码中 $\text{atLSB}$ 的定义为 证明 对 $x$ 进行简单的归纳即可。 我们可以将“带哨兵的移位”方案与 令 $n \ge 1$ 且令 $f : \text{Bits} \to \text{Bits}$ 是一个函数,使得 那么对于所有 $0 \lt x \lt 2^n$,
$$ \text{unshift}(n + 1, f(\text{shift}(n + 1, x))) = \text{atLSB}(f, x). $$ 证明相当繁琐但并非特别具有启发性,因此我们省略它(一个包含完整证明的扩展版本可以在作者的网站上找到)。然而,我们确实注意到 加上 LSB 是沿芬威克索引树向上移动到最近活跃父节点的正确方法,即
$$\begin{align*} & \text{activeParentFenwick}(x) \\ &= \text{b2f}(n, \text{activeParentBinary}(\text{f2b}(n, x))) \\ &= \text{add}(x, \text{lsb}(x)) \end{align*} $$
在范围 $[1, 2^n)$ 上处处成立。(我们排除了 $2^n$,因为它对应于芬威克索引方案下的树根。) 证明 $$
\begin{aligned}
& \text{b2f}(n, \text{activeParentBinary}(\text{f2b}'(n, x))) \\
= & \text{unshift}(n + 1, \text{inc}(\text{shift}(n + 1, x))) & \{ \text{先前的计算} \} \\
= & \text{atLSB}(\text{dec}, x) & \{ \text{引理 (sentinel)} \} \\
= & \text{add}(x, \text{lsb}(x)) & \{ \text{引理 (add-lsb)} \}
\end{aligned}
$$ 我们可以进行类似的过程来推导前缀查询的实现(据称它涉及减去 LSB)。同样,如果我们想计算 $[1, j]$ 的和,我们可以从芬威克数组中的索引 $j$ 开始,它存储了结束于 $j$ 的唯一段的和。如果索引 $j$ 处的节点存储了段 $[i, j]$,我们接下来需要找到存储结束于 $i-1$ 的段的唯一节点。我们可以重复这样做,一路累加段的和。 从图 20 中寻找灵感,我们可以看到我们想要做的是找到我们最近的非活跃父节点的左兄弟,也就是说,我们向上走直到找到第一个作为右子节点的祖先,然后移动到它的左兄弟。在二叉索引方案下,这可以简单地实现为: 减去 LSB 是将芬威克树向上移动到覆盖当前段的之前段的活动节点的正确方法、
$$\begin{align*} & \text{prevSegmentFenwick}(x) \\ &= \text{b2f}(n, \text{prevSegmentBinary}(\text{f2b}(n, x))) \\ &= \text{subtract}(x, \text{lsb}(x)) \end{align*} $$
在范围 $[1, 2^n)$ 上处处成立。 证明 $$
\begin{aligned}
& \text{b2f}(n, \text{prevSegmentBinary}(\text{f2b}(n, x))) \\
& \{ \text{展开定义} \} \\
= & \text{unshift}(n + 1, \underline{\text{inc}(\text{dec}}(\text{while}(\text{even}, \text{shr}, \text{dec}(\text{shift}(n + 1, x)))))) \\
& \{ \text{引理 (while-inc-dec)} \} \\
= & \underline{\text{unshift}(n + 1}, \text{while}(\text{even}, \text{shr}, \text{dec}(\text{shift}(n + 1, x)))) \\
& \{ \text{unshift} \} \\
= & \text{clear}(n + 1, \underline{\text{while}(\text{not}(\text{test}(n + 1, \cdot)), \text{shl} , \text{while}(\text{even}, \text{shr}}, \text{dec}(\text{shift}(n + 1, x)))))) \\
& \{ \text{引理 (shl-shr)} \} \\
= & \underline{\text{clear}(n + 1, \text{while}(\text{not}(\text{test}(n + 1, \cdot)), \text{shl}}, \text{dec}(\text{shift}(n + 1, x)))) \\
& \{ \text{unshift} \} \\
= & \text{unshift}(n + 1, \text{dec}(\text{shift}(n + 1, x))) \\
& \{ \text{引理 (sentinel)} \} \\
= & \text{atLSB}(\text{dec}, x) \\
& \{ \text{引理 (add-lsb)} \} \\
= & \text{subtract}(x, \text{lsb}(x)) \\
\end{aligned}
$$ 据我所知,从历史上看,芬威克树并非如本文所呈现的那般,作为线段树的一种优化而被开发出来。本文所叙仅仅是一种虚构的思想别史(但希望能有所启发),旨在彰显函数式思维、领域特定语言以及等式推理在探索不同结构与算法之间关系时的力量。作为未来工作,探索前文提及的线段树的某些泛化推广,考察是否能从中推导出支持额外操作的类芬威克结构,将不失为一桩趣事。 大家好!今天我想和大家分享如何用 MoonBit 语言实现一个 LRU(Least Recently Used,最近最少使用)缓存算法。无论你是刚接触 MoonBit,还是想了解 LRU 算法的实现细节,这篇文章都会带你深入了解这个经典而实用的算法。 什么是 LRU 缓存? LRU 缓存是一种常见的缓存淘汰策略,它基于一个简单的假设:最近访问过的数据在不久的将来很可能再次被访问。因此,当缓存空间不足需要淘汰数据时,应该优先淘汰最长时间未被访问的数据。 一个日常生活的例子 想象你的书桌上只能放 5 本书。每次你需要一本新书,但书桌已满时,你会把哪本书放回书架?最合理的选择是把最久没看的那本书放回去。这就是 LRU 策略的直观体现。 技术应用场景 LRU 缓存在计算机系统中有广泛的应用: LRU 缓存的实际例子 假设我们有一个容量为 3 的 LRU 缓存,初始为空。现在执行以下操作: 通过这个例子,我们可以看到 LRU 缓存如何维护“最近使用“的顺序,以及如何在缓存满时进行淘汰。 LRU 缓存的核心操作 一个标准的 LRU 缓存需要支持以下两个核心操作: get(key): 获取缓存中键对应的值 put(key, value): 向缓存中插入或更新键值对 这两个操作的时间复杂度都应该是 O(1),这就需要我们精心设计数据结构。 为什么需要特殊的数据结构? 实现一个高效的 LRU 缓存面临两个主要挑战: 如果只用数组,查找需要 O(n) 时间;如果只用哈希表,无法跟踪使用顺序。因此,我们需要结合两种数据结构。 实现思路:哈希表 + 双向链表 LRU 缓存的经典实现方式是结合使用: 这种组合让我们能够同时满足快速查找和顺序维护的需求。 接下来,我们将用 MoonBit 语言一步步实现这个数据结构,从基础的节点定义,到完整的 LRU 缓存功能。 在实现 LRU 缓存之前,我们首先需要定义一些基础的数据结构。正如前面所说,我们需要结合哈希表和双向链表来实现高效的 LRU 缓存。 节点结构 我们先定义双向链表的节点结构。每个节点需要存储键值对,并且包含指向前一个和后一个节点的引用: 在这个节点结构中有几个有趣的 MoonBit 特性值得我们关注: 泛型参数 可变字段 可选类型 简单构造函数: LRU 缓存结构 接下来,我们来定义 LRU 缓存的主体结构: 这个结构包含三个关键字段: capacity:定义了缓存可以存储的最大键值对数量。 dummy:一个特殊的哑元节点,不存储实际的键值对,而是用来简化链表操作。使用哑元节点是一个常见的编程技巧,它可以帮助我们避免处理空链表和边界条件的特殊情况。 key_to_node:一个从键到节点的映射表,使我们能够在 O(1) 时间内通过键找到对应的节点。 为什么使用哑元节点? 哑元节点的使用是一个很巧妙的设计。我们将在链表中使用一个环形结构,其中哑元节点同时充当链表的“头“和“尾“: 这样的设计使得我们在处理节点插入和删除时,不必担心空链表的特殊情况,代码逻辑会更加统一和清晰。 通过这两个基础数据结构,我们已经为实现一个高效的 LRU 缓存打下了基础。在下一部分,我们将开始实现 LRU 缓存的构造函数和核心操作。 现在我们已经定义好了基础数据结构,接下来需要实现 LRU 缓存的构造函数。构造函数是任何数据结构的起点,它负责正确初始化内部状态。 构造函数的设计 在设计 LRU 缓存的构造函数时,我们需要考虑: 让我们看看如何用 MoonBit 实现这个构造函数: 这段代码做了几件重要的事情: 泛型约束:注意 默认值参数:我们需要 自引用环:我们将哑元节点的 返回结构体实例:使用了 MoonBit 的结构体字面量语法 为什么要形成环形结构? 你可能注意到了,我们将哑元节点的前驱和后继都指向了自身,形成了一个环。这样做的好处是: 在空链表中,哑元节点既是“头“也是“尾“。当我们添加实际节点时,它们会被插入到这个环中,而哑元节点始终保持在原位,帮助我们定位链表的逻辑起点和终点。 示意图说明 初始状态下,我们的链表结构如下: 添加一个节点 A 后: 添加另一个节点 B(放在最近使用的位置)后: 在这个结构中, 这样的设计为我们后面实现 接下来我们要实现 LRU 缓存的两个核心操作: get 方法实现 这个实现看起来很简单,但它内部调用了 这里我们用到了两个辅助方法 put 方法实现 检查键是否已存在: 创建新节点: 添加到链表和哈希表: 检查容量并可能淘汰: LRU 算法的核心思想 通过这两个方法,我们可以看到 LRU 算法的核心思想: 这种设计确保了我们总是保留最有可能再次被访问的数据,而丢弃最不可能再次被访问的数据,从而最大化缓存的命中率。 在下一部分,我们将详细介绍 在上一部分中,我们实现了 LRU 缓存的核心操作 push_front 方法实现 这个方法的逻辑虽然只有几行,但需要仔细理解: 通过这四步,我们完成了在链表头部插入新节点的操作。注意我们使用了 remove 方法实现 这个方法的实现非常直观: 通过这两步,节点就从链表中“断开“了,不再是链表的一部分。 为什么这两个操作如此重要? 这两个看似简单的操作是整个 LRU 缓存算法的关键: 通过这两个基本操作,我们能够维护一个按照“最近使用“到“最久未使用“排序的双向链表,从而实现 LRU 缓存的核心功能。 双向链表操作的细节 在处理双向链表时,容易出现的错误是指针操作顺序不当导致链表断裂或形成环。我们的实现避免了这些问题: 这种实现方式确保了链表操作的安全性和正确性。 使用哑元节点的优势 回顾一下我们设计中使用的哑元节点(dummy node),它带来了以下优势: 有了这些辅助操作,我们的 LRU 缓存算法就更加完整了。接下来,我们会添加一些额外的实用方法,让我们的 LRU 缓存更加易用。 我们已经实现了 LRU 缓存的核心功能,包括基本数据结构、构造函数、核心操作 获取缓存大小 首先,我们实现一个方法来获取当前缓存中的元素数量: 这个方法非常简单,直接返回哈希表的大小,因为哈希表中的每一项都对应缓存中的一个元素。 检查缓存是否为空 接下来,我们添加一个方法来检查缓存是否为空: 这个方法检查哈希表是否为空,从而判断整个缓存是否为空。 检查键是否存在 最后,我们实现一个方法来检查缓存中是否存在某个键: 这个方法直接利用哈希表的 这些辅助方法的意义 虽然这些方法看起来很简单,但它们对于实际使用 LRU 缓存非常有价值: 这些辅助方法体现了良好的 API 设计原则 —— 简单、一致且易于使用。通过提供这些方法,我们的 LRU 缓存实现更加健壮和用户友好。 实际应用示例 这些辅助方法在实际应用中非常有用,例如: 这些方法虽然简单,但它们大大增强了 LRU 缓存的实用性。通过这些辅助方法,我们的 LRU 缓存实现已经相当完整和实用。 终于到了我们 LRU 缓存实现之旅的终点。这一路走来,我们从基本概念开始,一步步构建了一个完整的 LRU 缓存。说实话,当我第一次接触 LRU 算法时,就被它简单而优雅的设计所吸引。在实现过程中,我不仅体会到了算法的精妙之处,也感受到了 MoonBit 语言的表达力。 回顾整个实现过程,我最满意的是数据结构的选择。哈希表和双向链表的组合虽然是经典方案,但在 MoonBit 中实现时,语言本身的特性让代码显得格外简洁。特别是哑元节点的使用,解决了链表操作中的边界情况,让代码逻辑更加一致。这种小技巧看似简单,却能大幅简化实现,减少潜在的错误。 在编写过程中,我发现 MoonBit 的类型系统非常适合这类数据结构的实现。泛型让我们的缓存可以适用于各种类型的键值对,而可选类型(Option 类型)则优雅地处理了可能不存在的值的情况。与其他语言相比,不必担心空指针异常是一种解脱,让我可以更专注于算法本身的逻辑。 对我而言,编写 说到实际应用,这种 LRU 缓存在日常开发中其实非常实用。我曾在一个网页应用中使用类似的缓存来存储频繁访问的数据,显著提升了应用响应速度。见过太多项目因为缺乏合理的缓存策略而性能低下,一个好的 LRU 实现往往能起到事半功倍的效果。 当然,这个实现还有改进空间。比如添加线程安全支持,或者引入基于时间的过期策略。在实际项目中,我会考虑根据具体需求扩展这些功能。不过,目前的实现已经涵盖了 LRU 缓存的核心功能,足以应对大多数场景。 我最大的收获可能是深入理解了算法与数据结构如何相互配合。LRU 缓存的优雅之处在于它巧妙地结合了两种数据结构,各取所长,达到了理想的性能。这种思路启发我在面对其他问题时,不要局限于单一的数据结构,而是思考如何组合现有工具来获得最佳解决方案。 最后,希望这个 LRU 缓存的实现过程对你有所帮助。无论你是在学习 MoonBit 语言,还是想深入了解缓存算法,我都希望这篇文章能给你一些启发。编程的乐趣不仅在于解决问题,还在于创造优雅的解决方案。在这个意义上,LRU 缓存是一个小巧而完美的例子。 如果你有任何问题或改进建议,欢迎在 Github 留言讨论。毕竟,代码和思想总是在交流中不断完善的。 在静态类型编程语言的演进历程中,类型推断(type inference)机制始终扮演着至关重要的角色。
它允许程序员省略那些可由上下文导出的类型标注,从而极大地降低了代码的冗余度,
使得程序无论在阅读还是编写上都更为便捷。 在这一背景下,System $F_\leq$ 堪称一座里程碑式的理论高峰。
它优雅地统一了两种在现代编程中至关重要的概念:源自面向对象编程、
为代码复用与抽象提供极大便利的子类型化(subtyping),
以及作为泛型编程基石的非直谓多态(impredicative polymorphism)。
然而,一个严峻的现实阻碍了其在实践中的广泛应用:
其强大的表达能力,使得完全类型推断(complete type inference)被证明是不可判定的(undecidable)难题。 本文基于 Pierce 与 Turner 的研究 Local Type Inference,
但也关注工程实践。
它提出了一条迥然不同的路径:摒弃对「完全性」的执着,转而探索一种更简单、更务实的部分类型推断(partial type inference)。其核心理念,在于引入一个额外的简化原则 —— 局部性(locality)。
所谓「局部」,意指任何缺失的类型标注,都应仅仅依据其在语法树上的相邻节点信息来恢复,而不引入任何长距离的约束(例如 Algorithm J 中的那种全局性的合一变量)。 对于初次接触编程语言理论的读者而言,文中遍布的数学符号与推导规则或许会显得有些陌生和令人生畏。
请不必担忧。这些形式化工具并非为了故作高深,恰恰相反,
它们是为了达到自然语言难以企及的精确性(precision)与无歧义性(unambiguity)。
本节将提供一份阅读这些规则的简单指南,熟悉的读者可以直接跳过。 读者可以将这些规则,看作是一门编程语言最根本的「物理定律」。它们以一种极为严谨的方式,
定义了什么样的程序是结构良好、有意义的,而什么样的程序则不是。 本文中的大多数规则,都呈现为如下的结构:
$$\frac{\text{前提}_1 \quad \text{前提}_2 \quad ...}{\text{结论}} \quad (\text{规则名称})$$
这条长长的横线,是理解一切的核心。 在规则的前提与结论中,您会反复看到一种形如 $\Gamma \vdash e : T$ 的核心判断(judgment)。让我们来拆解它的每一个符号: 将它们组合在一起,$\Gamma \vdash e : T$ 这整个判断的直白解读就是:「在上下文 $\Gamma$ 所提供的已知条件下,我们可以推导出(或证明),程序项 $e$ 拥有类型 $T$。」 在放弃了对「完全类型推断」的追求之后,一个至关重要的问题便浮现出来:一个「部分」类型推断算法,其推断能力需要达到何种程度,才算是「足够」?一个极具实践智慧的回答:一个好的部分类型推断算法,其核心使命在于消除那些既普遍又愚蠢的类型标注。 此处的「愚蠢」与「合理」相对。「合理的」标注,如顶级函数定义中对其参数的类型声明,通常能作为有价值的、且经由编译器检查的文档,帮助人们理解代码。「愚蠢的」标注则恰恰相反,它们徒增代码的冗余,却几乎不提供任何有用的信息。可以想见,在一个完全显式类型的语言中,任何人都不会愿意去书写或阅读 Pierce 对十几万行 ML 代码的调研,揭示了三种最主要的「愚蠢标注」来源: 基于上述的定量观察,我们可以勾画出一个「足够」的部分类型推断算法的轮廓: 为了实现我们的目标,我们需要设计一套高效的策略来处理上述三种类型推断的场景。
下面的是两种本文将要介绍的主要策略: 这两项技术均恪守「局部性」原则,即所有推断所需的信息都只在语法树的相邻节点间传递,不涉及长距离的依赖或全局性的合一变量。 在严谨地探讨类型推导这一议题之前,我们必须首先清晰地界定其推断的目标——一个无歧义的、
被完全标注的内核语言(internal language)。此语言是编译器内部的「真实」表达,亦是程序员书写的、
允许省略标注的外部语言(external language)所要翻译成的最终形式。
本文所用的内核语言,源自 Cardelli 与 Wegner 提出的,融合了子类型化与非论域性多态的著名演算 System $F_\leq$,
但在此基础上我们增设了 $\bot$ (Bottom) 类型,为了保证上确界和下确界的存在,这种代数结构的完备性,
是后续章节中约束求解算法得以简洁、确定地运行的根本保障。此外它也可以被用作那些永不返回的表达式(如抛出异常的函数)的结果类型,
我们先定义形式语言如下
(注:横线是序列记号 $\overline{X} = X_1, X_2, \dots, X_n$,类似的,$\overline{x} : \overline{T} = x_1 : T_1, \dots, x_n : T_n$): $$
\begin{array}{ll}
T ::= X & \text{type variable} \\
\quad~\mid~ \top & \text{maximal type} \\
\quad~\mid~ \bot & \text{minimal type} \\
\quad~\mid~ \forall \overline{X} . \overline{T} \rightarrow T & \text{function type} \\[1em]
e ::= x & \text{variable} \\
\quad~\mid~ \text{fun}[ \overline{X} ]\, ( \overline{x} : \overline{T} )\, e & \text{abstraction} \\
\quad~\mid~ e[ \overline{T} ]\, ( \overline{e} ) & \text{application} \\[1em]
\Gamma ::= \bullet & \text{empty context} \\
\quad~\mid~ \Gamma, x : T & \text{variable binding} \\
\quad~\mid~ \Gamma, X & \text{type variable binding}
\end{array}
$$ 我们可将上面的形式语言简单翻译到下面的 MoonBit 代码,
其中 子类型关系,记作 $S \lt: T$(读作 $S$ 是 $T$ 的一个子类型),是本形式系统的核心。它定义了类型之间的一种「可替换性」:凡是需要类型 $T$ 的地方,都可以安全地使用一个类型为 $S$ 的项来代替。 与许多理论文献中的定义不同,本文特意选择了一种算法化(algorithmic)的方式来呈现子类型关系。这意味着,定义中仅包含一组最核心的、可直接用于实现判定的规则,而像传递性(transitivity)这样通常作为公理的性质,在此系统中则成为了可被证明的引理。这种风格使得定义本身更接近于一个类型检查算法的规约: $$
\begin{array}{ll}
X \lt: X & \text{(S-Refl)} \\[1em]
T \lt: \top & \text{(S-Top)} \\[1em]
\bot \lt: T & \text{(S-Bot)} \\[1em]
\dfrac{
\overline{T} \lt: \overline{R} \quad S \le: U
}{
\forall \overline{X}. \overline{R} \rightarrow S \lt: \forall \overline{X}. \overline{T} \rightarrow U
}
& \text{(S-Fun)}
\end{array}
$$ 其中 $\overline{T} \lt: \overline{R}$ 成立当且仅当 $\text{len}(T) = \text{len}(S) \land \forall 1 \leq i \leq \text{len}(S). S_i \lt: T_i$。
S-Fun 规则体现了函数类型子类型化的核心特征:在参数类型上是逆变(contravariant)的(子类型关系的箭头方向反转),而在返回类型上是协变(covariant)的(子类型关系箭头方向保持不变)。读者可以自己尝试一下将上文的形式语言翻译到 MoonBit 的一个谓词函数,或参考下面折叠起来的代码片段。 为了支持后续的约束求解算法,系统必须能计算任意两个类型的最小上界(join, 记作 $\lor$)和最大下界(meet, 记作 $\land$)。得益于 $\bot$ 和 $\top$ 的存在,这两个运算在本系统中是全函数(total functions),即对于任意一对类型,其界都必然存在。下面我们给出这两个运算的定义: 最小上界 $S \vee T$ 最大下界 $S \wedge T$ 通过简单的结构归纳法可以证明,这两个运算满足以下性质: 这里同样鼓励读者自己进行代码翻译,答案可展开下面的代码片段。 在 MoonBit 代码中我们将 $S \vee T$ 实现为 在定义了类型与子类型关系之后,我们便可以给出内核语言的类型定则。这些规则定义了类型判断(typing judgment)的形式 $\Gamma \vdash e : T$,意为「在上下文 $\Gamma$ 中,项 $e$ 拥有类型 $T$ 」。 与子类型关系的定义一脉相承,这里的类型定则同样采用了一种算法化的呈现方式。且省略了传统类型系统中常见的包容规则(subsumption,若 $e$ 的类型为 $S$ 且 $S \lt: T$,则 $e$ 的类型亦可为 $T$)。 通过省略此规则,本系统为每一个可被类型化的项,都计算出一个唯一的、最小的类型,作者称之为该项的显式类型(manifest type)。这一设计选择,并不改变语言中可被类型化的项的集合,而只是确保了任何一个项的类型推导路径都是唯一的。这极大地增强了系统的可预测性。 变量 (Variable) $$
\frac{}{\Gamma \vdash x : \Gamma(x)} \quad (\text{Var})
$$ 抽象 (Abstraction)
此规则统一了传统的项抽象与类型抽象。 $$
\frac{\Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e : T}{\Gamma \vdash \mathbf{fun}[\overline{X}] (\overline{x}:\overline{S}) e : \forall \overline{X}.\overline{S} \to T} \quad (\text{Abs})
$$ 若想要求解 $\mathbf{fun}[\overline{X}] (\overline{x}:\overline{S})$ 的类型,必须在上下文 $\Gamma$ 中添加类型变量 $\overline{X}$ 和值变量 $\overline{x}:\overline{S}$ 的绑定。然后,在这个扩展的上下文中,推导函数体 $e$ 的类型为 $T$。最终,整个函数的类型便是 $\forall \overline{X}.\overline{S} \to T$。 应用 (Application)
此规则同样统一了传统的项应用与多态应用。它首先推导函数 $$
\frac{\Gamma \vdash f : \forall \overline{X} . \overline{S} \to R \quad \Gamma \vdash \overline{e} \lt: [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f[\overline{T}] (\overline{e}) : [\overline{T}/\overline{X}]R} \quad (\text{App})
$$ 其中,记法 $\Gamma \vdash \overline{e} \lt: [\overline{T}/\overline{X}]\overline{S}$ 是一个缩写,表示 $\Gamma \vdash \overline{e} \lt: \overline{U}$,然后验证 $\overline{U} \lt: [\overline{T}/\overline{X}]\overline{S}$。最终,整个应用表达式的结果类型,是通过将实际类型参数 $\overline{T}$ 代入函数原始返回类型 $R$ 中得到的。 这里出现了一个新的记号 $[\overline{T}/\overline{X}]R$,
它表示将类型参数 $\overline{X}$ 替换为实际类型 $\overline{T}$ 后的结果类型。
这个记号在后续的代码中会频繁出现。
下面的代码定义 Bot 应用 (Bot Application)
$\bot$ 类型的引入,要求我们补充一条特殊的应用规则,以维护系统的类型安全(type soundness)。
由于 $\bot$ 是任何函数类型的子类型,一个类型为 $\bot$ 的表达式应当可以被应用于任何合法的参数,而不会产生类型错误。 $$
\frac{\Gamma \vdash f : \bot \quad \Gamma \vdash \overline{e} : \overline{S}}{\Gamma \vdash f[\overline{T}] (\overline{e}) : \bot} \quad (\text{App-Bot})
$$ 此规则规定,当一个类型为 $\bot$ 的项被应用时,无论参数为何,整个表达式的结果类型也是 $\bot$,这正是我们能给出的最精确(即最小)的结果类型。 这些规则共同保证了本类型系统的一个关键性质,即显式类型的唯一性(Uniqueness of Manifest Types):若 $\Gamma \vdash e : S$ 且 $\Gamma \vdash e : T$,那么必有 $S=T$。 截至目前,我们已经定义了内核语言的类型规则,
但是距离我们的目标还有很大距离:核心语言要求我们做出很多注解,
包括多态实例化时需要提供的类型参数,因为这在代码中非常常见,因此这是我们本节首要解决的痛点。 此即局部类型参数合成(Local Type Argument Synthesis)的目标:允许程序员在调用多态函数时,安全地省略其类型参数,写成 $\text{id}(3)$ 而不是 $\text{id}[\mathbb{Z}](3)$ 的形式。省略类型参数后,一个核心挑战随之而来:对于一个给定的应用,如 $\text{id} (x)$(其中 $x : \mathbb{Z}$,且 $\mathbb{Z} \lt: \mathbb{R}$),通常存在多种合法的类型参数实例化方案,例如这里的 $\text{id} [\mathbb{Z}](x)$ 或 $\text{id} [\mathbb{R}](x)$。我们必须确立一个清晰的标准来做出选择:选择能为整个应用表达式带来最精确(即最小)结果类型的类型参数。在 $\text{id} (x)$ 的例子中,由于 $\text{id} [\mathbb{Z}](x)$ 的结果类型 $\mathbb{Z}$ 是 $\text{id} [\mathbb{R}](x)$ 的结果类型 $\mathbb{R}$ 的一个子类型,前者显然是更优、更具信息量的选择。 然而,这种基于「最佳结果类型」的局部策略并非万能。在某些情况下,「最佳」解可能并不存在。例如,假设一个函数 $f$ 的类型为 $\forall X. () \to (X \to X)$。对于应用 $f()$,$f[\mathbb{Z}]()$ 和 $f[\mathbb{R}]()$ 都是合法的补全,其结果类型分别为 $\mathbb{Z} \to \mathbb{Z}$ 和 $\mathbb{R} \to \mathbb{R}$。这两种函数类型在子类型关系下是不可比较的,因此不存在一个唯一的最小结果类型。在这种情况下,局部合成宣告失败。 回顾之前的核心语言定义,我们要求 application 构造的形式为 $e[\overline{T}](\overline{e})$,
也就是说我们手动填写了类型参数 $\overline{T}$,规则 这里加入了新的表达式结构 $$
\frac{\text{magic we don't know}}{\Gamma \vdash f (\overline{e}) : [\overline{T}/\overline{X}]R} \quad (\text{App-Magic})
$$ 身为人类我们可以用直觉来制定规则,甚至设计出一些无法写成代码的声明式规则,
精确地定义「何为一次正确的、最优的类型参数推断」: $$
\frac{
\begin{array}{l}
\Gamma \vdash f : \forall \overline{X}. \overline{T} \to R
\qquad \exists \overline{U}
\\
\Gamma \vdash \overline{e} : \overline{S}
\qquad
|\overline{X}| > 0
\qquad
\overline{S} \lt: [\overline{U}/\overline{X}]\overline{T}
\\
\text{forall} (\overline{V}). \overline{S} \lt: [\overline{V}/\overline{X}]\overline{T} \implies [\overline{U}/\overline{X}]R \lt: [\overline{V}/\overline{X}]R
\end{array}
}{\Gamma \vdash f(\overline{e}) : [\overline{U}/\overline{X}]R} \quad (\text{App-InfSpec})
$$ 此处我们使用存在量化 $\exists \overline{U}$,并且要求 $\overline{U}$ 满足很多条件。
例如 $\overline{S} \lt: [\overline{U}/\overline{X}]\overline{T}$ 为合法性约束。
它规定我们所选定的类型参数 $\overline{U}$ 必须是合法的。
所谓合法,即指将 $\overline{U}$ 代入函数的形式参数类型 $\overline{T}$ 后,实际参数的类型 $\overline{S}$ 必须是其子类型。
更重要的是最后一条 $\text{forall} (\overline{V}). \overline{S} \lt: [\overline{V}/\overline{X}]\overline{T} \implies [\overline{U}/\overline{X}]R \lt: [\overline{V}/\overline{X}]R$ 规则,
它要求我们对所有可能的类型参数元组 $\overline{V}$ 进行考量,
这可以转化为对潜在无限空间 $\overline{V}$ 进行搜索的过程,是典型的非构造性描述,
我们无法在计算机中实现它。 至此,我们的目标已经明确:我们需要一个真正可执行的算法,其结果与 (App-InfSpec) 一致,
但不需要我们进行非构造性的搜索和回溯。这正是「约束生成」这一步骤所要扮演的角色。
它的设计动机,源于对问题本身的一次精妙的视角转换。 与其将类型参数推断视为一个在无限可能性中「寻找并验证最优解」的搜索问题,
不妨将其重构为一个类似于解代数方程的「求解未知数边界」的问题。
我们不再去猜测类型参数 $\overline{X}$ 可能是什么,
而是通过分析子类型关系本身,去推导出 $\overline{X}$ 必须满足的条件。 观察到我们的规则存在子类型约束,不妨考虑一般情况 $S \lt: T$,
这本身就隐含着对其构成部分(包括其中的未知变量)的约束。
若 $X$ 是 $T$ 中的一个未知变量,那么 $S$ 的结构就必然会限制 $X$ 可能的形态。
我们的算法,正是要将这种隐含的、结构上的限制,转化为一组显式的、关于 $X$ 上下界的断言。 然而,在系统性地提取这些约束之前,我们必须首先面对一个与变量作用域相关的、
虽属前期准备但至关重要的挑战。若不妥善处理,我们生成的约束本身就可能是非良构的。
这一挑战,催生了算法的第一个具体操作步骤:变量消去。 设想我们想为变量 $X$ 生成约束,以使得类型 $\forall Y. () \to (Y\to Y)$ 成为 $\forall Y. () \to X$ 的一个子类型。根据函数子类型的逆变/协变规则,这要求 $Y \to Y \lt: X$。然而,我们不能直接生成约束 $\{ Y \to Y \lt: X \lt: \top\}$,因为类型变量 $Y$ 在此约束中是自由的,但它本应被 $\forall Y$ 所绑定,这就造成了一种作用域错误。 正确的做法是,找到 $Y \to Y$ 的一个不含 $Y$ 的、且尽可能精确的超类型,并用它来约束 $X$。在本例中,即 $\bot \to \top$。变量消去机制,正是为了形式化地完成这一「寻找最精确边界」的任务。 这两套关系由一组递归的定则所定义,确保了对于任何类型 $S$ 和变量集 $V$,其结果 $T$ 都是唯一且总能被计算出来的(即它们是全函数)。
此处建议读者停下来思考一下,如何设计这两套关系的递归规则并自己使用代码实现它(提示:对于提升规则的情况,若 $X\in V$ 则将其提升到 $\top$,反之不变,其他情况是显然的) 提升规则 ($S \Uparrow^V T$) 下降规则 ($S \Downarrow^V T$) 这可以非常直接地在 MoonBit 中实现: 这套精心设计的规则,保证了变量消去操作的正确性与最优性,这由两个关键引理所保证: 约束生成是局部类型参数合成算法的核心引擎。
在通过变量消去确保了作用域安全之后,
此步骤的使命是将一个子类型判定问题——例如,
$S \lt: T$,其中 $S$ 或 $T$ 中含有待定的类型参数 $\overline{X}$ 转化为一组对这些未知参数 $\overline{X}$ 的显式约束。
现在我们形式化地定义代码中的约束具体是什么结构: 约束 (Constraint):在本系统中,每一个约束都具有形式 $S_i \lt: X_i \lt: T_i$,它为单个未知类型变量 $X_i$ 同时指定了一个下界 (lower bound) $S_i$ 和一个上界 (upper bound) $T_i$ 。 约束集 (Constraint Set):一个约束集 $C$ 是关于一组未知变量 $\overline{X}$ 到其对应约束的有限映射(在代码中可以实现为一个 Hash Map)。约束集的一个关键不变量是,其中任何约束的上下界($S_i, T_i$)都不能含有任何待定的未知变量(即 $\overline{X}$ 中的变量)或任何需要被消去的局部变量(即 $V$ 中的变量)。空约束集 ($\emptyset$) 代表最无限制的约束,相当于为每一个 $X_i$ 指定了约束 $\bot \lt: X_i \lt: \top$ 。 约束集的交 ($\wedge$) 定义为两个约束集 $C$ 和 $D$ 的交集,是通过将其对同一个变量的约束进行合并得到的。新的下界是原下界的最小上界(join, $\vee$),而新的上界是原上界的最大下界(meet, $\wedge$) 。 约束生成过程被形式化为一个推导关系 $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$,其意为:在需要回避的变量集为 $V$ 的条件下,为使 $S \lt: T$ 成立,关于未知变量 $\overline{X}$ 需满足的(最弱)约束集是 $C$,这个 $C$ 可以被视为是该推导关系的输出。 算法由一组递归规则定义,其中关键规则如下(注:我们始终假定 $\overline{X} \cap V = \emptyset$): 一个至关重要的观察是,在任何一次调用 $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$ 时,未知变量 $\overline{X}$ 都只会出现在 $S$ 和 $T$ 的其中一边。这使得整个过程是一个匹配模子类型(matching-modulo-subtyping)问题,而非一个完全的合一(unification)问题,从而保证了算法的简洁性与确定性。 通过前述的约束生成步骤,我们已经成功地将一个非构造性的最优解搜索问题,
转化为了一个具体、有形的产物:一个约束集 $C$。
这个约束集,凝聚了为了使整个多态应用类型正确,所有待定类型参数 $\overline{X}$ 必须满足的全部边界条件。
对于每一个未知变量 $X_i$,我们都得到了一个形如 $S_i \lt: X_i \lt: T_i$ 的合法区间。 至此,算法的第一阶段「我们对未知数了解了什么?」已经圆满完成。
然而,我们的工作尚未结束。一个约束区间,例如 $\mathbb{Z} \lt: X \lt: \mathbb{R}$,
本身可能允许多个合法的解(如 $\mathbb{Z}$ 或 $\mathbb{R}$)。
我们最终必须为每一个 $X_i$ 挑选出一个具体的类型值,以完成对内核语言项的最终构造。 这就引出了算法的最后一个,也是画龙点睛的一步:我们应依据何种准则,从每个变量的合法区间中做出最终的选择?
答案,必须回归到我们的初衷,即 App-InfSpec 规约中所声明的最优性要求:
我们所做的选择,必须能使整个应用表达式获得唯一的、最小的结果类型。
因此,算法的最后一步,便是要设计一个选择策略,
它能利用我们已经辛勤收集到的约束集 $C$,
并结合函数原始的返回类型 $R$,
来计算出一组能最终最小化 $R$ 的具体类型参数。
这便是本节「参数计算」的核心任务。 为了计算关于 $R$ 的具体类型参数,还有一个至关重要的操作:变量代换导致的极性变化。
一个类型变量 $X$ 在另一个类型表达式 $R$ 中的极性,描述了当该变量的类型变大或变小时,整个表达式的类型会如何相应地变化。 现在我们对极性的考虑主要集中在函数类型之上,
只需要关注变量在函数类型中的位置即可(在箭头的左边还是右边),
当然,需要考虑到嵌套的函数结构。建议读者在此稍作停顿,考虑一下该算法的设计。
当然你也可以直接展开下面的代码块来查看具体实现。 为了最小化返回类型 $R$,我们的选择策略变得显而易见: 上述策略被形式化为一个计算最小代换(minimal substitution) $\sigma_{CR}$ 的算法。给定一个可满足的约束集 $C$ 和返回类型 $R$: 对于 $C$ 中的每一个约束 $S \lt: X_i \lt: T$: 当 $\sigma_{CR}$ 未定义时,算法宣告失败,这精确地对应了 至此,我们已经完整地定义了一个由「变量消去」、「约束生成」和「参数计算」三步构成的、完全可执行的算法。但我们如何确保这个具体的算法,其行为与那个非构造性的、声明式的 其等价性的证明,浓缩于一个核心命题中,该命题断言: 证明概要: 第一部分(算法的正确性):
为证明 $\sigma_{CR}$ 是最优的,我们任取另一个满足约束的合法代换 $\sigma'$,并需要证明 $\sigma_{CR}(R) \lt: \sigma'(R)$。
考虑构建一个从 $\sigma_{CR}$ 到 $\sigma'$ 的「代换链」,每一步只改变一个变量的值。例如,$\sigma_0 = \sigma_{CR}$,$\sigma_1 = \sigma_0[X_1 \mapsto \sigma'(X_1)]$,…,$\sigma_n = \sigma'$。
接着,我们证明在此路径的每一步中,结果类型都是单调不减的,即 $\sigma_{i-1}(R) \lt: \sigma_i(R)$。这一步的证明,直接依赖于前述的极性定义。例如,若 $R$ 在 $X_i$ 上是协变的,我们的算法选择了下界 $S$,而 $\sigma'(X_i)$ 必然大于等于 $S$,因此根据协变的定义,结果类型必然「变大」。同理可以证明其他情况下该论断也成立。
最终,通过传递性,我们得出 $\sigma_{CR}(R) \lt: \sigma'(R)$,证明了 $\sigma_{CR}$ 的最优性。 第二部分(算法失败的完备性):
当算法失败时,必然是因为某个不变变量 $X_i$ 的约束区间 $[S, T]$ 中 $S \neq T$。
我们采用反证法:假设此时仍然存在一个最优解 $\sigma$。由于 $S \neq T$,我们总能找到另一个合法的代换 $\sigma'$,使得 $\sigma(X_i)$ 与 $\sigma'(X_i)$ 不同。但由于 $R$ 在 $X_i$ 上是不变的,$\sigma(R)$ 与 $\sigma'(R)$ 将变得不可比较,这与「$\sigma$ 是最优解(即比所有其他解都小)」的假设相矛盾。
因此,在这种情况下,最优解必然不存在。 这一核心命题证明了我们设计的这套具体算法与 $$
\frac{
\begin{array}{ccc}
\Gamma \vdash f : \forall \overline{X}.\overline{T} \to R & \Gamma \vdash \overline{e} : \overline{S} & |\overline{X}| > 0 \\
\emptyset \vdash_X \overline{S} \lt: \overline{T} \Rightarrow \overline{D} & C = \bigwedge \overline{D} & \sigma = \sigma_{CR}
\end{array}
}{
\Gamma \vdash f(\overline{e}) : \sigma R
}
\quad (\text{App-InfAlg})
$$ 至此,我们已经完整地剖析了本文的第一项重点:局部类型参数合成。它通过一套由「变量消去」、「约束生成」和「参数计算」构成的、逻辑严密且完全可执行的算法,完美地解决了由细粒度多命题所引发的类型参数标注繁琐的问题,达成了引言中所述三条设计准则中的第一条。 然而,我们的工具箱尚不完备。回顾引言中基于 ML 代码分析所提出的三条设计准则,仍有两项亟待解决: 局部类型参数合成机制,其信息流本质上是自下而上(bottom-up)的,它根据函数和参数的既有类型,向上推导出一个最佳的结果类型。这套机制,对于上述两个问题鞭长莫及,因为在类似 我们考虑一种在思想上与前者互补的、功能强大的局部推断技术。它不再仅仅依赖自下而上的信息综合,而是引入了一股自上而下(top-down)的信息流,让表达式所处的语境(context)来指导其内部的类型检查。这便是双向类型检查(Bidirectional Type Checking),其基本思想虽早已是编程语言社区的「民间共识」,并在一些基于属性文法的 ML 编译器中得以应用,本文将其在一个同时包含子类型化与非直谓多态的形式系统中进行严谨的公理化,并将其作为一种独立的局部推断方法,其威力出人意料地强大。 综合模式 (Synthesis Mode, $\Rightarrow$) 检查模式 (Checking Mode, $\Leftarrow$) 双向检查的精髓在于两种模式的灵活切换。一个典型的函数应用 本节是我们类型检查程序的最后一块拼图,
描述了整个双向类型检查的过程。 1. 综合 - 变量 (Synthesis-Var) $$
\frac{}{\Gamma \vdash x \Rightarrow \Gamma(x)} \quad (\text{S-Var})
$$ 这是变量的综合规则。如果要在综合模式下推导一个变量 $x$ 的类型,只需在当前的类型上下文 $\Gamma$ 中查找 $x$ 已经声明的类型 $\Gamma(x)$ 即可。这是最直接的类型推导形式:变量的类型就是它被定义时的类型。 2. 检查 - 变量 (Checking-Var) $$
\frac{\Gamma \vdash \Gamma(x) \lt: T}{\Gamma \vdash x \Leftarrow T} \quad (\text{C-Var})
$$ 这是变量的检查规则。要检查变量 $x$ 是否符合预期的类型 $T$,我们需要先从上下文 $\Gamma$ 中查找到 $x$ 的实际类型 $\Gamma(x)$,然后验证这个实际类型 $\Gamma(x)$ 是否是预期类型 $T$ 的一个子类型 (subtype)。这里的子类型关系用 $\Gamma \vdash \Gamma(x) \lt: T$ 表示。 3. 综合 - 抽象 (Synthesis-Abs) $$
\frac{\Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Rightarrow T}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}:\overline{S}) e \Rightarrow \forall \overline{X}. \overline{S} \rightarrow T} \quad (\text{S-Abs})
$$ 这是针对带有完整类型标注的函数抽象的综合规则。 4. 检查 - 无标注抽象 (Checking-Abs-Inf) $$
\frac{\Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Leftarrow T}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}) e \Leftarrow \forall \overline{X}. \overline{S} \rightarrow T} \quad (\text{C-Abs-Inf})
$$ 这是本节的核心规则之一,用于推断无标注匿名函数的参数类型。 5. 检查 - 有标注抽象 (Checking-Abs) $$
\frac{\Gamma, \overline{X} \vdash \overline{T} \lt: \overline{S} \quad \Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Leftarrow R}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}:\overline{S}) e \Leftarrow \forall \overline{X}. \overline{T} \rightarrow R} \quad (\text{C-Abs})
$$ 这是在检查模式下处理一个带有类型标注的函数的规则。 6. 综合 - 应用 (Synthesis-App) $$
\frac{\Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{S} \rightarrow R \quad \Gamma \vdash \overline{e} \Leftarrow [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Rightarrow [\overline{T}/\overline{X}]R} \quad (\text{S-App})
$$ 这是函数应用的综合规则。 7. 检查 - 应用 (Checking-App) $$
\frac{\Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{S} \rightarrow R \quad \Gamma \vdash [\overline{T}/\overline{X}]R \lt: U \quad \Gamma \vdash \overline{e} \Leftarrow [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Leftarrow U} \quad (\text{C-App})
$$ 这是函数应用的检查规则。它与综合规则非常相似,但增加了一个最终的子类型检查。 8. 综合 - 应用 - 推断规格 (Synthesis-App-InfAlg) $$
\frac{
\begin{array}{ccc}
\Gamma \vdash f : \forall \overline{X}.\overline{T} \to R & \Gamma \vdash \overline{e} : \overline{S} & |\overline{X}| > 0 \\
\emptyset \vdash_X \overline{S} \lt: \overline{T} \Rightarrow \overline{D} & C = \bigwedge \overline{D} & \sigma = \sigma_{CR}
\end{array}
}{
\Gamma \vdash f(\overline{e}) \Rightarrow \sigma R
}
\quad (\text{S-App-InfAlg})
$$ 这是在综合模式下推断函数应用中缺失的类型参数的规则,这正是上文「类型参数计算」一节导出的规则。 9. 检查 - 应用 - 推断规格 (Checking-App-InfAlg) $$
\frac{\begin{matrix} \Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{T} \rightarrow R \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S} \quad |\overline{X}| \gt 0 \\ \emptyset \vdash \overline{S} \lt: \overline{T} \Rightarrow C \quad \emptyset \vdash R \lt: V \Rightarrow D \quad \sigma \in \bigwedge C \wedge D \end{matrix}}{\Gamma \vdash f(\overline{e}) \Leftarrow V} \quad (\text{C-App-InfAlg})
$$ 这是 10. 检查 - 顶类型 (Checking-Top) $$
\frac{\Gamma \vdash e \Rightarrow T}{\Gamma \vdash e \Leftarrow \top} \quad (\text{C-Top})
$$ 这是一个从检查模式切换到综合模式的规则。如果一个表达式 $e$ 被要求检查是否符合顶类型 $\top$,由于任何类型都是 $\top$ 的子类型,这个检查总是会成功。$\top$ 类型没有提供任何有用的约束信息,所以规则允许我们直接切换到综合模式,推导出 $e$ 的具体类型 $T$ 即可。 11. 综合 - 应用 - 底类型 (Synthesis-App-Bot) $$
\frac{\Gamma \vdash f \Rightarrow \bot \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Rightarrow \bot} \quad (\text{S-App-Bot})
$$ 这是处理函数类型为 $\bot$ (底类型) 时的特殊情况。$\bot$ 类型代表那些永不返回的表达式(如抛出异常)。 12. 检查 - 应用 - 底类型 (Checking-App-Bot) $$
\frac{\Gamma \vdash f \Rightarrow \bot \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Leftarrow R} \quad (\text{C-App-Bot})
$$ 这是在检查模式下,函数类型为 $\bot$ 的情况。 最后的实现即是落到 最后一个关键目标是局部变量绑定的设计,
这要求我们引入新的语法结构 $$
\frac{\Gamma \vdash e \Rightarrow S \quad \Gamma, x:S \vdash b \Rightarrow T}{\Gamma \vdash \textbf{let } x = e \textbf{ in } b \Rightarrow T} \quad (\text{S-Let})
$$ $$
\frac{\Gamma \vdash e \Rightarrow S \quad \Gamma, x:S \vdash b \Leftarrow T}{\Gamma \vdash \textbf{let } x = e \textbf{ in } b \Leftarrow T} \quad (\text{C-Let})
$$ 实现留作习题。 至此,我们循着 Pierce 与 Turner 的足迹,完整地剖析了一套精巧而强大的局部类型推断机制。
通过将局部类型参数合成与双向类型检查这两项核心技术相结合,
我们最终完成了一个真正强大的类型检查器的设计。
它不仅能在理论上驾驭如 System $F_{\le}$ 这样兼具子类型化与非直谓多态的强大类型系统,
更在实践中,精准地解决了由多态、
高阶编程与纯函数式风格所引发的最为普遍和恼人的类型标注问题。
这套完全基于「局部性」原则的算法,其行为可预测、
易于实现且错误提示友好,堪称是连接艰深理论与日常编程实践的一座典范之桥。 当然,本文所探讨的,仅是这篇经典论文的核心部分。原文的疆域更为广阔,
其中最重要的扩展,便是对有界量化(Bounded Quantification)的支持。
有界量化,即形如 $\forall (X \lt: T_2, Y \lt: T_2, \cdots) . e$ 的多态,
它允许类型参数本身受到其超类型的约束。这一特性对于精确建模面向对象语言中的继承等高级特性至关重要,是通往更强大表达能力的必由之路。
原文第五章详细阐述了如何将本文介绍的局部推断技术扩展至支持有界量化的系统。该扩展使得算法,尤其是约束的生成与求解,将变得更为精妙和复杂,
特别是在处理 $\bot$ 类型与类型边界的相互作用时,
引入了新的挑战。限于篇幅,对这一部分的深入剖析,或许只能留待未来的文章再行探讨。
此外,本文的另一大遗憾是「形式证明」的缺失。我们关注的重点,在于阐明算法的设计动机与直觉,
并以一种接近实际代码实现的方式来呈现其逻辑。为此,我们省略了诸多严谨的数学证明细节,
例如约束生成算法的可靠性与完备性证明,仅以提要的形式一笔带过。 最后,值得一提的是,本文对类型系统代数性质的倚重——例如,确保任意类型间的最小上界(join)与最大下界(meet)总是存在——揭示了一条深刻的设计原则:一个具有良好代数结构的类型系统,往往更能催生出简洁而强大的类型推断算法。自这篇论文发表以来,寻求更优美的子类型化代数理论的探索从未停止。后续的研究,如 Stephen Dolan 等人提出的「代数子类型」(Algebraic Subtyping),
正是沿着这一思想路径,对子类型关系的形式化进行了更为深刻的抽象与简化,
在笔者看来,它是真正改变子类型研究的天才之作。
当然,对这些更前沿工作的介绍,已然超出了对这篇 2000 年经典论文本身进行解读的范畴,
我们把它留给未来的文章。 4. Blog [blog]
Blog 4.1. MoonBit 实现树的先序遍历 [blog/iterator/preorder-traversal]
priv enum Tree[A] {
Nil
Node(A, Tree[A], Tree[A])
}
fn[A] Tree::preorder(self : Tree[A], f : (A) -> Unit) -> Unit {
fn dfs(root) {
match root {
Nil => ()
Node(x, left, right) => {
f(x)
dfs(left)
dfs(right)
}
}
}
dfs(self)
}
Tree::preorder
改写为手动控制栈的过程 Tree::preorder_stack
fn[A] Tree::preorder_stack(self : Tree[A], f : (A) -> Unit) -> Unit {
let stack = Array::new(capacity=4096)
stack.push(self)
while not(stack.is_empty()) {
let root = stack.unsafe_pop()
match root {
Nil => ()
Node(x, left, right) => {
f(x)
stack.push(right) // 先进后出, 先被压入后处理
stack.push(left) // 先处理左节点
}
}
}
}
fn Tree::from_n(n : Int) -> Tree[Int] {
let mut i = 0
fn dfs() {
if i < n {
let x = i
i += 1
let res = Node(x, dfs(), dfs())
res
} else {
Nil
}
}
dfs()
}
fn test_preorder(root : Tree[Int]) -> Unit raise {
let b1 = StringBuilder::new()
let b2 = StringBuilder::new()
root.preorder(fn(x) { b1.write_object(x) })
root.preorder_stack(fn(x) { b2.write_object(x) })
assert_eq(b1.to_string(), b2.to_string())
}
test "preorder/preorder_stack" {
let t1 = Node(
1,
Node(2, Nil, Nil),
Node(3, Node(4, Nil, Nil), Node(5, Nil, Nil)),
)
let mut sum = 0
t1.preorder(fn(x) { sum += x })
inspect(sum, content="15")
let t2 = Tree::from_n(15)
test_preorder(t2)
}
Blog 4.2. MoonBit 实现外部迭代器 [blog/iterator/external]
4.2.1. 内部迭代器和外部迭代器 [blog/iterator/internal-vs-external]
Iter[A]
是内部迭代器,
没有办法把iter
切分为(first : A?)
和 (rest : Iter[A])
。fn uncons[A](xs : Iter[A]) -> (A, Iter[A])?
这样的接口。fn next[A](self : Iter[A]) -> A?
这样的接口。test "split internal iterator" {
let xs = [1,2,3,4,5]
let iter = xs.iter().drop(4)
// 这里的 drop 只是修饰器,改变迭代的行为
inspect!(xs.iter().last(), content="Some(5)")
// 但是迭代过程还是 xs.iter()
inspect!(iter.head(), content="Some(5)")
// xs.iter().last() 仍然需要迭代5次
}
uncons
。next
。 4.2.2. 不可变外部迭代器和可变外部迭代器 [blog/iterator/immut-vs-mut]
uncons
, 但是迭代每个元素的过程仍是可分割的。next
方法后,可变外部迭代器的内部状态改变,变成剩余的迭代了。 4.2.3. 可变外部迭代器 [blog/iterator/mut-exiter]
priv type ExIter[A] () -> A?
fn ExIter::next[A](self : ExIter[A]) -> A? {
(self._)()
}
fn ExIter::from_array[A](xs : Array[A]) -> ExIter[A] {
let mut i = 0 // i 是内部可变状态
fn() {
if i < xs.length() {
let res = xs[i]
i = i + 1
Some(res)
} else {
None
}
}
}
test {
let xs = [1, 2, 3, 4, 5]
let iter = ExIter::from_array(xs)
let mut sum = 0
loop iter.next() {
None => ()
Some(x) => {
sum += x
continue iter.next()
}
}
inspect!(sum, content="15")
}
ExIter::from_tree
是从 Tree::Tree::preorder_stack
改编而来,
loop
变成 if
迭代过程可以切分,而不是一个整体。each
和eachi
这样的内部迭代器的方法,只能一下子迭代全部元素读者可以再一次看外部迭代器的性质 [blog/iterator/internal-vs-external]
Iter[A]
是内部迭代器,
没有办法把iter
切分为(first : A?)
和 (rest : Iter[A])
。fn uncons[A](xs : Iter[A]) -> (A, Iter[A])?
这样的接口。fn next[A](self : Iter[A]) -> A?
这样的接口。test "split internal iterator" {
let xs = [1,2,3,4,5]
let iter = xs.iter().drop(4)
// 这里的 drop 只是修饰器,改变迭代的行为
inspect!(xs.iter().last(), content="Some(5)")
// 但是迭代过程还是 xs.iter()
inspect!(iter.head(), content="Some(5)")
// xs.iter().last() 仍然需要迭代5次
}
uncons
。next
。fn ExIter::from_tree[A](root : Tree[A]) -> ExIter[A] {
let stack = Array::new(capacity=4096) // stack 是内部可变状态
stack.push(root)
fn() {
if not(stack.is_empty()) {
let root = stack.unsafe_pop()
match root {
Nil => None
Node(x, left, right) => {
stack.push(right)
stack.push(left)
Some(x)
}
}
} else {
None
}
}
}
zipWith
来同时迭代两个迭代器,
但是和不可变迭代器比,ExIter
只能迭代一次,迭代后就使用完所有的元素。
这个和文件流的概念很相似。fn ExIter::zipWith[A,B,C](self : ExIter[A], other : ExIter[B], f : (A,B) -> C) -> ExIter[C] {
let xs = self
let ys = other
fn () {
match (xs.next(),ys.next() ) {
(Some(x),Some(y)) => {
Some(f(x,y))
}
(_,_) => None
}
}
}
test "ExIter::zipWith" {
let xs = ["apple", "orange", "watermetlon"]
let ys = Tree::from_n(5)
let xs = ExIter::from_array(xs)
let ys = ExIter::from_tree(ys)
let zs = xs.zipWith(ys,fn (x,y) { (x,y)})
let b1 = StringBuilder::new()
loop zs.next() {
None => ()
Some(x) => {
b1.write_string("\{x},")
continue zs.next()
}
}
inspect!(b1, content=
#|("apple", 0),("orange", 1),("watermetlon", 2),
)
}
test "ExIter::from_tree" {
let t2 = Tree::from_n(15)
let iter = ExIter::from_tree(t2)
let b1 = StringBuilder::new()
loop iter.next() {
None => ()
Some(x) => {
b1.write_string("\{x},")
continue iter.next()
}
}
inspect!(b1, content="0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,")
let b2 = StringBuilder::new()
t2.preorder(fn(x) { b2.write_string("\{x},") })
inspect!(b2, content="0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,")
}
4.2.4. 不可变外部迭代器 [blog/iterator/immut-exiter]
priv type ImmutExIter[A] () -> (A,ImmutExIter[A])?
fn ImmutExIter::uncons[A](self : ImmutExIter[A]) -> (A,ImmutExIter[A])? {
(self._)()
}
Array[A]
构造不可变外部迭代器fn ImmutExIter::from_array[A](xs : Array[A]) -> ImmutExIter[A] {
fn aux(i) -> (A,ImmutExIter[A])? {
if (i < xs.length()) {
Some((xs[i],fn () { aux(i + 1) } ) )
} else {
None
}
}
fn () {
aux(0)
}
}
test "ImmutExIter::from_array" {
let xs = [1,2,3,4,5]
let iter = ImmutExIter::from_array(xs)
let buf = StringBuilder::new()
loop iter.uncons() {
None => ()
Some((x,xs)) => {
buf.write_object(x)
continue xs.uncons()
}
}
inspect!(buf, content="12345")
}
4.2.4.1. 实现树的不可变外部迭代器 [blog/iterator/immut-exiter-tree]
Blog 4.2.4.1.1. 前置知识 [blog/iterator/preorder-traversal]
priv enum Tree[A] {
Nil
Node(A, Tree[A], Tree[A])
}
fn[A] Tree::preorder(self : Tree[A], f : (A) -> Unit) -> Unit {
fn dfs(root) {
match root {
Nil => ()
Node(x, left, right) => {
f(x)
dfs(left)
dfs(right)
}
}
}
dfs(self)
}
Tree::preorder
改写为手动控制栈的过程 Tree::preorder_stack
fn[A] Tree::preorder_stack(self : Tree[A], f : (A) -> Unit) -> Unit {
let stack = Array::new(capacity=4096)
stack.push(self)
while not(stack.is_empty()) {
let root = stack.unsafe_pop()
match root {
Nil => ()
Node(x, left, right) => {
f(x)
stack.push(right) // 先进后出, 先被压入后处理
stack.push(left) // 先处理左节点
}
}
}
}
fn Tree::from_n(n : Int) -> Tree[Int] {
let mut i = 0
fn dfs() {
if i < n {
let x = i
i += 1
let res = Node(x, dfs(), dfs())
res
} else {
Nil
}
}
dfs()
}
fn test_preorder(root : Tree[Int]) -> Unit raise {
let b1 = StringBuilder::new()
let b2 = StringBuilder::new()
root.preorder(fn(x) { b1.write_object(x) })
root.preorder_stack(fn(x) { b2.write_object(x) })
assert_eq(b1.to_string(), b2.to_string())
}
test "preorder/preorder_stack" {
let t1 = Node(
1,
Node(2, Nil, Nil),
Node(3, Node(4, Nil, Nil), Node(5, Nil, Nil)),
)
let mut sum = 0
t1.preorder(fn(x) { sum += x })
inspect(sum, content="15")
let t2 = Tree::from_n(15)
test_preorder(t2)
}
4.2.4.1.2. 正文 [blog/iterator/immut-exiter-tree-content]
ImmutExIter[A]
需要保存整个迭代上下文,
typealias Stack[A] = @immut/list.T[A]
fn ImmutExIter::from_tree[A](root : Tree[A]) -> ImmutExIter[A] {
fn aux(stack : Stack[_]) -> (A,ImmutExIter[A])? {
match stack {
Nil => None
Cons(root,rest_stack) => { // pop root from stack
match root {
Nil => None
Node(x,left,right) => {
let stack = Stack::Cons(left,Stack::Cons(right,rest_stack))
// push right into stack
// push left into stack
Some((x,fn () { aux(stack)}))
}
}
}
}
}
fn () {
aux(@immut/list.singleton(root))
}
}
test "ImmutExIter::from_tree" {
let t2 = Tree::from_n(15)
let iter = ImmutExIter::from_tree(t2)
let b1 = StringBuilder::new()
loop iter.uncons() {
None => ()
Some((x,rest)) => {
b1.write_string("\{x},")
continue rest.uncons()
}
}
inspect!(b1, content="0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,")
let b2 = StringBuilder::new()
t2.preorder(fn(x) { b2.write_string("\{x},") })
inspect!(b2, content="0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,")
}
zipWith
,这里和普通的List[A]
的 zipWith
别无二致fn ImmutExIter::zipWith[A,B,C](self : ImmutExIter[A], other : ImmutExIter[B], f : (A,B) -> C) -> ImmutExIter[C] {
let xs = self
let ys = other
match (xs.uncons(),ys.uncons()) {
(Some((x,xs)),Some((y,ys))) => {
fn () { Some((f(x,y), ImmutExIter::zipWith(xs,ys,f)))}
}
(_,_) => {
fn () { None }
}
}
}
test {
let xs = ["apple", "orange", "watermetlon"]
let ys = Tree::from_n(5)
let xs = ImmutExIter::from_array(xs)
let ys = ImmutExIter::from_tree(ys)
let zs = xs.zipWith(ys,fn (x,y) { (x,y)})
let b1 = StringBuilder::new()
loop zs.uncons() {
None => ()
Some((x,rest)) => {
b1.write_string("\{x},")
continue rest.uncons()
}
}
inspect!(b1, content=
#|("apple", 0),("orange", 1),("watermetlon", 2),
)
}
Blog 4.3. MoonBit 实现内部迭代器 [blog/iterator/internal]
priv type InIter[A] ((A) -> Unit) -> Unit
fn InIter::run[A](self : InIter[A], f : (A) -> Unit) -> Unit {
(self._)(f)
}
InIter::from_array
相当于 OCaml
的柯里化。fn InIter::from_array[A](xs : Array[A]) -> InIter[A] {
fn(k) { xs.each(k) }
}
with_index
是装饰器,装饰 iter
默认的行为。fn InIter::with_index[A](self : InIter[A]) -> InIter[(Int, A)] {
let mut i = 0
fn(k) {
self.run(fn(x) {
k((i, x))
i += 1
})
}
}
impl[A : Show] Show for InIter[A] with output(self, logger) {
logger.write_string("[")
self.run(fn(x) {
logger.write_object(x)
logger.write_string(",")
})
logger.write_string("]")
}
test {
let xs = ["apple", "orange", "strawberry"]
let iter = InIter::from_array(xs).with_index()
inspect!(iter.to_string(), content=#|[(0, "apple"),(1, "orange"),(2, "strawberry"),]
)
}
IterResult
.yield : (A) -> IterResult
这个回调函数可以控制循环是停止还是继续。type InIter[A] ((A) -> Unit) -> Unit
type Iter[A] ((A) -> IterResult) -> IterResult
Iter[A]
和 InIter[A]
的定义,Unit
替换成 IterResult
之后,就和 MoonBit 内建的内部迭代器定义一样了
InIter[A]
返回 Unit
和 回调函数返回 Unit
, 相当于一直返回 IterResult::IterContinue
。Iter::take
, Iter::drop
, Iter::flat_map
… 这些方法都是装饰器,用来修饰原先 iter
的行为。core
的 Iter::take
的实现,
这个 Iter::take
可以用来解释, yield_
如何控制循环的状态。// ref: https://github.com/moonbitlang/core/blob/main/builtin/iter.mbt
pub fn Iter::take[T](self : Iter[T], n : Int) -> Iter[T] {
// [..take(10,seq), next] would continue
// even if seq has less than 10 elements
// but `for x in [..take(10,seq), next ] { break }` would stop
//
fn(yield_) {
let mut i = 0
let mut r = IterContinue
self.just_run(fn {
a =>
if i < n {
if yield_(a) == IterContinue {
// yield_ 这个回调函数,有循环的控制权
i = i + 1
IterContinue
} else {
r = IterEnd
IterEnd // 这里 yield 让整个循环退出了
}
} else {
IterEnd // i < n, 停止循环
}
})
r
}
}
Iter::drop
的实现,可以解释为什么内部迭代器是不可分割的。// ref: https://github.com/moonbitlang/core/blob/main/builtin/iter.mbt
pub fn Iter::drop[T](self : Iter[T], n : Int) -> Iter[T] {
fn(yield_) {
let mut i = 0
self.run(fn(a) {
if i < n {
i = i + 1
IterContinue
// 这里跳过 n 个元素, 但是这个 Iter::drop 只是装饰器,
// 让 self 这个迭代器,不对前 n 个元素,调用 yield_ 而已
// 即使drop 之后,i 仍然会递增 n
} else {
yield_(a)
}
})
}
}
test "split internal iterator" {
let xs = [1,2,3,4,5]
let iter = xs.iter().drop(4)
// 这里的 drop 只是修饰器,改变迭代的行为
inspect!(xs.iter().last(), content="Some(5)")
// 但是迭代过程还是 xs.iter()
inspect!(iter.head(), content="Some(5)")
// xs.iter().last() 仍然需要迭代 5 次
// 上面的源码解析,解释了为什么仍然需要迭代 5 次
}
Iter::drop
之后,还需要递增内部状态的 i
, 所以说内部迭代器是不可分割的 4.3.1. 内部迭代器和外部迭代器 [blog/iterator/internal-vs-external]
Iter[A]
是内部迭代器,
没有办法把iter
切分为(first : A?)
和 (rest : Iter[A])
。fn uncons[A](xs : Iter[A]) -> (A, Iter[A])?
这样的接口。fn next[A](self : Iter[A]) -> A?
这样的接口。test "split internal iterator" {
let xs = [1,2,3,4,5]
let iter = xs.iter().drop(4)
// 这里的 drop 只是修饰器,改变迭代的行为
inspect!(xs.iter().last(), content="Some(5)")
// 但是迭代过程还是 xs.iter()
inspect!(iter.head(), content="Some(5)")
// xs.iter().last() 仍然需要迭代5次
}
uncons
。next
。Blog 4.4. Derive Iteration from Recursion [blog/defunctionalize]
for
、while
) 逐步更新状态,直接控制计算流程。然揆诸实现,则各具长短:
4.4.1. Defunctionalization: A Taste on Filter DSL [blog/defunctionalize/filter]
filter
函数,该函数接收列表与谓词函数作为输入,返回满足谓词条件的所有元素构成的新列表。
采用递归策略可达成如下实现:fn[T] filter(xs : List[T], pred : (T) -> Bool) -> List[T] {
match xs {
Nil => Nil
Cons(x, xs) if pred(x) => Cons(x, filter(xs, pred))
Cons(_, xs) => filter(xs, pred)
}
}
pred
作为高阶函数的特性引发了一个本质性问题:在底层编译场景中 (如将 MoonBit 编译至 C 语言时),函数无法以常规数据结构的形式进行存储与传递。换言之,在目标语言层面,一等函数的直接表示存在根本性限制。enum Filter {
IsEven
IsOdd
IsPositive
IsNegative
}
fn run(self : Filter, data : Int) -> Bool {
match self {
IsEven => data % 2 == 0
IsOdd => data % 2 != 0
IsPositive => data > 0
IsNegative => data < 0
}
}
fn filter_defunct(xs : List[Int], pred : Filter) -> List[Int] {
match xs {
Nil => Nil
Cons(x, xs) if pred.run(x) => Cons(x, filter_defunct(xs, pred))
Cons(_, xs) => filter_defunct(xs, pred)
}
}
IsNegative
推广为带参数的 IsLessThan
:enum FilterExtend {
//...
IsLessThan(Int)
}
fn run_extend(self : FilterExtend, data : Int) -> Bool {
match self {
IsLessThan(n) => data < n
//...
}
}
And
等逻辑连接词,可实现谓词函数的组合运算:enum FilterExtendCompose {
//...
And(FilterExtend, FilterExtend)
}
fn run_extend_compose(self : FilterExtendCompose, data : Int) -> Bool {
match self {
And(f1, f2) => f1.run_extend(data) && f2.run_extend(data)
//...
}
}
Filter
类型本质上已演变为一种领域特定语言 (Domain-Specific Language)。
建议感兴趣的读者可进一步探索其 Parser 与 Pretty Printer 的实现路径,以完善该 DSL 的序列化能力。run
函数)。
这与高阶函数与生俱来的开放性形成鲜明对比:后者允许在不修改现有代码的前提下自由扩展新函数。 4.4.2. Traverse a Tree [blog/defunctionalize/tree]
enum Tree[T] {
Leaf(T)
Node(T, Tree[T], Tree[T])
}
fn[T] pre_order(tree : Tree[T], f : (T) -> Unit) -> Unit {
match tree {
Leaf(x) => f(x)
Node(x, left, right) => {
f(x)
pre_order(left, f)
pre_order(right, f)
}
}
}
f
的精确,
且严格遵循前序遍历(pre-order traversal)的既定顺序,但其递归范式存在显著的效率瓶颈。
具体而言,由于该递归过程并非尾递归(tail recursion)的优化形态,
导致现代编译器的尾调用优化(TCO)机制无法将其自动转换为等价的迭代形式,
这种特性必然造成调用栈的持续累积,进而影响程序的执行效能。
有鉴于此,我们亟需运用前文阐述的「去函数化」(defunctionalization)这一程序变换技术来突破此局限。 4.4.3. Continuation-Passing Style Transformation [blog/defunctionalize/cps]
pre_order(left, f)
调用执行时,
其延续正是 fn (_) { pre_order(right, f) }
表征的右子树遍历过程。
我们通过扩展函数签名引入延续参数,重构后的实现显式地将计算结果注入到延续中:fn[T] pre_order_cps(self : Tree[T], f : (T) -> Unit) -> Unit {
fn go(t, g) {
match (t, g) {
(Leaf(x), k) => k(f(x))
(Node(x, left, right), k) => {
f(x)
go(left, _ => go(right, k))
}
}
}
go(self, x => x)
}
go(tree, cont)
与恒等函数 fn { x => x }
,我们将其编码为代数数据类型:enum TreeCont[T] {
Return
Next(Tree[T], TreeCont[T])
}
run_cont
实现之:fn[T] pre_order_cps_defunct(self : Tree[T], f : (T) -> Unit) -> Unit {
letrec run_cont = fn(k) {
match k {
Next(tree, k) => go(tree, k)
Return => ()
}
}
and go = fn(t, g) {
match (t, g) {
(Leaf(x), k) => {
f(x)
run_cont(k)
}
(Node(x, left, right), k) => {
f(x)
go(left, Next(right, k))
}
}
}
go(self, Return)
}
fn[T] pre_order_cps_defunct_loop(self : Tree[T], f : (T) -> Unit) -> Unit {
loop (self, Return) {
(Leaf(x), k) => {
f(x)
match k {
Next(tree, k) => continue (tree, k)
Return => ()
}
}
(Node(x, left, right), k) => {
f(x)
continue (left, Next(right, k))
}
}
}
fn[T] pre_order_loop(self : Tree[T], f : (T) -> Unit) -> Unit {
let mut k = Return
let mut t = self
while true {
match t {
Leaf(x) => {
f(x)
match k {
Next(tree, next) => {
k = next
t = tree
}
Return => break
}
}
Node(x, left, right) => {
f(x)
k = Next(right, k)
t = left
}
}
}
}
TreeCont
实质上模拟了栈式存储结构:Next(right, k)
对应入栈操作,
而模式匹配 Next(tree, next)
则对应出栈操作。
这一洞察使我们能直接给出基于显式栈的实现:fn[T] pre_order_loop_stack(self : Tree[T], f : (T) -> Unit) -> Unit {
let k = []
let mut t = self
while true {
match t {
Leaf(x) => {
f(x)
match k.pop() {
Some(tree) => t = tree
None => break
}
}
Node(x, left, right) => {
f(x)
k.push(right)
t = left
}
}
}
}
4.4.4. Review and Summary [blog/defunctionalize/review]
TreeCont
。
这一转换揭示了延续本质上是对调用栈的结构化建模,
其中 Next
构造子对应栈帧压入操作,对其模式匹配则是出栈,
Return
则表征栈空状态。
通过此步骤,动态的函数调用关系被静态的数据结构所替代。run_cont
内联到主处理流程,
我们消除了函数间的相互递归调用,形成严格的尾递归形式。
此时程序的执行流已呈现近线性结构,
每个函数调用点的上下文关系完全由传入的延续对象所决定,
这为尾调用优化提供了理想的先决条件。TreeCont
到命令式栈的转换验证了理论计算机科学中“程序即数据”的观点。Blog 4.5. The Abstraction of Scientific Computing in LunaFlow [blog/lunaflow]
4.5.1. Levels of Abstraction [blog/lunaflow/layers]
Luna-Generic
的抽象框架下扩展自定义数据结构,
这些用户定义类型可无缝融入现有类型系统,并与上层模块达成双向互操作。
自然地,这引出一个关键性问题:如何构建具有数学严谨性的通用数据抽象? 4.5.2. Mathematical Structures In Luna-Generic [blog/lunaflow/generic]
4.5.2.1. Semiring [blog/lunaflow/semiring]
AddMonoid
与 MulMonoid
的实现
(其中 AddMonoid
隐含地要求加法运算满足交换律这一数学性质):trait AddMonoid: Add + Zero {}
trait MulMonoid: Mul + One {}
trait Semiring: AddMonoid + MulMonoid {}
/-- A semigroup is a type with an associative `(*)`. -/
class Semigroup (G : Type u) extends Mul G where
/-- Multiplication is associative -/
protected mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
Semiring
特征,
即可安全地调用加法与乘法运算。无论具体实例化为整数环、
布尔半环还是其他自定义代数结构,
编译器都能在类型检查阶段确保所有运算的合法性与完备性。
这种设计在保障类型安全的同时,达到了代码复用的最大化。
如 Luna-Poly
的实现中,多项式结构被 A
参数化,
并通过 Semiring
特征约束其元素类型,
任意实现了 Semiring
特征的类型都可以作为多项式的系数类型,
从而可以调用多项式的加法与乘法运算:impl[A : Eq + Semiring] Mul for Polynomial[A] with op_mul(xs, ys)
impl[A : Eq + Semiring] Add for Polynomial[A] with op_add(xs, ys)
4.5.3. Validating Constraints on Algebraic Structures [blog/lunaflow/testing]
4.5.3.1. How QuickCheck Works? [blog/lunaflow/quickcheck]
(T) -> Bool
的函数,
其中返回值 Bool
表示程序是否满足该属性。
随后通过生成器(Generator)来创建随机数据,
并将其传递给属性函数,并验证返回值是否为 true
。
(默认采用的是类型导向采样:即通过 Arbitrary
trait 将类型与数据生成规则绑定)
若属性函数在所有随机数据上均返回 true
,
则可以认为该属性成立。
否则,可认为该属性不成立,并且找到了一个反例,
QuickCheck 接着尝试缩小反例的大小,
以便更好地理解问题的根源。
(T) -> Bool
。其中,布尔返回值直观地表征当前输入数据是否满足预期性质。Arbitrary
这个 trait 将具体数据类型与其对应的随机生成规则进行约束绑定,从而实现类型安全的测试用例自动化生成。true
,则表明属性成立。反之,若发现存在反例,框架不仅会精准定位违规用例,还会使用收缩算法,通过逐步缩小反例的大小,最终呈现最精简的反例形态,以提高诊断问题的效率与精确度。Vector[T]
类型及其加法运算 op_add
时,
作为向量空间的基本要求,加法运算必须严格满足交换律与结合律。
具体而言,对于任意选择的向量 $\vec{u}, \vec{v}, \vec{w} \in V$,
必须满足以下数学约束:Vector
类型已正确实现 Arbitrary
trait):test "algebraic laws" {
fn prop(a : Vector[Int], b) { a + b == b + a }
fn prop(a : Vector[Int], b, c) { a + (b + c) == (a + b) + c }
quick_check_fn!(fn {
((a : Vector[Int]), (b : Vector[Int])) => {
guard a.length() == b.length() else { true }
prop(a, b)
}
})
quick_check_fn!(fn {
((a : Vector[Int]), (b : Vector[Int]), (c : Vector[Int])) => {
guard a.length() == b.length() && b.length() == c.length() else { true }
prop(a, b, c)
}
})
}
4.5.4. Real-world Usage of LunaFlow (Polynomial) [blog/lunaflow/instances]
4.5.5. Future of LunaFlow [blog/lunaflow/future]
Blog 4.6. You could have invented Fenwick trees [blog/fenwick]
4.6.1. Introduction [blog/fenwick/introduction]
Code 4.6.1.1. Implementing Fenwick trees with bit tricks in Java [blog/fenwick/java_fenwick]
class FenwickTree {
private long[] a;
public FenwickTree(int n) { a = new long[n+1]; }
public long prefix(int i) {
long s = 0;
for (; i > 0; i -= LSB(i)) s += a[i]; return s;
}
public void update(int i, long delta) {
for (; i < a.length; i += LSB(i)) a[i] += delta;
}
public long range(int i, int j) {
return prefix(j) - prefix(i-1);
}
public long get(int i) { return range(i,i); }
public void set(int i, long v) { update(i, v - get(i)); }
private int LSB(int i) { return i & (-i); }
}
range
、get
和 set
函数尚属直观,但其余函数则令人困惑。我们可以观察到,prefix
和 update
函数均调用了另一个名为 LSB
的函数,该函数不知何故对一个整数及其负数执行了按位逻辑与运算。事实上,LSB(x)
计算的是 $x$ 的最低有效位(least significant bit),即它返回最小的 $2^k$,使得 $x$ 的第 $k$ 位为 1。然而,LSB
的实现原理,以及最低有效位在此处用于计算更新和前缀和的方式与缘由,均非显而易见。LSB
函数的实现(第 4 节)。借助于该 DSL,我们将推导出在芬威克树与标准二叉树之间来回转换的函数(第 5 节)。最终,我们将能够推导出在芬威克树内部移动的函数:先将其转换为二叉树索引,执行显而易见的操作以实现二叉树内的预期移动,然后再转换回来。通过等式推理将转换过程融合消除,最终将揭示隐藏其后的LSB
函数,一如预期(第 6 节)。 4.6.2. Segment tree [blog/fenwick/segtree]
Code 4.6.2.1. Simple segment tree implementation in MoonBit [blog/fenwick/segtree_code]
update
和 rq
;随后,get
和 set
亦可基于它们来实现。将此代码推广至适用于存储来自任意交换幺半群(若不需要 set
操作)或任意阿贝尔群(即带逆元的交换幺半群,若需要 set
操作)的值的线段树亦非难事——但为简单起见,我们在此保持原状,因为这种推广对我们的主线故事并无增益。priv enum SegTree {
Empty
Branch(Int, Range, SegTree, SegTree)
} derive(Eq, Show)
fn SegTree::update(self : SegTree, i : Index, v : Int) -> SegTree {
match self {
Empty => Empty
Branch(a, rng, l, r) if rng.contains(i) =>
Branch(a + v, rng, l.update(i, v), r.update(i, v))
_ => self
}
}
fn rq(self : SegTree, q : Range) -> Int {
match self {
Empty => 0
Branch(a, rng, l, r) =>
if disjoint(rng, q) {
0
} else if subset(rng, q) {
a
} else {
l.rq(q) + r.rq(q)
}
}
}
fn SegTree::get(self : SegTree, i : Index) -> Int {
self.rq((i, i))
}
fn SegTree::set(self : SegTree, i : Index, v : Int) -> SegTree {
self.update(i, v - self.get(i))
}
typealias Int as Index
priv struct Range((Index, Index)) derive(Eq, Show)
fn subset(r1 : Range, r2 : Range) -> Bool {
let (a1, b1) = r1.inner()
let (a2, b2) = r2.inner()
a1 >= a2 && b1 <= b2
}
fn contains(self : Range, i : Index) -> Bool {
subset((i, i), self)
}
fn disjoint(r1 : Range, r2 : Range) -> Bool {
let (a1, b1) = r1.inner()
let (a2, b2) = r2.inner()
b1 < a2 || b2 < a1
}
range
函数的实现所见,如果我们能够计算任意 $k$ 的前缀和 $P_k = a_1 + \cdots + a_k$,那么我们就能通过 $P_j - P_{i-1}$ 来计算区间和 $a_i + \cdots + a_j$。Theorem 4.6.2.2. [blog/fenwick/thm/thm1]
4.6.3. Fenwick trees [blog/fenwick/fenwick_tree]
4.6.4. Two’s complement binary [blog/fenwick/two_complement]
to_enum
和 from_enum
的实现,用于实现和 Int
类型的互转,在此省略):enum Bit {
O
I
} derive(Eq)
pub fn Bit::not(self : Bit) -> Bit {
match self {
O => I
I => O
}
}
impl BitAnd for Bit with land(self, other) {
match (self, other) {
(O, _) => O
(I, x) => x
}
}
impl BitOr for Bit with lor(self, other) {
match (self, other) {
(I, _) => I
(O, x) => x
}
}
Int
—— 我们如何知道何时停止?(译者注:Lazy List 在 MoonBit 中也容易出现栈溢出的问题,比原文使用的 Haskell List
还要更坏一些) 事实上,这些实际问题源于一个更根本的问题:无限位列表对于二进制补码位串来说是一个糟糕的表示,因为它包含“垃圾”,即那些不对应于我们预期语义域中值的无限位列表。例如,cycle([I, O])
是一个永远在 I
和 O
之间交替的无限列表,但它并不代表一个有效的二进制补码整数编码。更糟糕的是非周期列表,比如在每个素数索引处为 I
而其他地方均为 O
的列表。priv enum Bits {
Rep(Bit)
Snoc(Bits, Bit)
} derive(Eq)
Rep(b)
代表一个由无限个位 b
组成的序列,而 Snoc(bs, b)
则代表位串 bs
后跟一个末位 b
。我们使用 Snoc
而非 Cons
,是为了与我们通常书写位串的方式相匹配,即最低有效位在最后。另请注意在 Snoc
的 Bits
字段上使用了严格性注解;这是为了排除仅使用 Snoc
构成的无限位列表,例如 bs = Snoc(Snoc(bs, O), I)
。换言之,构造类型为 Bits
的非底层值的唯一方法是拥有一个有限的 Snoc
序列,最终由一个 Rep
终止。Snoc(Rep(O)), O)
和 Rep(O)
都代表包含全零的无限位串。在 Haskell 中可以通过精心构造一个双向模式(Pickering et al., 2016)来解决这个问题,但是 MoonBit 并没有 ViewPatterns
的概念,所以我们必须手动调整模式匹配,下面的 pat_match
函数可以从一个 Bits
中匹配出一个 Bits
和一个 Bit
,make
则是其构造对偶,可以从一个 Bits
和一个 Bit
中构造出一个 Bits
。fn to_snoc(self : Bits) -> Bits {
match self {
Rep(a) => Snoc(Rep(a), a)
self => self
}
}
fn Bits::pat_match(self : Bits) -> (Bits, Bit) {
guard self.to_snoc() is Snoc(bs, b)
(bs, b)
}
fn Bits::make(self : Bits, b : Bit) -> Bits {
match (self, b) {
(Rep(b), b1) if b == b1 => Rep(b)
(bs, b) => Snoc(bs, b)
}
}
.pat_match()
进行匹配时,会潜在地将一个 Rep
展开一步成为 Snoc
,这样我们就可以假装 Bits
值总是由 make
构造的。反之,使用 make
构造一个 Bits
值时,如果我们恰好将一个相同的位 b
追加到一个现有的 Rep b
上,它将什么也不做。这确保了只要我们坚持使用 make
和 pat_match
而从不直接使用 Snoc
,Bits
值将始终被规范化,使得末端的 Rep(b)
立即跟随着一个不同的位。
读者可能会认为 pat_match
中的 guard
并不安全,实际上它确实足以处理 Bits
类型的所有可能输入。然而,为了获得能停机的算法,我们通常会包含一个或多个针对 Rep
的特殊情况。Bits
和 Int
之间转换以及显示 Bits
(仅用于测试目的)的函数开始。fn Bits::to_bits(n : Int) -> Bits {
match n {
0 => Rep(O)
-1 => Rep(I)
n => Bits::make(Bits::to_bits(div(n, 2)), Bit::to_enum(n % 2))
}
}
fn Bits::from_bits(self : Bits) -> Int {
match self {
Rep(O) => 0
Rep(I) => -1
bs => {
let (bs, b) = bs.pat_match()
2 * Bits::from_bits(bs) + Bit::from_enum(b)
}
}
}
Show
的实现:impl Show for Bits with to_string(self) {
fn go(s) {
match s {
Rep(b) => b.to_string().repeat(3) + "..."
s => {
let (bs, b) = s.pat_match()
b.to_string() + go(bs)
}
}
}
go(self).rev()
}
impl Show for Bits with output(self, logger) {
logger.write_string(self.to_string())
}
test "from . to == id" {
let b = Snoc(Rep(O), O) |> Snoc(I) |> Snoc(O) |> Snoc(I)
inspect(b, content="...0000101")
let b1 = Snoc(Rep(I), O) |> Snoc(I)
inspect(b1, content="...11101")
let b26 = Bits::to_bits(26)
inspect(b26, content="...00011010")
let b_30 = Bits::to_bits(-30)
inspect(b_30, content="...11100010")
inspect(b_30.from_bits(), content="-30")
@qc.quick_check_fn(x => Bits::from_bits(Bits::to_bits(x)) == x)
// +++ [100/0/100] Ok, passed!
}
Bits
上实现一些基本操作了。首先,递增和递减可以递归地实现如下:fn inc(self : Bits) -> Bits {
match self {
Rep(I) => Rep(O)
s =>
match s.pat_match() {
(bs, O) => Bits::make(bs, I)
(bs, I) => Bits::make(bs.inc(), O)
}
}
}
fn dec(self : Bits) -> Bits {
match self {
Rep(O) => Rep(I)
s =>
match s.pat_match() {
(bs, I) => Bits::make(bs, O)
(bs, O) => Bits::make(bs.dec(), I)
}
}
}
fn lsb(self : Bits) -> Bits {
match self {
Rep(O) => Rep(O)
s =>
match s.pat_match() {
(bs, O) => Bits::make(bs.lsb(), O)
(_, I) => Bits::make(Rep(O), I)
}
}
}
Rep(O)
添加了一个特殊情况,以确保 lsb
是全函数。严格来说,Rep(O)
没有最低有效位,因此定义 lsb(Rep(O)) = Rep(O)
似乎是合理的。test "lsb" {
inspect(Bits::to_bits(26), content="...00011010")
inspect(Bits::to_bits(26).lsb(), content="...00010")
inspect(Bits::to_bits(24), content="...00011000")
inspect(Bits::to_bits(24).lsb(), content="...0001000")
}
pat_match
的匹配会自动扩展较短的一个以匹配较长的那个。impl BitAnd for Bits with land(self, other) {
match (self, other) {
(Rep(x), Rep(y)) => Rep(x & y)
(xs, ys) =>
match (xs.pat_match(), ys.pat_match()) {
((bs, b), (bs1, b1)) => Bits::make(bs.lsb() & bs1.lsb(), b & b1)
}
}
}
fn Bits::inv(self : Bits) -> Bits {
match self {
Rep(x) => Rep(x.not())
s =>
match s.pat_match() {
(bs, b) => Bits::make(bs.inv(), b.not())
}
}
}
zipWith
来实现 land
,用 map
来实现 inv
。然而,就目前的目的而言,我们不需要这种额外的通用性。Rep
的特殊情况。
(译者注:原文中 op_add
的实现是非穷尽的,下面是修正后的版本):impl Add for Bits with op_add(self, other) {
match (self, other) {
(xs, Rep(O)) | (Rep(O), xs) => xs
(Rep(I), Rep(I)) => Bits::make(Rep(I), O)
_ =>
match (self.pat_match(), other.pat_match()) {
((xs, I), (ys, I)) => Bits::make((xs + ys).inc(), O)
((xs, x), (ys, y)) => Bits::make(xs + ys, x | y)
}
}
}
test "add" {
@qc.quick_check_fn(fn(x : (Int, Int)) {
x.0 + x.1 == Bits::from_bits(Bits::to_bits(x.0) + Bits::to_bits(x.1))
})
// +++ [100/0/100] Ok, passed!
}
x : Bits
,都有 $x + \text{neg } x = \text{Rep(O)}$。impl Neg for Bits with op_neg(self) {
self.inv().inc()
}
Theorem 4.6.4.1. [blog/fenwick/thm/thm2]
pat_match(bs, b)
和 make(bs, b)
记为 $bs : b$,运算名的 op_
前缀均省略。
fn set_to(self : Bits, idx : Int, b1 : Bit) -> Bits {
match (idx, self.pat_match()) {
(0, (bs, _)) => Bits::make(bs, b1)
(k, (bs, b)) => Bits::make(bs.set_to(k - 1, b1), b)
}
}
fn Bits::set(self : Bits, idx : Int) -> Bits {
self.set_to(idx, I)
}
fn Bits::clear(self : Bits, idx : Int) -> Bits {
self.set_to(idx, O)
}
fn test_helper(self : Bits, i : Int) -> Bool {
loop (i, self.pat_match()) {
(0, (_bs, b)) => b == I
(k, (bs, _b)) => continue (k - 1, bs.pat_match())
}
}
fn odd(self : Bits) -> Bool {
self.test_helper(0)
}
fn even(self : Bits) -> Bool {
not(self.odd())
}
while
组合子,它迭代一个给定的函数,返回第一个使得谓词为假的迭代结果。fn shr(self : Bits) -> Bits {
self.pat_match().0
}
fn shl(self : Bits) -> Bits {
Bits::make(self, O)
}
fn[A] while_(p : (A) -> Bool, f : (A) -> A, x : A) -> A {
loop x {
x => if p(x) { continue f(x) } else { x }
}
}
4.6.5. Index conversion [blog/fenwick/index_conv]
Code 4.6.5.1. Recurrence for sequence of binary tree indices in a Fenwick array [blog/fenwick/interleaving]
fn[T] interleave(sel : List[T], other : List[T]) -> List[T] {
match (sel, other) {
(Nil, _) => Nil
(Cons(x, xs), ys) => Cons(x, interleave(ys, xs))
}
}
fn b(i : Int) -> List[Int] {
match i {
0 => Cons(2, Nil)
n =>
Int::until(1 << n, (1 << n) + (1 << (n - 1))).map(x => x * 2)
|> from_iter
|> interleave(b(n - 1))
}
}
interleave
记为中缀运算符 $\curlyvee$)。test "b(4)" {
inspect(
b(4),
content="@list.of([32, 16, 34, 8, 36, 18, 38, 4, 40, 20, 42, 10, 44, 22, 46, 2])",
)
}
s.nth(k)
(译者注:这和 MoonBit 标准库的 nth
存在差异,它是从 0 开始的索引)。下面的代码指出了两个关于索引和交错相互作用的简单引理,即 $(xs \curlyvee ys) ! (2 \cdot j) = ys ! j$ 和 $(xs \curlyvee ys) ! (2 \cdot j - 1) = xs ! j$(只要 $xs$ 和 $ys$ 长度相等)。// suppose xs.length() == ys.length()
interleave(xs, ys).nth(2 * j) == ys.nth(j)
interleave(xs, ys).nth(2 * j + 1) == xs.nth(j)
f2b
的定义如下。首先,对于偶数输入,我们有fn { x => 2 * x }
的简写,$[2^n \ldots 2^n + 2^{n-1} - 1]$ 是闭区间 $[2^n, 2^n + 2^{n-1} - 1]$ 的列表。对于奇数输入有:f2b
包括只要输入是偶数就重复除以 2(即右位移),然后最终减 1 并加上一个 2 的幂。然而,要知道最后要加哪个 2 的幂,取决于我们移动了多少次。思考这个问题的一个更好的方法是在开始时加上 $2^{n+1}$,然后让它随着其他所有位一起移动。(译者注:原文在这里说的并不是很清楚,在这里补充一下我的解释:我们想要求解 $X = 2^{n-a+1} + b$,可以先乘上一个因子 $2^a$ 得到 $2^a X = 2^{n+1} + 2^ab$,这样表达式中便有一个 $k = 2^a \cdot b$ 存在,它是函数的参数。这样一来等式的右边即是 $k$ 加上一个 $2^{n+1}$,而 $X = \dfrac{2^{n+1} + 2^a \cdot b}{2^a}$,除法在这里可以使用位移操作实现)因此,我们使用我们的 Bits
DSL 得到 f2b
的最终定义。单独定义 shift
函数将使我们的一些证明更加紧凑。fn shift(n : Int, se : Bits) -> Bits {
while_(Bits::even, Bits::shr, se.set(n))
}
fn f2b(n : Int, se : Bits) -> Bits {
shift(n + 1, se).dec()
}
f2b(4, k)
相同的结果。b2f(n, _)
,它将从二叉树索引转换回芬威克索引。b2f(n, _)
应该是 f2b(n, _)
的左逆,也就是说,对于任何 $k \in [1, 2^n]$,我们应该有 $\text{b2f}(n, \text{f2b}(n, k)) = k$。
如果 $k$ 是 f2b
的一个输入,我们有 $k = 2^a \cdot b \le 2^n$,因此 $b-1 \lt 2^{n-a}$。故给定输出 $\text{f2b}(n, k) = m = 2^{n-a+1} + b - 1$,
$m$ 的最高位是 $2^{n-a+1}$,其余位代表 $b - 1$。所以,一般地,给定某个作为 f2b(n, _)
输出的 $m$,我们可以唯一地将其写为 $m = 2^c + d$,其中 $d \lt 2^{c-1}$;那么fn unshift(n : Int, se : Bits) -> Bits {
while_(x => not(x.test_helper(n)), Bits::shl, se) |> Bits::clear(_, n)
}
fn b2f(n : Int, se : Bits) -> Bits {
unshift(n + 1, se.inc())
}
test "id" {
let f = size => Int::until(1, 1 << size)
.map(x => (f2b(size, x |> Bits::to_bits) |> b2f(size, _) |> Bits::from_bits) ==
x)
.all(x => x)
assert_true(f(4))
assert_true(f(5))
}
4.6.6. Deriving Fenwick operations [blog/fenwick/deriving]
Theorem 4.6.6.1. shr-inc-dec [blog/fenwick/thm/thm3]
Theorem 4.6.6.2. while-inc-dec [blog/fenwick/thm/thm4]
Bits
归纳证明。例如,对于 inc
的情况,两侧的函数都会丢弃连续的 1 位,然后将第一个 0 位翻转为 1。Theorem 4.6.6.3. shl-shr [blog/fenwick/thm/thm5]
test_helper
,$\cdot$ 在此处是匿名函数简写: fn { x => not(test_helper(x, n + 1)) }
)update
和 query
;我们先从 update
开始。在实现 update
操作时,我们需要从一个叶节点开始,沿着路径向上到达根节点,更新沿途所有活跃的节点。实际上,对于任何给定的叶节点,其最近的活跃父节点恰好是存储在过去对应于该叶节点的槽中的节点(参见图 13)。因此,要更新索引 $i$,我们只需从芬威克数组中的索引 $i$ 开始,然后重复找到最近的活跃父节点,边走边更新。回想一下,用于 update
的命令式代码就是这样做的,通过在每一步加上当前索引的 LSB 来找到最近的活跃父节点:fn update(self : FenwickTree, i : Int, delta : Int) -> Unit {
let mut i = i
while i < self.inner().length() {
self.inner()[i] += delta
i += FenwickTree::lsb(i)
}
}
fn active_parent_binary(self : Bits) -> Bits {
while_(Bits::odd, Bits::shr, self.shr())
}
lsb
函数本身通过递归栈来跟踪;找到第一个 1 位后,递归栈展开并将所有递归经过的 0 位重新追加回去。上述流水线代表了一种替代方法:将位 $n+1$ 设置为“哨兵”来跟踪我们移动了多少;右移直到第一个 1 确实在个位上,此时我们加 1;然后通过左移将所有 0 位移回,直到哨兵位回到 $n+1$ 的位置。这个过程的一个例子如图 19 所示。当然,这只适用于值足够小,以至于哨兵位在整个操作过程中不会受到干扰的情况。at_lsb
,它执行一个“在 LSB 处”的操作,即它移出 0 位直到找到一个 1,应用给定的函数,然后恢复 0 位。fn at_lsb(self : Bits, f : (Bits) -> Bits) -> Bits {
match self {
Rep(O) => Rep(O)
s =>
match s.pat_match() {
(bs, O) => bs.at_lsb(f) |> Bits::make(O)
(bs, I) => Bits::make(bs, I) |> f
}
}
}
Theorem 4.6.6.4. add-lsb [blog/fenwick/thm/thm6]
at_lsb
)atLSB
形式化地关联起来,通过以下(相当复杂的)引理:Theorem 4.6.6.5. sentinel [blog/fenwick/thm/thm7]
inc
和 dec
都符合 $f$ 的标准:只要 $n \ge 1$,对某个 $0 \lt x \lt 2^n$ 进行递增或递减不会影响第 $(n+1)$ 位,并且对一个小于 $2^n + 2^{n-1}$ 的数进行递增或递减的结果将是一个小于 $2^{n+1}$ 的数。我们现在可以将所有部分组合起来,证明在每一步加上 LSB 是实现 update
的正确方法。Theorem 4.6.6.6. [blog/fenwick/thm/thm8]
fn prev_segment_binary(self : Bits) -> Bits {
while_(Bits::even, Bits::shr, self).dec()
}
Theorem 4.6.6.7. [blog/fenwick/thm/thm9]
4.6.7. Conclusion [blog/fenwick/conclusion]
Blog 4.7. 用 MoonBit 实现 LRU 缓存算法 [blog/lrualgorithm]
4.7.1. LRU 缓存简介 [blog/lrualgorithm/whats]
put(1, "一")
→ 缓存现状:[(1, “一”)]put(2, "二")
→ 缓存现状:[(2, “二”), (1, “一”)]put(3, "三")
→ 缓存现状:[(3, “三”), (2, “二”), (1, “一”)]get(1)
→ 返回 “一”,缓存现状:[(1, “一”), (3, “三”), (2, “二”)] (注意 1 被移到了最前面)put(4, "四")
→ 缓存已满,淘汰最久未使用的 (2, “二”),缓存现状:[(4, “四”), (1, “一”), (3, “三”)]get(2)
→ 返回 None (不存在)
4.7.2. 定义基础数据结构 [blog/lrualgorithm/define]
// 定义Node结构体,用于双向链表
struct Node[K, V] {
key : K
mut value : V
mut pre : Node[K, V]? // 前驱节点
mut next : Node[K, V]? // 后继节点
}
// Node构造函数
fn new_node[K, V](k : K, v : V) -> Node[K, V] {
{ key: k, value: v, pre: None, next: None }
}
[K, V]
:这使得我们的 LRU 缓存可以适用于任何类型的键和值,非常灵活。mut
:value
、pre
和 next
都被标记为 mut
,意味着它们可以在创建后修改。这对于我们需要频繁调整链表结构的 LRU 缓存来说是必须的。?
:pre
和 next
是可选类型,表示它们可能为 None
。这样处理链表两端的节点会更加自然。new_node
函数帮助我们创建一个新节点,初始状态下前驱和后继都是 None
。// LRU缓存结构体
struct LRUCache[K, V] {
capacity : Int // 容量
dummy : Node[K, V] // 哑节点,用于标记双向链表的头尾
key_to_node : Map[K, Node[K, V]] // 键到节点的映射
}
dummy.next
指向链表中最近使用的节点(实际的第一个节点)dummy.pre
指向链表中最久未使用的节点(实际的最后一个节点) 4.7.3. 构造函数实现 [blog/lrualgorithm/construction]
fn new[K : Hash + Eq, V](
capacity : Int,
default_k : K,
default_v : V
) -> LRUCache[K, V] {
// 创建一个哑元节点,使用提供的默认值
let dummy = new_node(default_k, default_v)
// 初始化dummy节点,指向自身形成环
dummy.next = Some(dummy)
dummy.pre = Some(dummy)
{ capacity, dummy, key_to_node: Map::new() }
}
K : Hash + Eq
这个约束,它表明我们的键类型必须支持哈希操作和相等性比较。这是因为我们要用键来创建哈希映射,所以键必须是可哈希和可比较的。default_k
和 default_v
来初始化哑元节点。这是 MoonBit 类型系统的要求,即使哑元节点不用于存储实际数据,我们也需要为它提供合法的值。next
和 pre
都指向自身,形成一个空的环形链表。这是一种巧妙的技巧,确保我们在链表为空时,不会遇到空指针问题。{ capacity, dummy, key_to_node: Map::new() }
创建并返回了 LRUCache 的实例。
dummy ⟷ dummy (自己指向自己)
dummy ⟷ A ⟷ dummy
dummy ⟷ B ⟷ A ⟷ dummy
dummy.next
指向最近使用的节点(B),而 dummy.pre
指向最久未使用的节点(A)。get
和 put
等核心操作奠定了基础。下一步,我们将实现这些核心操作以完成 LRU 缓存的功能。 4.7.4. 核心操作 - get 和 put [blog/lrualgorithm/core]
get
和 put
。这两个操作是 LRU 缓存的精髓所在,也是最常用的接口。get
方法用于从缓存中获取某个键对应的值。如果键存在,它还需要将对应的节点移到“最近使用“的位置:fn get[K : Hash + Eq, V](self : LRUCache[K, V], key : K) -> V? {
let node = get_node(self, key)
match node {
Some(n) => Some(n.value)
None => None
}
}
get_node
方法,这个方法不仅查找节点,还负责调整节点位置。下面是 get_node
的实现:fn get_node[K : Hash + Eq, V](self : LRUCache[K, V], key : K) -> Node[K, V]? {
if self.key_to_node.contains(key) {
if self.key_to_node.get(key) is Some(node) {
// 将节点移到链表前端
remove(self, node)
push_front(self, node)
return Some(node)
}
}
None
}
get_node
方法做了几件重要的事:
remove
和 push_front
(后面会详细介绍),它们负责链表的具体操作。put
方法用于向缓存中添加或更新键值对:fn put[K : Hash + Eq, V](self : LRUCache[K, V], key : K, value : V) -> Unit {
// 如果键已存在,更新值并移到链表前端
let existing = get_node(self, key)
if existing is Some(node) {
node.value = value
return
}
// 创建新节点
let node = new_node(key, value)
// 将新节点加入链表前端
push_front(self, node)
self.key_to_node.set(key, node)
// 如果超出容量,删除最久未使用的节点
if self.key_to_node.size() > self.capacity {
if self.dummy.pre is Some(last_node) {
self.key_to_node.remove(last_node.key)
remove(self, last_node)
}
}
}
put
方法的逻辑分为几个部分:
get_node
方法)get_node
已经将节点移到了链表前端
dummy.pre
)指向的节点
push_front
和 remove
这两个关键的辅助方法,它们是实现 LRU 缓存链表操作的基础。 4.7.5. 辅助操作 - push_front 和 remove [blog/lrualgorithm/auxiliary]
get
和 put
,但它们都依赖于两个关键的辅助方法:push_front
和 remove
。这两个方法负责维护双向链表的结构,是整个 LRU 算法能够正常工作的基础。push_front
方法用于将一个节点插入到链表的最前端(即最近使用的位置):fn push_front[K, V](self : LRUCache[K, V], node : Node[K, V]) -> Unit {
node.next = self.dummy.next
node.pre = Some(self.dummy)
if node.pre is Some(pre) {
pre.next = Some(node)
}
if node.next is Some(next) {
next.pre = Some(node)
}
}
next
指向原来的第一个节点(即 dummy.next
)pre
指向哑元节点next
指向新节点pre
指向新节点is Some
模式匹配来安全地处理可选值,这是 MoonBit 处理空值的一种优雅方式。remove
方法用于从链表中删除一个节点:fn remove[K, V](self : LRUCache[K, V], node : Node[K, V]) -> Unit {
if node.pre is Some(pre) {
pre.next = node.next
}
if node.next is Some(next) {
next.pre = node.pre
}
}
next
指向节点的下一个节点pre
指向节点的前一个节点
push_front
确保最近访问的项总是位于链表的前端remove
用于两个场景:
push_front
中,我们先设置新节点的指针,再更新相邻节点的指针remove
中,我们直接更新相邻节点的指针,跳过要删除的节点
4.7.6. 实用辅助方法 [blog/lrualgorithm/auxiliary-other]
get
/put
以及链表操作的辅助方法。为了让我们的 LRU 缓存更加完整和易用,现在我们来添加一些实用的辅助方法。fn size[K, V](self : LRUCache[K, V]) -> Int {
self.key_to_node.size()
}
fn is_empty[K, V](self : LRUCache[K, V]) -> Bool {
self.key_to_node.size() == 0
}
fn contains[K : Hash + Eq, V](self : LRUCache[K, V], key : K) -> Bool {
self.key_to_node.contains(key)
}
contains
方法,快速判断一个键是否在缓存中。
is_empty()
比 size() == 0
更直观key_to_node
哈希表// 检查键是否存在,而不获取值(避免改变使用顺序)
if contains(cache, "key") {
// 键存在,可以进行一些操作
}
// 缓存为空时执行特定逻辑
if is_empty(cache) {
// 缓存为空,可以执行初始化或其他操作
}
// 获取缓存使用情况
let usage_percentage = size(cache) * 100 / cache.capacity
4.7.7. 总结与思考 [blog/lrualgorithm/summary]
get
和 put
方法是最有趣的部分。这两个方法看似简单,却包含了 LRU 算法的核心思想:每次访问都要更新使用顺序,确保最近使用的项目保留在缓存中。当我看到这些方法能够正确工作时,那种成就感是难以形容的。Blog 4.8. Understanding Local Type Inference [blog/lti]
4.8.1. How to Read Typing Rules [blog/lti/how_to_read]
Var
或 App
。
4.8.2. Just Enough Type Information [blog/lti/enough]
cons[Int](3, nil[Int])
中那两个多余的 Int
标注。
map(list, fun(x) x+1)
这样的上下文中,为匿名函数的参数 x
补上类型标注,只会掩盖其核心逻辑,实为一种不必要的干扰。
4.8.2.1. Strategies [blog/lti/strategies]
4.8.3. Language Specification [blog/lti/language]
Var
是类型变量的实现:pub(all) enum Type {
TyVar(Var)
TyTop
TyBot
TyFun(Array[Var], Array[Type], Type)
} derive(Eq)
pub(all) enum Expr {
EVar(Var)
EApp(Expr, Array[Type], Array[Expr])
EAbs(Array[Var], Array[(Var, Type)], Expr)
}
4.8.3.1. Subtyping Relation [blog/lti/subtype]
4.8.3.1.1. Solution [blog/lti/subtype_code]
/// l <: r
struct Subtype {
l : Type
r : Type
}
pub fn subtype(self : Subtype) -> Bool {
match (self.l, self.r) {
(TyVar(v1), TyVar(v2)) => v1 == v2
(_, TyTop) => true
(TyBot, _) => true
(TyFun(xs1, r, s), TyFun(xs2, t, u)) if xs1 == xs2 =>
subtypes(t, r) && { l: s, r: u }.subtype()
_ => false
}
}
4.8.3.1.2. Solution [blog/lti/subtype_code2]
s | t
,
将 $S \wedge T$ 实现为 s & t
。这两个运算符的定义如下:impl BitAnd for Type with land(s, t) {
match (s, t) {
(TyFun(xs1, v, p), TyFun(xs2, w, q)) if xs1 == xs2 => {
guard v.length() == w.length() else { TyBot }
TyFun(xs1, v.zip(w).map(z => z.0 | z.1), p & q)
}
(s, t) if s.subtype(t) => s
(s, t) if t.subtype(s) => t
_ => TyBot
}
}
impl BitOr for Type with lor(s, t) {
match (s, t) {
(TyFun(xs1, v, p), TyFun(xs2, w, q)) if xs1 == xs2 => {
guard v.length() == w.length() else { TyTop }
TyFun(xs1, v.zip(w).map(z => z.0 & z.1), p | q)
}
(s, t) if s.subtype(t) => t
(s, t) if t.subtype(s) => s
_ => TyTop
}
}
4.8.4. Explicit Typing Rules [blog/lti/explicit]
核心定则 (Core Rules)
f
的类型,然后验证所有实际参数(包括类型参数与项参数)是否与函数的签名相符。
这里的要求更宽松了一些:只要实际参数的类型满足参数类型的子类型关系即可,而不需要完全匹配。 4.8.4.1. Type Parameter Substitution [blog/lti/subst_code]
mk_subst
函数,用来生成一个类型替换映射,
还有一个 apply_subst
函数可以将这个映射应用到一个具体类型上。
$[\overline{T}/\overline{X}]R$ 就是通过 $\text{apply\_subst}(\text{mk\_subst}(\overline{X},\overline{T}), R)$ 得到的。pub fn mk_subst(vars : Array[Var], tys : Array[Type]) -> Map[Var, Type] raise {
guard vars.length() == tys.length() else { raise ArgumentLengthMismatch }
Map::from_array(vars.zip(tys))
}
pub fn apply_subst(self : Type, subst : Map[Var, Type]) -> Type {
match self {
TyVar(v) => subst.get(v).unwrap_or(self)
TyTop | TyBot => self
TyFun(xs, ss, t) => {
let fs = subst.iter().filter(kv => !xs.contains(kv.0)) |> Map::from_iter
let new_ss = ss.map(s => s.apply_subst(fs))
let new_t = t.apply_subst(fs)
TyFun(xs, new_ss, new_t)
}
}
}
4.8.5. Local Type Argument Synthesis [blog/lti/synthesis]
App
能够根据此参数为应用表达式计算出结果类型。
现在我们为了语言更简单易用,允许省略类型参数 $\overline{T}$,现在我们更新语言的构造:pub(all) enum Type {
TyVar(Var)
TyTop
TyBot
TyFun(Array[Var], Array[Type], Type)
} derive(Eq)
pub(all) enum Expr {
EVar(Var)
EAppI(Expr, Array[Expr])
EApp(Expr, Array[Type], Array[Expr])
EAbs(Array[Var], Array[(Var, Type)], Expr)
EAbsI(Array[Var], Array[Var], Expr)
}
EAppI(Expr, Array[Expr])
,对应我们的省略类型参数形式。
(为了后文叙述方便,这里也增加了后文会用到的 EAbsI
构造)
现在我们需要一条新的规则: 4.8.6. Constraint Generation [blog/lti/cg]
4.8.6.1. Variable Elimination [blog/lti/var_elim]
4.8.6.1.1. Promotion and Demotion Rules [blog/lti/ve_rules]
pub fn promotion(self : Type, v : Set[Var]) -> Type {
match self {
TyFun(xs, ss, t) => {
let vP = v.iter().filter(x => !xs.contains(x)) |> Set::from_iter
let us = ss.map(_.demotion(vP))
let r = t.promotion(vP)
guard xs.iter().all(x => !v.contains(x))
TyFun(xs, us, r)
}
TyVar(vr) if v.contains(vr) => TyTop
_ => self
}
}
pub fn demotion(self : Type, v : Set[Var]) -> Type {
match self {
TyFun(xs, ss, t) => {
let vP = v.iter().filter(x => !xs.contains(x)) |> Set::from_iter
let us = ss.map(_.demotion(vP))
let r = t.demotion(vP)
TyFun(xs, us, r)
}
TyVar(vr) if v.contains(vr) => TyBot
_ => self
}
}
4.8.6.2. Constraint and Constraint Set Code [blog/lti/cg_def_code]
struct Constraints(Map[Var, Subtype])
pub fn Constraints::empty() -> Constraints {
Constraints(Map::new())
}
pub fn meet(self : Constraints, other : Constraints) -> Constraints {
union_with(self.inner(), other.inner(), (l, r) => {
let { l: l1, r: r1 } = l
let { l: l2, r: r2 } = r
{ l: l1 & l2, r: r1 | r2 }
})
}
pub fn meets(c : Array[Constraints]) -> Constraints {
c.iter().fold(init=Constraints::empty(), Constraints::meet)
}
4.8.6.3. Constraint Generation Code [blog/lti/cg_code]
/// Pre-condition: xs and v are disjoint sets of variables.
pub fn generate(
self : Subtype,
xs : Array[Var],
v : Set[Var],
) -> Constraints raise {
match (self.l, self.r) {
(_, TyTop) | (TyBot, _) => Constraints::empty()
(TyVar(y1), TyVar(y2)) if y1 == y2 && !xs.contains(y1) =>
Constraints::empty()
(TyVar(y), s) if xs.contains(y) => {
let t = s.demotion(v)
Map::from_array([(y, { l: TyBot, r: t })])
}
(s, TyVar(y)) if xs.contains(y) => {
let t = s.promotion(v)
Map::from_array([(y, { l: t, r: TyTop })])
}
(TyFun(ys1, r, s), TyFun(ys2, t, u)) if ys1 == ys2 => {
let vy = v.union(Set::from_array(ys1))
let cs = t.zip(r).map(tr => { l: tr.0, r: tr.1 }.generate(xs, vy))
|> meets()
cs.meet({ l: s, r: u }.generate(xs, vy))
}
_ => raise ConstraintGenerationError
}
}
4.8.7. Calculating Type Arguments [blog/lti/calc_args]
4.8.7.1. Polarity [blog/lti/polarity]
4.8.7.1.1. Variance Code [blog/lti/variance_code]
pub fn variance(self : Type, va : Var) -> Variance {
letrec go = (ty : Type, polarity : Bool) => match ty {
TyVar(v) if v == va => if polarity { Covariant } else { Contravariant }
TyVar(_) | TyTop | TyBot => Constant
TyFun(_, params, ret) => {
let param_variance = params
.map(p => go(p, !polarity))
.fold(init=Constant, combine_variance)
combine_variance(param_variance, go(ret, polarity))
}
}
and combine_variance = (v1 : Variance, v2 : Variance) => match (v1, v2) {
(Constant, v) | (v, Constant) => v
(Covariant, Covariant) | (Contravariant, Contravariant) => v1
(Covariant, Contravariant) | (Contravariant, Covariant) => Invariant
(Invariant, _) | (_, Invariant) => Invariant
}
go(self, true)
}
App-InfSpec
中无法找到唯一最优解的情形。 4.8.7.2. Solving Constraints [blog/lti/solve_code]
pub fn solve(self : Constraints, ty : Type) -> Map[Var, Type]? {
let f = (vs : (Var, Subtype)) => {
let { l, r } = vs.1
let v = match ty.variance(vs.0) {
Constant | Covariant => Some(l)
Contravariant => Some(r)
Invariant => if l == r { Some(l) } else { None }
}
v.map(v => (vs.0, v))
}
let i = self.inner().iter().filter_map(f)
guard i.count() == self.inner().size() else { None }
Some(Map::from_iter(i))
}
4.8.7.3. Proof Sketch [blog/lti/proof_eq]
App-InfSpec
规约完全一致?
App-InfSpec
规约之间的等价性。
它允许我们最终用一个完全算法化的规则 App-InfAlg
来取代那个不可执行的规约: 4.8.8. Bidirectional Checking [blog/lti/bidirectional]
fun[](x) x+1
)中绑定变量 x
的类型?let x = ...
)无需显式类型标注?fun[](x) x+1
这样的表达式中,没有任何子结构能为 x
的类型提供信息。两种模式:综合与检查
f(e)
完美地展示了这一过程:类型检查器会先综合出函数 f
的类型,然后利用该类型提供的信息,切换模式去检查参数 e
。 4.8.8.1. Typing Rules [blog/lti/bidi_rules]
变量规则 (Variable Rules)
函数抽象规则 (Function Abstraction Rules)
fun [X] (x:S) e
的函数,其类型参数 $\overline{X}$ 和值参数 $\overline{x}$ 的类型 $\overline{S}$ 都被明确标注了。
fun [X] (x) e
时,我们可以从预期的函数类型 $\forall \overline{X}. \overline{S} \rightarrow T$ 中获取信息。
fun [X] (x:S) e
需要被检查是否符合某个预期类型 $\forall \overline{X}. \overline{T} \rightarrow R$ 时:
函数应用规则 (Function Application Rules)
S-App
一样:综合 $f$ 的类型,并检查参数 $\overline{e}$。
结合双向检查和类型参数综合的规则
App-InfAlg
规则的检查版本。
顶类型和底类型
synthesis
和 check
两个关键函数上,
这是本文最重要的一个练习,
强烈建议读者自己尝试实现这两个函数,来体会双向检查的精妙之处,
并从中学习将类型规则转化为代码的技巧。 4.8.8.2. Bidirectional Typing Code [blog/lti/bidi_code]
pub fn synthesis(self : Expr, gamma : Context) -> Type raise {
match self {
EVar(v) => gamma[v]
EAbs(xs, vs, body) => {
let ctx = gamma.append_vars(xs).append_binds(vs)
let body_ty = body.synthesis(ctx)
TyFun(xs, vs.map(xS => xS.1), body_ty)
}
EAppI(f, e) => {
let t = f.synthesis(gamma)
guard !(t is TyBot) else { TyBot }
guard t is TyFun(xs, t, r) else { raise SynthesisError }
// guard !xs.is_empty() else { raise NotFound }
let es = e.map(_.synthesis(gamma))
let cs = es.zip(t).map(z => { l: z.0, r: z.1 }.generate(xs, Set::new()))
let sigma = meets(cs).solve(r)
sigma.map(s => r.apply_subst(s)).or_error(SynthesisError)
}
EApp(f, ty, e) => {
let t = f.synthesis(gamma)
guard !(t is TyBot) else { TyBot }
guard t is TyFun(xs, ss, r) else { raise SynthesisError }
let subst = mk_subst(xs, ty)
e.zip(ss).each(es => es.0.check(es.1.apply_subst(subst), gamma))
r.apply_subst(subst)
}
_ => raise SynthesisError
}
}
pub fn check(self : Expr, ty : Type, gamma : Context) -> Unit raise {
match (self, ty) {
(_, TyTop) => ()
(EVar(v), t) => {
let gx = gamma[v]
guard gx.subtype(t) else { raise CheckError }
}
(EAbs(xs, vs, body), TyFun(xsP, t, r)) if xs == xsP => {
let ctx = gamma.append_vars(xs)
guard t.zip(vs.map(xS => xS.1)).iter().all(z => z.0.subtype(z.1)) else {
raise CheckError
}
body.check(r, ctx.append_binds(vs))
}
(EAbsI(xs, vs, body), TyFun(xsP, ss, t)) if xs == xsP &&
ss.length() == vs.length() =>
body.check(t, gamma.append_vars(xs).append_binds(vs.zip(ss)))
(EAppI(f, e), u) => {
let t = f.synthesis(gamma)
guard !(t is TyBot && u is TyBot) else { () }
guard f.synthesis(gamma) is TyFun(xs, t, r) else { raise CheckError }
guard !xs.is_empty() else { () }
let es = e.map(_.synthesis(gamma))
let cs = es.zip(t).map(z => { l: z.0, r: z.1 }.generate(xs, Set::new()))
let d = { l: r, r: u }.generate(xs, Set::new())
guard meets(cs).meet(d).satisfiable() else { raise CheckError }
}
(EApp(f, ty, e), u) => {
let t = f.synthesis(gamma)
guard !(t is TyBot && u is TyBot) else { () }
guard t is TyFun(xs, ss, r)
let subst = mk_subst(xs, ty)
e.zip(ss).each(es => es.0.check(es.1.apply_subst(subst), gamma))
guard r.apply_subst(subst).subtype(u) else { raise CheckError }
}
_ => raise CheckError
}
}
ELet
,但其规则是显然的: 4.8.9. Conclusion and Future [blog/lti/conclusion]
Question 1 Question 2 5. Knowledge Base [knowledge]
5.2. Glossary [knowledge/glossary]
5.3. FAQ [knowledge/faq]
这里列出了 MoonBit Community Blog 目前的维护团队 等待更多新成员的加入… 如果您希望加入 Community-Blog 的日常维护,请发邮件到 me@lampese.com。 6. Team [team]
6.1. Leaders [team/leaders]