使用 Idris 的依赖类型简明导论
Gentle Introduction to Dependent Types with Idris
作者未知 · 初版 2018 年
- 2次提及
- 1人推荐
- 2位 HN 评论者
简介
Dependent types 是一种强大的概念，它使我们能够编写携带证明的代码。Idris 是一种支持 dependent types 的编程语言。我们将学习其数学基础，随后编写正确的软件并在数学上对其性质进行证明。本书旨在让没有高中以上数学背景的初学者也能轻松阅读，因此内容设计完全自成体系。本书第一部分介绍了 Idris 背后的理论，第二部分则结合实例对 Idris 进行了实操性介绍。
Hacker News 读者推荐
……上面列出的），去看看佩尔·马丁-洛夫的《直觉主义类型论》、罗朝晖的《计算与推理：计算机科学中的类型论》、埃德温·布雷迪的《Idris 类型驱动开发》、博罗·西特尼科夫斯基的《Idris 依值类型轻巧入门》、皮尔斯的《类型与程序设计语言》、罗伯特·哈珀的《程序设计语言实用基础》（或者他在 YouTube 上关于 Type Theory 的任何视频）、《The Little Typer》……
codeismath 在 HN 的推荐
找书
豆瓣 微信读书 京东 Open Library ISBN 1723139416
数据整理自 Hacker News 公开评论，数据来源 hackerbooks.org 与 Open Library。