使用 Idris 的依赖类型简明导论
Gentle Introduction to Dependent Types with Idris
作者未知 · 初版 2018 年
1人推荐
2位读者提及
2次提及
Dependent types 是一种强大的概念，它使我们能够编写携带证明的代码。Idris 是一种支持 dependent types 的编程语言。我们将学习其数学基础，随后编写正确的软件并在数学上对其性质进行证明。本书旨在让没有高中以上数学背景的初学者也能轻松阅读，因此内容设计完全自成体系。本书第一部分介绍了 Idris 背后的理论，第二部分则结合实例对 Idris 进行了实操性介绍。
Hacker News 上怎么说
正在加载完整评论……
……上面列出的），去看看佩尔·马丁-洛夫的《直觉主义类型论》、罗朝晖的《计算与推理：计算机科学中的类型论》、埃德温·布雷迪的《Idris 类型驱动开发》、博罗·西特尼科夫斯基的《Idris 依值类型轻巧入门》、皮尔斯的《类型与程序设计语言》、罗伯特·哈珀的《程序设计语言实用基础》（或者他在 YouTube 上关于 Type Theory 的任何视频）、《The Little Typer》……
…above), check out "Intuitionistic Type Theory" by Per Martin-Lof "Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo "Type-Driven Development with Idris" by Edwin Brady "Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski "Types and Programming Languages" by Pierce "Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory) "The Little Typer"…
对我个人而言，最大的门槛是缺乏一份带有大量实例的靠谱入门指南。我正试图通过我即将出版的书来稍微打破这个门槛：《Idris 依值类型轻巧入门》。我对这个领域非常感兴趣，但新手如果不深挖的话根本摸不着门道。《Logical Foundations》还不错，但我还是觉得缺少了理论层面的解释（“为什么……”
To me, personally, the biggest barrier was lack of a proper introduction with a lot of examples. I try to break this barrier a bit with my upcoming book: Gentle Introduction to Dependent Types with Idris. I am very interested in this area but it is impossible for newcomers to get a grasp of it without too much digging. Logical Foundations was OK but I was still missing the theoretical explanation ("why…