Idris 类型驱动开发

Hacker News 上怎么说

• bjz_ · 2017 年

  《Type-Driven Development with Idris》：https://www.manning.com/books/type-driven-development-with-i...

  Type-Driven Development with Idris: https://www.manning.com/books/type-driven-development-with-i...

• lodi · 2017 年

  在读《Type-Driven Development with Idris》[0]之前，我一直觉得这种东西既晦涩又脱离实际，但这本书把基础的依赖类型示例——就像主楼帖子里演示的那些——讲得极其通俗易懂。事实证明，只要语言选对了，这玩意其实真没那么难……

  I always thought this kind of thing was abstruse and impractical until I read Type-Driven Development with Idris[0], which made basic dependent type examples--like those demonstrated in the posted article--completely straightforward. Turns out that this kind of thing isn't actually that hard with the right language…

• rq1 · 2020 年

  恰恰相反，我建议直接从 Idris 入手。这门语言的整体设计更好，也连贯得多。它修复了 Haskell 的很多“失误”。去看看 Edwin Brady 本人写的《Type-Driven Development with Idris》吧，这本书写得真心神。

  On the contrary, I’d recommend to start with Idris instead. The design of the language is globally better and way more coherent. It fixes a lot of Haskell “mistakes”. Check out “Type-Driven Development with Idris” by Edwin Brady himself. The book is truly amazing.

• ojnabieoot · 2020 年

  ……[1] 《Lectures on the Curry-Howard Isomorphism》[2] 是我最喜欢的（研究生级别）类型论和 lambda 演算入门书，内容涵盖了“lambda 立方体”和纯类型系统（PTS）。最后，虽然《Type-Driven Development With Idris》[3] 一点也不偏向“纯理论”，但它依然是学习依赖类型和“证明即程序（proof-as-program）”理念的极佳入门教程。这也是我读过的唯一一本专门针对某一门特定编程语言的书……

  …[1] Lectures on the Curry-Howard Isomorphism[2] is my favorite (graduate-level) introduction to type theory and the lambda calculus, including the “lambda cube” and pure type systems. Finally, while Type-Driven Development With Idris[3] is not at all “theoretical,” it is still an excellent introduction to dependent types and the idea of proof-as-program. It’s also the only book about a specific programming language I’ve ever read…

• edko · 2017 年

  《Type-driven development with Idris》（https://www.manning.com/books/type-driven-development-with-i...）。它彻底让我大开眼界，认识到了类型能做到何种地步。

  Type-driven development with Idris (https://www.manning.com/books/type-driven-development-with-i...). It was a real eye-opener of what types can do.

• icebraining · 2017 年

  要是那个值必须介于 0 和 1 之间呢？普通类型可没法帮你保证这一点。但其实利用依赖类型就可以做到 :) 我是个 Python 粉，但《Type-Driven Development with Idris》读起来真的趣味十足。

  what if that something must be between zero and one? A type can't tell you that. Actually, it can, using dependent types :) I'm a Python fan, but Type-Driven Development with Idris has been a very interesting read.

正在加载完整评论……