编程语言与软件工程2019microsoft.com
Haskell 中的高阶类型级编程
Higher-Order Type-Level Programming in Haskell
专业 · 约 90 分钟读完前置知识：Haskell 类型系统、类型族与类型级编程、GHC 扩展机制
导读
这篇论文研究 Haskell 中类型级编程的局限性：现有类型族在处理高阶类型级函数时存在“可匹配性”问题，导致许多类型级计算难以表达。作者提出扩展 Haskell 类型系统以支持高阶类型级编程，并声称在不破坏向后兼容的前提下可显著提升相关计算的处理能力。
HN 关注点：Haskell 社区长期受类型级编程的繁琐所苦，论文由 SPJ 等人提出，被视为简化 singletons 库、实现类型级归纳证明的重要一步。
HN 评论精选
这几条评论里：质疑 1 补充 1 亲历 1
亲历亲历者认为该工作解决了实际痛点，可简化 singletons 库并支持类型级归纳证明
我认为这是让 Haskell 类型级编程更愉悦的重要一步。我最近做了一个重度依赖类型级的 side project，可匹配性确实是真实痛点。这可能会极大简化整个 singletons 库，还能让人完全在类型层通过归纳进行证明。
LeanderK查看英文原文
I think it's a major step towards more pleasant type-level programming in haskell. I recently worked on a very type-level heavy side-project and the matchability is a real issue. I think this could drastically simplify the whole singletons-library and would also enable proving stuff via induction entirly in the type-level.
补充好奇该形式化方法能否用于解决 TypeScript 中高阶函数的类型难题
不知道这套形式化方法能否应用到 TypeScript。我偶尔会遇到像 flatten 这类高阶函数的棘手类型问题，这可能有帮助。
mpoteat查看英文原文
I wonder if this formalism can be applied to Typescript. I occasionally come across tricky typing problems with higher order functions like "flatten" that this might be helpful for.
质疑外行读者肯定其价值但质疑记号可读性，并指出难以独立验证 SPJ 的工作
这里十个概念我只能理解一个。但感觉它在说有用的东西，且有形式化证明的质感——如果正确，意义很大：他们开篇就提到在不破坏向后兼容的情况下能大幅提升输入处理速度。文中有“名人说了所以就是对的”的意味，因为很难反驳 SPJ。我完全没资格质疑其逻辑，但如果有反驳，应该由有能力的人提出。另外记法上，我怀疑 ASCII 版本的可读性，他们依赖形式逻辑排版才能打出 ->> 符号。我不喜欢 ::=、:=、->、->> 这类新映射带来的风险，在类型系统里我总迫切想找到内心那个把符号念成连贯语句的“声音”。“is”和“maybe”是很好用的词，那 ->> 该怎么念才能清楚表达它的含义？
ggm查看英文原文
I understood about one concept in 10 here. Not all of the and and but were understood btw. But, that said, it feels like this is saying something useful, and has a formal proof quality which if correct, has a really strong indication of a useful thing: They say up front that noting issues in backwards compatibility this can make a very big difference to the speed of processing inputs. There is "famous person said so, so it must be true" in this because its hard to contradict SPJ. I don't think I'm even in the corridor, let alone the room of people who could question the logic, but I think the rebuttal needs to be said by somebody who could, if there is one. Notationally I struggle to see how well people could "read" the ascii version of this because they depended on formal logic typography to make the ->> symbol. I don't like ::= and := and -> and ->> risks which are inherent in new mappings into a language, and in type systems I find myself desperately searching for the "said voice" internally which speaks the symbols as a cogent language statement. "is" is such a useful word. "maybe" is such a useful word. "x is an Integer" and "x maybe is an Integer" are easy to understand. How would I "say" ->> to be clear its meaning against is and maybe?
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2019Hacker News 讨论帖155 分 · 17 评
同领域还值得读
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 分钟编辑精选