编程语言与软件工程2015homepages.inf.ed.ac.uk编辑精选
命题即类型（Propositions as Types）
Propositions as Types (2014)
进阶 · 约 75 分钟读完前置知识：命题逻辑、λ演算、函数式编程基础
导读
这是 Philip Wadler 的综述文章《Propositions as Types》，系统梳理了逻辑学中的「命题」与计算中的「类型」之间的对应关系（即 Curry–Howard 对应）：一个命题对应一个类型，一个证明对应一个程序，证明的化简对应程序的求值。文章兼具历史考证与概念讲解，指出这一思想在逻辑学与计算机科学中被多次独立发现，并讨论其意义与影响。
HN 关注点：这篇经典综述把「证明即程序」这一深刻对应讲得清楚易懂，并由此更深入理解类型系统在编程语言中的作用。
HN 评论精选
这几条评论里：补充 1 亲历 1
补充推荐 Wadler 同主题的 Strange Loop 演讲作为论文的通俗替代。
如果你觉得这篇论文太密集难读，Philip 今年在 Strange Loop 上就同一主题做了一场非常有趣的演讲：https://www.youtube.com/watch?v=IOiZatlZtGU
chrislloyd查看英文原文
If you're finding the paper too dense, Philip gave a extremely entertaining talk on the same subject at Strange Loop this year: https://www.youtube.com/watch?v=IOiZatlZtGU
亲历亲历：这篇论文帮助读者理解 PureScript 中 type class 等类型系统概念。
昨晚有人向我推荐了这篇论文，起因是我说自己没能完全理解 PureScript 书里 6.9 节（关于 nullary type class）的内容。它确实让我对类型系统的本质和作用有了更深的理解。
michaelsbradley查看英文原文
This paper was recommended to me yesterday evening, when I expressed difficulty in fully understanding section 6.9 in the PureScript book: https://leanpub.com/purescript/read#leanpub-auto-nullary-type-classes It's certainly opening my eyes to a deeper understanding of the nature and role of the type system.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
- 视频与演讲
历次讨论
- 2015Hacker News 讨论帖43 分 · 6 评
- 2025Hacker News 讨论帖108 分 · 75 评
同领域还值得读
Google 的软件工程（2017）
Software Engineering at Google (2017)
介绍了 Google 的软件工程实践，包括其单一代码库（monorepo）、几乎全部开发在主干进行而非分支、代码审查、构建系统 Blaze、协议缓冲区等工具与流程，并讨论了频繁重…
编程语言与软件工程2017 · 1,127 分 · 465 评 · 引用 15入门 · 约 45 分钟编辑精选Peter Naur：编程作为理论构建 (1985)
Peter Naur – Programming as Theory Building (1985)
Peter Naur 1985 年的经典论文《Programming as Theory Building》提出：编程的本质不是写代码或文档，而是在程序员头脑中构建对程序及其运行…
编程语言与软件工程2016 · 629 分 · 74 评入门 · 约 45 分钟编辑精选SciPy 1.0：Python 科学计算的基础算法
SciPy 1.0: fundamental algorithms for scientific computing in Python
这篇发表于 Nature Methods 的论文介绍了 SciPy 1.0——Python 科学计算生态的基石库，涵盖其核心算法模块（优化、积分、插值、线性代数等）、软件架构与社…
编程语言与软件工程2020 · 387 分 · 98 评入门 · 约 45 分钟编辑精选Lisp 的历史（1979）
History of Lisp (1979)
这是 Lisp 发明者 John McCarthy 于 1979 年为 HOPL（编程语言史）会议撰写的回顾文章，讲述 Lisp 的起源、设计动机与早期演进，文中也涉及 if 表…
编程语言与软件工程2018 · 352 分 · 44 评入门 · 约 45 分钟编辑精选使用 NumPy 进行数组编程
Array Programming with NumPy
这篇 Nature 文章介绍 NumPy 的数组编程模型及其在科学计算中的核心作用：以 ndarray 为中心，通过向量化操作让 Python 高效处理多维数组。
编程语言与软件工程2020 · 318 分 · 134 评入门 · 约 40 分钟编辑精选