编程语言与软件工程2017cl.cam.ac.uk编辑精选
代数子类型（2016）
Algebraic Subtyping (2016)
专业 · 约 180 分钟读完前置知识：类型系统基础、λ演算、格与序理论
导读
这篇论文是 Stephen Dolan 的博士论文，研究编程语言中的子类型推断，提出用代数方法来刻画子类型关系（即“代数子类型”），并强调子类型与程序数据流之间的联系。评论者认为其问题表述新颖，可能对 TypeScript、Scala 等语言的类型系统设计有应用价值。
HN 关注点：类型系统理论如何落地到语言设计，讨论焦点包括它与 Scala/DOT 类型系统的比较、非面向对象场景下的子类型推断，以及“代数先于语法”的方法论。
后来怎么样
提出了代数子类型与 MLsub，成为后续子类型推断研究的重要基础，并启发了《The Simple Essence of Algebraic Subtyping》等后续工作；但尚未成为主流语言类型系统的通用标准。
HN 评论精选
这几条评论里：支持 2 补充 2
支持期待与 Odersky 的 DOT/Scala 类型系统作比较，并看好其在 TypeScript/Scala 的应用。
只粗略浏览引言，这看起来是非常令人兴奋的工作。用数据流来表述问题对我来说很新颖。令我惊讶的是，我在论文中找不到任何对 Martin Odersky 的引用；他多年在 EPFL 的工作一直致力于在健全类型系统下统一函数式与面向对象编程，这项工作的产物是 Scala。最近他用一种叫 DOT（依赖对象类型演算）的系统重构了 Scala 的基础。我在论文中似乎也没找到相关引用。很难想象作者不知道这项工作，但我非常想听到更多关于两种方法如何比较的讨论。总之，我想这项工作可能对 TypeScript 甚至 Scala 有很好的应用。
acjohnson55查看英文原文
From just skimming the intro, this seems like very exciting work. And the formulation of the problem in terms of data flow was really novel to me. I was surprised that I couldn't find any references to Martin Odersky in the paper, whose work for years at EPFL has been focused on unifying functional and object oriented programming under a sound type system. This work produced the Scala programming language. More recently, he reworked the foundations of Scala using a system he developed called the calculus of dependent object types (DOT) [1]. I couldn't seem to find any references to this in the thesis. It's hard to imagine the author was unaware of this work, but I'm really interested in hearing more about how the two approaches compare. Anyway, I'm imagining this work could have great applications for things like TypeScript, and maybe even Scala. [1] http://scala-lang.org/blog/2016/02/03/essence-of-scala.html
支持非面向对象的例子说明子类型推断与数据流相关，且论文对非专业读者友好。
我目前只读了引言——但它已经教会了我一些东西。作为外行，我觉得它非常易读、易懂。我一直以为子类型推断只是面向对象风格语言才需要的东西。但他一开始就给了两个非常清晰、非面向对象的动机例子和一个关键洞察：不支持子类型会忽略程序的数据流。
Patient0查看英文原文
I've only read the introduction so far - but already it has taught me something. As a lay-person I am finding it very readable and accessible. I'd always thought that subtyping inference was only something you need for OO style languages. But he begins with two very clear, non-OO, motivating examples and a key insight: failing to support subtyping ignores the data flow of the program.
补充赞赏“代数先于语法”的方法论，并补充 LtU 讨论链接。
“代数先于语法”这一教训我以前见过，很高兴看到它在这里带来如此大的收益。LtU 上也有讨论：http://lambda-the-ultimate.org/node/5393
ezyang查看英文原文
The lesson of "algebra before syntax" is one that I have seen before, and it is very gratifying to see it pay off such dividends here. There is also discussion on LtU here: http://lambda-the-ultimate.org/node/5393
补充补充作者另一篇论文，并欣赏其论文中的幽默脚注。
同样出自 Stephen（此前 HN 也讨论过）：https://www.cl.cam.ac.uk/~sd601/papers/mov.pdf。和往常一样，他恰如其分地加入幽默。例如他论文中的脚注：“本文已绝版，为俄文，且很难获得，因此感兴趣的读者可参阅 Conway 的一个更短证明 [Con71, p. 105]，它也只是绝版而已。”
rjtobin查看英文原文
Also by Stephen (and previously discussed on HN): https://www.cl.cam.ac.uk/~sd601/papers/mov.pdf As usual, he injects just the right amount of humour. Eg. this footnote in his thesis: "*This paper is out of print, in Russian, and quite difficult to get a hold of, so the interested reader is directed to a shorter proof by Conway [Con71, p. 105], which is merely out of print."
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2017Hacker News 讨论帖252 分 · 58 评
同领域还值得读
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 分钟编辑精选