编程语言与软件工程2020arxiv.org
Featherweight Go
Featherweight Go
进阶 · 约 90 分钟读完前置知识:类型系统基础、Go 语言基础、Lambda calculus / Featherweight Java 风格形式化方法
导读
这篇论文提出 Featherweight Go,一个 Go 语言核心子集的形式化模型,用于严格证明 Go 的类型系统(尤其是结构化子类型与接口)的性质。作者计划后续扩展出覆盖更多特性(Bantamweight Go)和并发机制(Cruiserweight Go)的更大模型。
HN 关注点:论文与 Go 泛型设计密切相关,且由 Wadler 等知名学者撰写,HN 读者关注其对 Go 类型系统的形式化分析及泛型实现的前景。
后来怎么样
Featherweight Go 为 Go 泛型设计提供了形式化基础,作者团队随后将其扩展为覆盖完整 Go 泛型的模型,直接支撑了 Go 1.18(2022 年)正式引入泛型的设计论证。
HN 评论精选
这几条评论里:质疑 1 补充 2
提供作者报告的直播信息
Philip Wadler 将于 6 月 8 日就这篇论文做报告,直播地址见 chalmersfp.org 和对应的 YouTube 频道。
journeeman查看英文原文
There's an upcoming talk by Philip Wadler on this paper on June 8 - http://chalmersfp.org/ YouTube channel where the talk will be streamed live - https://www.youtube.com/channel/UCiGOzKde1rlvzEB7J73gvrQ
补充补充论文后续研究计划与命名
引用结论:Featherweight Go 只覆盖 Go 的极小子集,后续计划建模赋值、数组、切片、包等特性(Bantamweight Go),以及基于 goroutine 和消息传递的并发机制(Cruiserweight Go)。很喜欢这套命名!
ainar-g查看英文原文
From the conclusion: Featherweight Go is restricted to a tiny subset of Go. We plan a model of other important features such as assignments, arrays, slices, and packages, which we will dub Bantamweight Go; and a model of Go’s innovative concurrency mechanism based on “goroutines” and message passing, which we will dub Cruiserweight Go. Love the naming!
补充关注泛型对 Go 编译速度的影响
Go 仓库的一个分支上已有泛型实现。我最好奇的是大型项目大量使用泛型后的编译速度表现——Go 团队应该不会合并任何导致明显变慢的方案。TypeScript 编译慢但我不那么反感,是因为可以异步做类型检查并在热重载时剥离类型信息。
parhamn查看英文原文
There’s also a generics implementation on a branch of the go repo. I’m most curious how they perform on compilation speed assuming a big project makes decent use of generics. I doubt golang would merge anything that causes significant slowdown. And I don’t blame them, the only reason I don’t dread TypeScript dev given its slow compile times is you can typecheck async and strip the typing information for the hot reload.
质疑质疑论文关于 Go 独有结构化子类型的说法
论文称 Go 是主流类型化语言中唯一使用结构化子类型的,但 TypeScript 显然也是结构化子类型:任何恰好有 String() 方法的类都能传给接受 Stringer 接口的函数。是我理解有误,还是作者不认为 TypeScript 是主流类型化语言?
TheDong查看英文原文
> Whereas most programming languages use nominal subtyping, Go is unique among mainstream typed programming languages in using structural subtyping. I thought typescript also used structural subtyping? i.e. in typescript I can define: interface Stringer { String: () => string } function takesStringer(s: Stringer) {} And now I can call takesStringer with any class that happens to have a String() method. This seems to match structural subtyping in go. Am I missing some reason that this isn't structural subtyping as referred to in the paper? Do they mean to say that typescript isn't a "mainstream typed programming language"?
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2020Hacker News 讨论帖252 分 · 160 评
同领域还值得读
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 分钟编辑精选