Torturing Rustc by Emulating HKTs
2 months ago
- #Type Systems
- #Rust
- #Functional Programming
- 作者尝试创建一门函数式编程脚本语言时，遇到了Rust缺乏高阶类型（HKTs）导致的问题。
- 高阶类型允许泛型本身拥有泛型，但Rust原生不支持此特性，开发者只能通过泛型关联类型（GATs）变通实现。
- 作者通过研究归纳与余归纳等数学概念，试图理解Rust特质求解器对递归类型的处理逻辑。
- 一个最小复现案例揭示了Rust特质推导中的归纳循环问题，该问题会触发编译器报错。
- 作者使用Lean 4形式化验证类型系统相关证明，实践了数学证明与编程的 Curry-Howard同构理论。
- Rust特质求解器采用归纳推理，无法处理无限证明树，而余归纳特质（如自动特质）可应对循环引用。
- 作者以幽默笔调调侃Rust的局限性及其复杂性，同时肯定这些探索对计算机科学教育的价值。