“讨论室:学术” 上的话题

如何在计算机科学中应用类型论和范畴论?

14 个评论 • 2023 年 1 月 21 日 (六) 09:47 2023 年 1 月 21 日 (星期六)

14

由Ice1000做出的摘要

已经回答

Master (讨论贡献)

如题, 我好奇计算机学家为何要考虑类型论和范畴论, 它反映了计算机科学中何种对象的数学结构?

2023 年 1 月 19 日 (四) 02:35 2023 年 1 月 19 日 (星期四)

Ice1000 (讨论贡献)

这是个很好的问题. 首先, 计算机科学 (广义) 很难应用类型论和范畴论, 实际上是类型论的研究中有大量对范畴论的应用, 而类型论本身是编程语言理论的基础理论. 在我看来 (前面部分应该是成立的, 从现在开始是我的个人想法) , 类型论之于对编程语言学家来说有点类似集合论之于数学家: 大家都接受过相关的基础教育, 理解这些理论的重要性, 但该不了解领域的前沿研究. 数学家中也有专门研究集合论的人, 同样, 编程语言学家中也有研究类型论的人, 只是后者的比例相对高一些.

因此, 根据我的个人观点, 这个问题的题设不成立, 计算机科学家基本不考虑类型论和范畴论. 下面我说说我为什么关心类型论和范畴论.

2023 年 1 月 19 日 (四) 06:09 2023 年 1 月 19 日 (星期四)

Ice1000 (讨论贡献)

编程语言是非常常用的计算机工具, 这个是计算机科学家比较关心的, 并且编程语言对于程序员的思维影响非常深刻, 比如常年使用 Java 的人会认为子类型多态是天经地义的, 而长时间使用 Rust 的人脑子里会对程序进行线性逻辑式的建模, 长时间使用 typescript 的话会内化结构化类型的思想, 等等. 拥有这些不同的思想对程序员来说, 并不影响她们完成编程任务, 因此大部分程序员都对这些想法停留在「知道有这些概念, 但不深究, 也不感兴趣」的程度. 在我看来, 有这么多编程语言的原因, 就是不同的人对理想的编程方式有不同的看法, 而这些想法往往是互斥的. 如果你希望程序能随时中断执行、跨函数跳转, 这当然听起来没有问题, 但也有的人希望程序在每个函数结尾自动清理局部内存, 这两者就冲突了——跳出当前函数就没有办法进行内存清理了. 因此会有人互相看不惯, 就会不断地产生新的语言.

我最早写程序的时候, 就感受到了这一点, 因此想要探索这些思想的本质、想要自己设计出完美的编程语言 (实际上是不存在的) , 所以就接触到了编程语言理论的研究: 这个理论将编程语言抽象成各种语言特性的组合, 并重点研究具体的语言特性、语言特性之间的交互, 因此熟悉编程语言理论的人能准确判断「将什么样的语言特性组合起来是能工作的」, 并且设计出好用的编程语言. 我觉得这很酷, 但随后就接触到了类型论: 它不研究具体的语言特性了, 而是直接发明了更底层的代数结构, 并认为编程语言就是这个代数结构在计算机中的模拟. 这样的代数结构有很多, 比如广义代数理论、概括范畴、偏等关系等. 这样的建模方式有很多局限性, 但它却给理解编程语言的方式带来了全新的直觉, 比如将计算视为一种单子、将类型视为一个范畴里的对象等等. 这就是类型论研究者关心范畴论的地方.

除此之外, 现代的编程语言研究除了大规模的工程问题 (提升计算性能、支持更多架构等) 和怎么设计好用的语言特性 (全凭审美和感觉) 这两个发表论文比较看脸的方向之外, 就是类型论了, 我觉得后者对 career 来说比较靠谱. 我个人也对编程工具比较感兴趣, 但学术界并不 appreciate 这些, 所以就是 sidekick.

2023 年 1 月 19 日 (四) 06:33 2023 年 1 月 19 日 (星期四)

Master (讨论贡献)

计算视为单子具体指什么呢?

2023 年 1 月 19 日 (四) 07:21 2023 年 1 月 19 日 (星期四)

Ice1000 (讨论贡献)

令 Computed : Set → Set 作为一种标记计算的函数, 输入一个表达式的集合, 过滤掉里面那些会因为计算而变成其它东西的表达式, 比如 1 + 1 就会被删掉, 因为它运行后就是 2 了. 这里 Computed 就是一个 Monad. 不知道这么说能不能表达出它里面微妙的意思, 但大概就是过滤两遍和只过滤一遍效果是一样的, 而且 “把一个没化简的东西拿去化简” 本身是一个可重复而不可逆的过程, 这对应了单子的那两个自然变换

编辑: 经过后面的讨论, 这个说法是有问题的.

编辑于 2023 年 1 月 19 日 (四) 10:26 2023 年 1 月 19 日 (星期四)

Trebor (讨论贡献)

计算并不是值到值的映射 (如果是, 这称作纯计算) . 一次计算可能会产生异常, 生成随机数, 读取磁盘文件等. 单子这个数学结构可以刻画绝大部分计算的概念.

单子是一个自函子 $m : C \to C$ 上配备一些结构. $C$ 是所有类型的范畴, 态射是函数. $m (x)$ 表示一次计算, 产生类型 $x$ 的值. 单子配备了自然变换 $x \to m (x)$ , 表示不做任何计算直接返回输入.

$x \to m (y), y \to m (z)$ 表示两个输入值, 经过一些计算, 产生新的值的函数. 单子配备了一个运算将这两次计算连起来得到 $x \to m (z)$ , 满足自然性. 我们要求它们满足单位律和结合律.

编程语言里面可以直接提供一个单子 (类似公理, 看不到这个单子内部的定义) 与一些计算 $x \to m (y)$ , 让程序员使用. 程序员也可以自己定义单子, 如 $m (x) = 1 + x$ 表示可能失败的运算, 并上的这个点表示失败; $m_{s} (x) = s \to s \times x$ 表示带有一个状态的计算, 输入一个起始状态, 输出计算结果与结束状态, 等.