编程语言与软件工程2022arxiv.org
Python 类型提示是图灵完备的
Python type hints are Turing complete
进阶 · 约 30 分钟读完前置知识：Python 类型注解、子类型关系与类型系统基础、可计算性/λ 演算基础
导读
这篇论文讨论 Python 的类型提示（type hints）体系在表达力上是否达到图灵完备。作者论证：借助注解与类型构造，可以在类型层面编码任意计算，因此像 mypy 这样的静态类型检查在一般情况下既无法保证终止，也无法完全判定。
HN 关注点：一门动态语言的类型标注居然能编码任意计算，这对静态类型检查工具意味着什么；讨论还延伸到“注解本质上只是运行期元数据”。
HN 评论精选
这几条评论里：质疑 1 补充 3
补充注解是任意合法 Python 表达式、运行期即元数据，所以图灵完备性并不令人意外。
先不谈类型系统本身，注解（annotations）本来就是独立存在的，在 Python 里不绑定任何行为，只是承载元数据。Python 3 引入注解时并没有为其确定用途，而是一次实验，看社区会拿它做什么，而不是由核心开发者按自己的判断强加一个用例。为此，注解允许写成任何合法的 Python 表达式。如今类型提示赢了：注解被广泛用于给 Python 加静态类型检查，但语言处理注解的方式除了变成惰性求值外没太大变化。mypy 虽然无法理解注解里的动态 Python 表达式，但这些仍是合法语法，运行时会产生正确的元数据。因此，就算类型系统不是图灵完备的，注解本身按其性质（基本等同于 exec()）也早已是图灵完备的。
BiteCode_dev查看英文原文
Even before talking about the typing system itself, annotations existed by themselves and are not attached to any behavior in Python: they simply hold metadata. When Python 3 came out, annotations were indeed added to the language, but no use case was decided for them. It was an experiment to see what the community would do with them instead of forcing a use case base on what the core devs would think would be useful. In order to allow this, annotations where permitted to be any legal python expression. Nowadays, type hints have won: annotations are widely used to add static type checking in Python. But the way the language treat them have not changed much appart from becomming lazy. While mypy cannot understand dynamic Python expressions in them, those are nevertheless legal syntax, and will result in correct metadata at runtime. Therefore, were the typing system not turing complete, the annotations would have been anyway by nature of being basically an exec().
质疑指出论文第一页子类型关系符号疑似写错，应为 object ≮: str。
我可能理解有误，但第一页似乎有个错误：文中写“每个字符串都是对象，str <: object，但并非每个对象都是字符串，str ≮: object”。可是 str <: object ∧ str ≮: object 不就是自相矛盾吗？表示“并非每个对象都是字符串”的正确写法不应该是 object ≮: str 吗？
vngzs查看英文原文
I may be misunderstanding this, but it seems like there is a mistake on the first page: > For example, every string is an object, `str <: object`, but not every object is a string, `str ≮: object`. Is not str <: object ∧ str ≮: object a contradiction? Wouldn't `object ≮: string` be the correct representation of "not every object is a string"?
补充认为类型系统走向图灵完备几乎是普遍规律。
我曾半开玩笑地发过一条推文，但其实是半认真的：类型最终总是会变成图灵完备的。
titzer查看英文原文
I tongue-in-cheek tweeted this, but I was semi-serious. Types end up being Turing-complete all the time: https://twitter.com/TitzerBL/status/1567677824105947136
补充补充 ar5iv 的 HTML 阅读链接，并吐槽 arXiv 不提供该入口。
这里是渲染成 HTML 的版本：https://ar5iv.labs.arxiv.org/html/2208.14755 （把 arxiv.org 里的 x 换成 5 就能到）。我觉得它在多数情况下都足够好用，arXiv 什么时候才会从文章页面直接链接过去？
w-m查看英文原文
Here's the article rendered as html: https://ar5iv.labs.arxiv.org/html/2208.14755 (Replace the x in arxiv.org with a 5 to get there. I feel like it's working well enough in most cases, when will they start linking these from the actual arxiv article pages?)
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2022Hacker News 讨论帖246 分 · 135 评
同领域还值得读
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 分钟编辑精选