Lean 函数式编程
作者：David Thrane Christiansen
版权所有：Microsoft Corporation 2023
这是一本免费的书，介绍了如何将 Lean 4 作为编程语言使用。本书中所有代码示例均经过了 Lean 4 版本 4.1.0 验证。
发行历史
2024 年 1 月
这是一个次要的 bug 修复版本，修复了示例程序中一个回退问题。
2023 年 10 月
在首次维护版本中，修复了许多较小的错误，并根据 Lean 的最新版本更新了文本。
2023 年 5 月
本书现已完成！与 4 月份的预发布版本相比，许多小细节得到了改进，并修复了一些小错误。
2023 年 4 月
此版本添加了关于使用策略编写证明的插曲，以及添加了将性能和成本模型的讨论，与停机证明和程序等价性证明相结合的最后一章。这是最终版本前的最后一个版本。
2023 年 3 月
此版本添加了关于使用依值类型和索引族编程的章节。
2023 年 1 月
此版本添加了关于单子变换器的章节，其中包括对 do-记法中可用的命令式特性的描述。
2022 年 12 月
此版本添加了关于应用函子的章节，此外还更加详细地描述了结构和类型类。此外改进了对单子的描述。由于冬季假期，2022 年 12 月版本被推迟到 2023 年 1 月。
2022 年 11 月
此版本添加了关于使用单子编程的章节。此外，强制转换一节中使用 JSON 的示例已更新为包含完整代码。
2022 年 10 月
此版本完成了类型类的章节。此外，在类型类章节之前添加了一个简短的插曲，介绍了命题、证明和策略，因为简单了解一下这些概念有助于理解一些标准库中的类型类。
2022 年 9 月
此版本添加了一个关于类型类的章节的前半部分，这是 Lean 的运算符重载机制，也是组织代码和构建函数库的重要手段。此外，还更新了第二章以适应 Lean 中 Stream 流 API 的变化。
2022 年 8 月
第三次公开发布增加了第二章，其中描述了编译和运行程序以及 Lean 的副作用模型。
2022 年 7 月
第二次公开发布，完成了第一章。
2022 年 6 月
这是第一次公开发布，包括引言和第一章的一部分。
关于作者
David Thrane Christiansen 已使用函数式语言二十年，并使用依值类型十年。他与 Daniel P. Friedman 合著了《The Little Typer》，介绍了依值类型论的关键思想。他拥有哥本哈根 IT 大学的博士学位。在学习期间，他为 Idris 语言的第一个版本做出了重大贡献。离开学术界后，他曾在俄勒冈州波特兰的 Galois 和丹麦哥本哈根的 Deon Digital 担任软件开发人员，并担任 Haskell 基金会执行董事。在撰写本文时，他受雇于 Lean 专注研究组织，全职从事 Lean 的工作。"
授权许可
本作品采用知识共享-署名 4.0 国际许可协议授权。