最新

大家好。在过去两年里，我作为一名开发者，利用业余时间拓展了我的知识边界。虽然我本人并非数学家，但我发现用数学语言形式化概念，对于改进对这些概念本身的符号推理仍然很有用。我利用了书籍和人工智能，并主要以批判的眼光关注着后者（AI）的发展。我有一些正在进行的项目，从其中一些项目的观察和探索中，我开始思考当前推理、逻辑和数学本身的极限在哪里。因此，我探索了范畴论和拓扑，尤其是在 Mazzola 的音乐理论基础上。我思考这是否会影响编程中的类型论，并进行了一些实验。由此诞生了这门编程语言 Yon，其灵感来源于 Yoneda 引理和态射。从另一个项目我观察到了 Leech 格子；从另一个项目，我进行了一些关于 mmap 和基于坐标分配的实验，这种结构在拓扑学意义上具有优势。 这门语言当然存在一些错误，文档也是仓促写就的；整个工作耗时 3 周。为了性能，它被编译到 LLVM，目前我更倾向于避免使用虚拟机和垃圾回收器。它包含一些不寻常但性能出色的数据结构。它值得一看，我希望它能吸引一些用户，并有人愿意帮助我一起开发。我希望它能为编程带来新的刺激，并可能开辟一些新的前沿。 一些具体细节，供有兴趣深入了解的人参考。编译器是一个真正的流水线，而不是解释器：OCaml 前端将 .yon 源代码转换为我称为“topos”的自定义 MLIR 方言，其中范畴结构作为一等操作存在；其降低（lowering）过程将一切转换为 LLVM IR，然后生成原生可执行文件。一个简单的命令 `yonc` 驱动整个链条，你可以随时停止在任何中间阶段，查看范畴结构在通往硅片的过程中实际变成了什么。 运行时是 Leech 格子观察结果的归宿。堆（heap）是基于 Λ₂₄ 的内容寻址：每个值都被映射到一个格子点，并在 Conway 群 Co₀（通过 libmmgroup）下进行规范化，因此相同的内容始终位于相同的地址。这带来了三个我现在难以割舍的好处：无论值有多大，相等性比较都只需一次机器比较（字符串相等性测试在 32,768 个字符的字符串上也能达到约 17 纳秒，因为它比较的是句柄，而不是字节）；去重是全局且自动的，用户代码中没有内部化（interning）逻辑；并且放弃 GC 不再是一种妥协，因为单元是不可变的且内容寻址的，所以无需跟踪也无需移动。 并发我故意保持了简单：没有线程，没有共享可变状态。程序被分割成隔离的“空间”（Spaces）（独立的进程，由 MMU 强制隔离），它们通过具有明确失败语义的共享内存通道进行通信。 关于哪些是经过验证的，哪些只是希望：基本事实是一个包含 112 个示例的回归测试套件，以及一个跨空间场景测试套件，在 Linux x86-64 和 macOS Apple Silicon 上（Intel Mac 未测试）具有相同的退出码。网站上的书，共 21 章加上附录，在写下之前，每个代码片段都经过了编译和运行。基准测试附录声明了其环境和方法；我尽量不发布任何没有这些信息的数字。1.0 版本的一些限制也已写下，在一个基础文档中列出了所有固定的池（每个链 256 个堆，64 个空间，16 个并发 RPC 会话，等等），其原理是明确失败的硬限制是规范，而静默退化的软限制是 bug。 关于许可，我采用了 GCC 的模式：编译器和工具链是 AGPLv3，运行时是 AGPLv3 并带有明确的链接例外，因此语言本身保持自由，而你用它编写的程序完全属于你，可以采用任何你选择的许可。 网站+书籍：https://yon-lang.org 代码库：https://github.com/yon-language/yon (tag v1.0.0) 很乐意回答任何问题：关于 topos 方言，为什么选择格子而不是哈希表，范畴结构如何降低，以及过程中有哪些地方出了问题。