编程语言与软件工程2024arxiv.org
从第一性原理推导依赖类型面向对象编程
Deriving Dependently-Typed OOP from First Principles
专业 · 约 90 分钟读完前置知识：依赖类型论、Codata 与 copattern matching、面向对象设计模式
导读
论文试图从第一性原理出发，用依赖类型论推导/形式化面向对象编程。作者把“针对接口编程”对应到类型论中的 codata 与 copattern matching，并讨论其与 visitor pattern 等概念的关联。
HN 关注点：OOP 与 FP 的对偶和深层联系，以及把 OOP 本质归结为 codata/copattern matching 是否成立。
HN 评论精选
这几条评论里：质疑 1 补充 2
补充推荐一本以 Scheme 式风格讲 Java 的书，帮助理解 FP 与 OOP 的深层联系。
对我来说，最好用《A Little Java, A Few Patterns》来描述，论文也提到它与 visitor pattern 的联系。这本书写的 Java 很不实用，但方式很像 Scheme，能让人真正理解函数式与面向对象编程之间的深层联系。
_glass查看英文原文
For me best described in, and also as a topic mentioned in the paper about the visitor pattern connection, "A Little Java, A Few Patterns". This book writes really impractical Java, but in such a Scheme way, that you really can understand the deep connections between functional and object-oriented programming.
质疑质疑把 OOP 本质等同于 codata/copattern matching，认为 Stream 例子更偏函数式。
也许我只是没看懂，但我不认同他们在引言里采纳的定义。> 面向对象编程的本质是针对接口编程，这对应类型论中的 codata 和 copattern matching。然后他们用了经典的 codata 例子 Stream，有 head 和 tail。他们声明的 Stream 看起来更像函数式语言里的版本，而不是 OO 里的版本，不过这个概念显然两种范式都有。
abeppu查看英文原文
Maybe I'm just missing something, but I'm not on board with the definitions they take in the introduction. > the essence of object-oriented programming is programming against interfaces, which correspond to the type theoretic concept of codata and copattern matching They then use the classic codata example of a Stream, with a head and a tail. The Stream they declare looks a lot more like the version of that concept in functional languages than the version of it in an OO one, but clearly it exists in both paradigms. https://www.cs.cmu.edu/~15150/resources/libraries/stream.pdf https://hackage.haskell.org/package/Stream-0.4.7.2/docs/Data-Stream.html https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/stream/Stream.html
补充对“derive a programming paradigm”的具体含义感到好奇。
很有意思，我好奇“推导出一个编程范式”到底意味着什么。
grafs50查看英文原文
Interesting, I wondered what it would even mean to derive a programming paradigm.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2024Hacker News 讨论帖172 分 · 18 评
同领域还值得读
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 分钟编辑精选