编程语言与软件工程2016arxiv.org
Java 泛型是图灵完备的
Java Generics Are Turing Complete
进阶 · 约 60 分钟读完前置知识：Java 泛型、图灵机基础、子类型系统
导读
这篇论文研究 Java 泛型类型系统是否图灵完备，并通过在泛型类型声明和子类型关系中编码图灵机来论证它可以表达任意计算。其含义是 javac 的类型检查可能不终止，甚至可被构造成栈溢出或极慢。
HN 关注点：把抽象的类型系统理论与实际编译器行为联系起来：复杂泛型可让 javac 栈溢出或卡死，并引发对宏和语言设计的讨论。
HN 评论精选
这几条评论里：质疑 1 补充 1 亲历 2
亲历实际写出复杂泛型可让 javac 栈溢出或产生运行时类型错误。
在实践中，这意味着如果你写出这种嵌套泛型代码（原评论给出了示例），你可以让编译器：1. 输出奇怪的错误（循环一阵后因内部栈溢出停止）；2. 编译出会运行时报类型错误的代码。
chvid查看英文原文
In practice in means if you write stuff like this: interface Z {} interface N<x> {} interface L<x> {} interface Qlr<x> {} interface Qrl<x> {} interface E<x> extends Qlr<N<?super Qr<?super E<?super E<?super x>>>>>, Qrl<N<?super Ql<?super E<?super E<?super x>>>>> {} interface Ql<x> extends L<N<?super Ql<?super L<?super N<?super x>>>>>, E<Qlr<?super N<?super x>>> {} interface Qr<x> extends L<N<?super Qr<?super L<?super N<?super x>>>>>, E<Qrl<?super N<?super x>>> {} class Main { L<?super N<?super L<?super N<?super L<?super N<?super E<?super E<?super Z>>>>>>>> doit( Qr<? super E<? super E<? super Z>>> v ){ return v; } } You can make your compiler: 1. Bark out an odd error. (Loop for a while and then stop due to an internal stack overflow.) 2. Compile something that gives a runtime type error.
质疑图灵完备类型系统不如一等宏/AST 变换实用。
叮！事情总是这样。如果你想对代码做有用的变换，最终会逼近一个图灵完备系统。现在你有一个类型系统，可以用极其绕、极慢且丑陋的方式计算任何程序变换。要是语言一开始就提供合适的宏会好得多：一个真正用于 AST 操作的库，以及告诉编译器“在对代码做任何其他处理前应用这个变换”的方式，而不是在原语言内部再搞一个只有编译器用的解释型语言。人们不必学两套语法，编译也可能更快（我这里更多想到的是重度依赖模板的 C++ 库）。
Faint查看英文原文
DING! This is what always happens. If you want to get useful manipulations done to code you'll eventually creep up to a Turing complete system. Now you have a type system where you could calculate any program transformation, albeit in really really convoluted, slow and ugly way. It would have been SO much better to give the language proper macros to begin with. I mean, a library that's actually meant for doing AST manipulations, and a way to tell the compiler "apply this transformation to that code before doing anything else with it", instead of another compiler-only interpreted language inside the original language. People would not have to learn 2 different syntaxes, and compilation would probably be faster (well I'm thinking more of heavily templating dependant C++ libraries here).
亲历类似结论早由 Lex Spoon 在 GWT-RPC 泛型中证明，实际影响类型推断和代码生成可能需判定停机问题。
GWT 工程师、前 Scala 开发者 Lex Spoon 几年前在我们升级 GWT-RPC 泛型时证明了类似定理。GWT RPC 代码生成器必须推断方法返回类型，以及比如返回 List<Foo> 时哪些类可能被反序列化。Lex 展示了如何在 Java 泛型中构造皮亚诺算术，并把问题表述为：判断 RPC 调用可能返回哪些类型，等同于判定这些小定理/问题，因此 GWT 的 SerializationTypeOracleBuilder 类将不得不解决停机问题。这大概是错误的转述，也许 Lex 看到会补充，但原始讨论大概随着用 GWT 构建的 Wave 关闭而永远丢失了，很讽刺。
cromwellian查看英文原文
An GWT engineer and former Scala guy, Lex Spoon, proved a similar theorem several years ago when we were upgrading generics for GWT-RPC. The GWT RPC code generator has to reason about return types of methods and which classes could possibly be deserialized say if you return a List of Foo. Lex showed how to construct the peano arithmetic in Java generics and how to formulate problems such that solving the question of what types could be returned from An Rpc call with List would amount to deciding these small theorems or problems and therefore the GWT SerializationTypeOracleBuilder class would have to solve the halting theorem. That's probably a wrong paraphrasing and maybe lex will see this and chime in but I think the original discussion was lost forever ironically when Wave, which was built with GWT, was shut down.
补充提供论文中可运行的编码图灵机示例，默认栈溢出，增大栈后缓慢通过类型检查。
顺便，这是论文中一个 Java 泛型程序的 URL：https://gist.github.com/rgrig/b4cdaed3ed9a70dbdb6f158f14b57263 源码注释说：// 编码一个用二进制计数的图灵机，然后停机。// 默认会栈溢出。// 如果增大栈（javac -J-Xss100M Main.java），它能通过类型检查，但耗时很长。
cleeus查看英文原文
btw, here is the URL for a Java-Generics-Program from the paper: https://gist.github.com/rgrig/b4cdaed3ed9a70dbdb6f158f14b57263 comment from the source: // Encodes a Turing machine that counts in binary, and then halts. // Gives stack overflow by default. // If you increase the stack size (javac -J-Xss100M Main.java), // then it type-checks, but it takes a lot of time.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2016Hacker News 讨论帖112 分 · 101 评
同领域还值得读
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 分钟编辑精选