编程与软件工程cl.cam.ac.uk
谈谈“类型”
Talking about “types”
2014 — 2019，它一次次回到首页
黑点是上首页（≥ 50 分）的那次投稿，空心点是没冲上去的投稿，点越大分数越高。
导读
剑桥大学研究者撰写的博文，冷静剖析了关于静态类型与动态类型的常见争论，指出“类型安全”与静态检查无关、类型系统并非规范与验证的一站式解决方案，并批评了社区中一些被神化的观念（如对 Curry-Howard 的过度推崇）。文章立场均衡、信息量大，被视为关于类型之争最有价值的文章之一。
为什么经久不衰：它跳出了“静态 vs 动态”的站队式争论，用严谨的技术分析澄清了长期被混淆的概念，多年后仍是讨论类型系统时值得引用的参考。
HN 评论精选
高度赞扬文章公允且专业，堪称类型之争的最佳读物
赞。这是我在任何地方读到的关于类型问题（静态和动态）最好的文章。它非常公允，承认了静态和动态语言各自的优点与局限，而且信息极其扎实。下次有人想给我寄一本 PFPL，我就把这篇文章发给他。
StefanKarpinski查看英文原文
Bravo. This is the best thing I've read anywhere about the general issue of types, both static and dynamic. It is even-handed, acknowledging the benefits and limitations of both static and dynamic languages, and incredibly well-informed. I now have something to send to the next person that threatens to send me a copy of PFPL.
反驳文章对 Curry-Howard 的批评：类型系统确实能模块化地表达活性与不可达性
文章的观点大多很有道理，但对结尾部分不敢苟同。说 Curry-Howard 是“恋物崇拜”？基于 Curry-Howard（配合全函数）恰恰能表达活性与不可达性：比如在 Coq 里给 HTTP 响应处理函数标注 HttpRequest -> HttpResponse 类型，我就知道它是活的，因为函数是全的；死代码路径也可以通过消除 False 的证明来去除。当然证明方式与全程序分析不同，但这正是人们喜欢类型系统的原因——可以模块化地思考程序，而不是一次性看全部。
vilhelm_s查看英文原文
Certainly very sensible points. But I take some issue with the bits towards the end: > Fetishising Curry-Howard Hey, I happen to find Curry-Howard sexy, you have no right to shame me! > To specify and check liveness or reachability, we need to represent programs as some kind of flow graph, where flows are very likely to span multiple functions and multiple modules. But no, this is exactly what basing systems on Curry-Howard (with terminating functions) buys you. If I give a HTTP response handler in Coq the type HttpRequest -> HttpResponse I know it is live, because the function is total. And similarly, dead code paths can be gotten rid of by eliminating a proof of False. So this lets you state liveness and unreachability. Of course, the proofs of those statements is very different from program-analysis-style systems. In a whole-program analysis, the analyser goes over the entire program, and at the end it says "well, I could not find anything calling this function, so I guess it's dead". In a Curry-Howard-style system, you need to look at the function and figure out when it should be called and what preconditions need to be true for it to work properly. But this is exactly why people like type systems, you can think about programs modularly rather than all at once.
为类型级与基级分离辩护：语言限制反而减轻了人的认知负担
这篇文章说了很多该说的话，但有一点我不同意：“没有正常人会主张把语言割裂成基级和类型级两个片段”。那我一定是疯子了。我更喜欢在没有变异、没有迭代的语言里写类型表达式。限制语言不仅帮助分析程序的计算机，也帮助编写程序的人类——记住“我不允许变异任何东西”比记住“我可以用变异，但以某种方式使用时编译器就无法静态确定类型，除非版本是 4.2.3 以上”要容易得多。
colanderman查看英文原文
This article says many things that need to be said, but I take issue with this: > No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments. Well, I must be insane then. I much prefer writing type expressions in a language free from, say, mutation and iteration. Restricting languages aids not only computers which analyze programs, but also humans which create programs. It's much easier to remember, say, "I'm not allowed to mutate anything, there's no syntax for it", than, "I can use mutation, but if I use it in such-and-such a way, then compiler won't be able to statically determine the type, unless I have version 4.2.3 or later".
静态类型的重要价值在于作为程序员的认知辅助工具，而非仅服务于编译器证明
我觉得这里的论证有点偏向“静态类型能为编译器做什么”，即如何帮助计算机构造形式证明。对我来说同样有价值的是静态类型如何帮助我思考和设计代码。类型信息时刻提醒“这个实体属于这组对象”，把我从工作记忆的持续负担中解放出来；具体的函数签名也文档化了这些实体上的变换。静态类型作为认知工具的这一面非常个人化，并非对每个人都一样。
fsloth查看英文原文
I think the argumentation here is a bit a skewed towards 'what static types can and cannot do for the compiler' - i.e. how they can help the computer in constructing formal proofs. For me another almost as valuable thing is how static types help me think about and design the code. The static type information is always there to remind "this entity belongs to this set of objects" which frees me from the cognitive burden of maintaining this constantly in my working memory. With specific static types the function signatures now document the tranforms defined for those entities . This aspect of static types as a cognitive tool is highly personal, and not same for everyone, unlike the language and the compiler, though.
引用 Rich Hickey：类型系统管不住外部世界，其价值在于保持内部模型的自洽
“静态类型有什么用”这个问题一直困扰着我，直到看到 Rich Hickey 的评论：“静态类型的程序和程序员对外部世界可以和其他程序一样正确，但类型系统与此无关。外部世界与前提之间的联系永远在任何类型系统的范围之外。”这正是我喜欢类型的原因：自洽性确保我不在自设的逻辑模型内犯错，它不帮我构建更好的模型，但模型建好后能帮我写出不破坏所选形式化不变量的程序。所以争论不该是静态还是动态更好，而应聚焦于哪些问题模式更适合哪种系统。
fsloth查看英文原文
This topic of "what are static types good for" continued to bug me because I could not formulate a concrete answer to myself. I found the following Reddit discussion http://www.reddit.com/r/programming/comments/lirke/simple_made_easy_by_rich_hickey_video/ Which had eventually the specific thing I was after in a comment by Rich Hickey which helped to nail the concept I was after "Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system." Which is precisely why I enjoy types: Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism. Which, I think tells exactly what static types are good for: For those sort of problems that benefit from having a formal specification. There are a lot of programs that have this quality. So the argumentation is a bit skewed off. It should not be about whether static or dynamic types are better but more focus on what are those identifiable problem patterns where a dynamic type system helps programmer create more value than a static one and vice versa.
批评文章“一切都是权衡”的中庸立场，认为强观点间的辩论更健康
整篇文章反映了一种我很不喜欢但如今很流行的信念：没有什么比别的更好，一切都是权衡，强烈的肯定性主张天生就是错的。我不买账。这等于默认一切都处在帕累托前沿上，极不可信——本质上是诉诸中庸和诉诸流行的混合体。有些东西就是比另一些好，强立场之间的强辩论，比把所有人拉回均值的人为社会力量更健康。
tikhonj查看英文原文
This whole article is a reflection of a belief that I really don't like but is all too common these days. It's the idea that nothing is better than anything else, everything is a trade-off and strong positive are inherently wrong. I don't buy it. It's a tacit assumption that, somehow, everything is on the Pareto frontier. Profoundly implausible. In the background, it's basically a hybrid appeal to moderation (all extreme positions are wrong) and popularity (if so many people are doing something, it can't be wrong). Never mind the fact that popularity is almost meaningless, driven by fashion more than anything, and that what's "extreme" is arbitrary and largely driven by popularity itself... This is how we get "worse is better"; this is how we get standards that are compromises ideal for nobody but still widely adopted because they're standard or because that seems like the thing to do or because that's what everyone else is doing or because " engineering". The worst part is that this all goes unsaid, assumed correct by default. Just the fact that we're having the discussion the article wants, and not this meta-discussion, implicitly elevates its premise! Some things are better than others. A strong debate between strong positions is healthier than an artificial social force reverting everyone back to mean. Now, all this is not to say the usual message about types is perfect. It could definitely be improved in many different ways. But not by muzzling, weakening or qualifying: not by most of the argument's suggestions. Especially ironic is the rhetorical techniques the author uses to argue against rhetoric. The one I personally find the most grating—beyond the ambient implication that everything is equal that I've just written about—is establishing cheap credibility by aligning himself with the camp he's arguing against. "I like X, but..." Or, in this case, "I use OCaml, but..." Then again, my pointing this out is probably ironic in the same way. Or is it?
逐条反驳文章结论：足够强的类型系统可以编码任意正确性属性
我强烈反对这篇文章的许多结论。“类型系统不能成为规范与验证的一站式解决方案”——错！任何正确性属性都可以编码进足够强大的类型系统里。“Curry-Howard 不推进关于如何有效写软件的论证”——荒谬，类型系统与证明系统之间的同构让我们造出了 Agda 和 Coq 这样的系统。想要在同一种语言里写规范和普通代码？Agda 就允许你用与值级代码相同的语言写类型级代码。至于 Hickey 的 transducers 例子，很多人已经成功给它标注类型了。
wyager查看英文原文
I emphatically reject the many of the conclusions of this article. >Let me say it simply. Type systems cannot be a one-stop solution for specification and verification. Wrong! Any correctness property can be encoded into a sufficiently powerful type system. Which brings me to... >Curry-Howard is an interesting mathematical equivalence, but it does not advance any argument about how to write software effectively. This is absurd, of course. The isomorphism between type systems and proof systems allows us to build lots of impressive systems like Agda and Coq. >No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments. That's actually quite a reasonable desire. >Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code. To the author, this seems to mean "therefore, we shouldn't have types!". In reality, a sufficiently flexible programming language allows you to write type-level code in the same language as value-level code. See Agda. >Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic. Lots of people have typed transducers just fine... http://blog.podsnap.com/ducers2.html http://conscientiousprogrammer.com/blog/2014/08/07/understanding-cloure-transducers-through-types/
历次讨论
同类还值得读
开源应用架构
The Architecture of Open Source Applications
《开源软件架构》（AOSA）是一本在线免费书，邀请知名开源项目的作者亲自剖析其内部设计，涵盖 SQLAlchemy、LLVM、Audacity、Apache、Bash 等系统。
编程与软件工程上首页 9 次 · 2011–2024aosabook.org编辑精选编程语言简史：简短、不完整且多半错误
A Brief, Incomplete, and Mostly Wrong History of Programming Languages
一篇以戏谑、故意不准确的方式回顾编程语言史的博客文章，用夸张轶事和讽刺定义串起 Lisp、C、C++、Java、JavaScript、PHP 等语言。
编程与软件工程上首页 8 次 · 2009–2021james-iry.blogspot.comSQLite 是如何测试的
How SQLite is tested
SQLite 官方文档页，系统介绍 SQLite 的测试体系：多种测试方法（TCL 测试、模糊测试、回归测试、静态分析等）和海量测试用例，展示了这个小型开源项目如何靠极致测试获得…
编程与软件工程上首页 8 次 · 2009–2025sqlite.org编辑精选高级编程语言（2009）
Advanced programming languages (2009)
Matt Might 的经典文章，按用途推荐“高级编程语言”：如果追求就业就选主流语言，如果追求表达力、学术研究或创业，则推荐 Haskell、OCaml、Scala 等函数式语…
编程与软件工程上首页 8 次 · 2009–2022matt.might.net我的 Forth 与栈机器经历
Yosefk - My history with Forth & stack machines
作者以亲身经历回顾了使用 Forth 语言和栈式机器的历程：既赞叹其简洁优雅、代码量小、可自举的优点，也坦率指出栈操作在实际编程中的痛苦，以及 Forth 社区文化中的问题。
编程与软件工程上首页 8 次 · 2010–2024yosefk.com编辑精选