小小 Typer

Hacker News 上怎么说

• auslegung · 2018 年

  《A Philosophy of Software Design》给我留下了很深的印象。《The Little Typer》（MIT 出版社）https://www.amazon.com/dp/0262536439/ref=cm_sw_r_cp_api_pXxS... 看起来也很有搞头

  I’ve been impressed with A Philosophy of Software Design. The Little Typer The Little Typer (The MIT Press) https://www.amazon.com/dp/0262536439/ref=cm_sw_r_cp_api_pXxS... looks promising

• isaac21259 · 2022 年

  Daniel P. Friedman 和 David Thrane Christiansen 写的《The Little Typer》。整本书基本上就是一长串层层递进的代码示例，用来展示依赖类型编程语言的语义。它启发了我去……

  The Little Typer by Daniel P. Friedman and David Thrane Christianse. It's basically one long book of examples building on each other to show the semantics of a dependently typed programming language. It inspired me to…

• codeismath · 2025 年

  ……Boro Sitnikovski 的《Type-Driven Development with Idris》、Pierce 的《Types and Programming Languages》、Robert Harper 的《Practical Foundations for Programming Languages》（或者他在 YouTube 上关于类型论的任何视频）、Friedman 和 Christiansen 的《The Little Typer》、David Corfield 的《Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy》（上周去北卡 OBX 海滩度假还带着这本打发时间！……

  …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" by Friedman and Christiansen "Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week!…

• mkw5053 · 2026 年

  ……还有两本关于如何证明程序正确性的极好且短小精悍的书（不过不是用 Lean）：1. https://mitpress.mit.edu/9780262527958/the-little-prover/ 2. https://mitpress.mit.edu/9780262536431/the-little-typer/。第二本书的合著者 David Thrane Christiansen 除了写了大量的教程和资料外，还写了《Functional Programming in Lean》（针对 Lean 4）。

  …are two more great, short books on proving things about your program (not with Lean, though): 1. https://mitpress.mit.edu/9780262527958/the-little-prover/ 2. https://mitpress.mit.edu/9780262536431/the-little-typer/ David Thrane Christiansen, co-author of the second, also wrote Functional Programming in Lean (Lean 4) among many other tutorials and things.

• ekidd · 2022 年

  这是“The Little <X>er”系列里我最喜欢的两本书之一。另一本是《The Reasoned Schemer》。《The Little Typer》带你入门了依赖类型（dependent types）。你可以用它来保证诸如“对长度为 X 的列表和长度为 Y 的列表调用 'concat'，一定会返回一个长度为 X+Y 的列表”。在某种程度上，还可以……

  This is one of my two favorite books in The Little <X>er series. The other is The Reasoned Schemer. The Little Typer provides an introduction to dependent types. These can by used to guarantee things like "applying 'concat' to a list of length X and list of length Y returns a list of X+Y". It is also possible, to some…

• juxtapose · 2022 年

  ……感兴趣的话，你可以看看 Lean [1]、Idris [2] 以及其他几个 [3,4]。这些语言的语法通常比较晦涩古怪，但也有一些项目采用了更常规的语法，比如 Cicada [5]。《The Little Typer》[6] 是关于这个主题非常不错的入门书。[1] https://leanprover.github.io [2] https://www.idris-lang.org [3] https://github.com/agda/agda [4] https://coq.inria.fr [5] https://cicada-lang.org [6]……

  …interested, you can take a look at Lean [1], Idris [2], and a few others [3,4]. Often these languages have esoteric syntax, but there are projects using a more conventional syntax, too, e.g. Cicada [5]. "The Little Typer" [6] is a pretty good introduction to this topic. [1] https://leanprover.github.io [2] https://www.idris-lang.org [3] https://github.com/agda/agda [4] https://coq.inria.fr [5] https://cicada-lang.org [6]…

正在加载完整评论……