面向计算机爱好者的泛代数入门教程
原文标题:Algebra 作者:Oleg Kiselyov 原文链接:Algebra 代数式副作用(algebraic effects)和代数数据类型(algebraic data type)中的「代数」究竟是什么?哪些模块/对象的签名是「代数」的?「代数」到底是什么?自由代数(free algebra)的「自由」在哪里?初始代数(initial algebra)是什么,它有什么用,我们如何证明一个代数具有「初始性」?我们能准确地描述 tagless-final 式 DSL 嵌入,及其解释器的正确性吗?如果能描述,如何证明这种正确性? 本文以讲义的形式展示了一些泛代数(Universal Algebra)领域的标准入门材料,旨在解答这一类问题。不过,这些材料是专门为程序员,尤其是那些对 tagless-final 方法感兴趣的程序员所挑选和安排的。我们只使用编程中遇到的例子,并尽可能使用具体的编程语言中的符号,而非数学符号。 导言 什么是代数(Algebra)?Garet Birkhoff 被现在的人们誉为「泛代数」领域的创始人,他是这么说的: By an `abstract algebra’ is meant, loosely speaking, any system of elements and operations such as a ring, a field, a group, or a Boolean algebra. 译:「抽象代数」泛指那些由元素和运算组成的系统:如环、域、群和布尔代数。(Birkhoff,1935) 随后,他又提出了一个「临时用的形式定义」,这一定义现在仍被人们使用(稍后会回顾这些形式定义)。 泛代数是数学的一个领域——关于泛代数的课程和教科书的很大一部分内容是格论(Lattice theory)和组合数学(Combinatorics)。看起来,这似乎与常见的编程任务没有太大联系。但世事无常,造化弄人,自动机(Automata)理论(有限状态机、Kleene 代数、正则表达式)是代数在计算机科学的最早应用之一。根据 Gougen 等人(1977)的说法:Burstall 和 Landin 共著的《Programs and their proofs: An algbraic approach》(1969)首次在编程语言语义学研究中使用了泛代数和(隐含的)代数初始性。F. L. Morris(《Correctness of translations of programming languages》斯坦福大学博士论文,1972 年)则引入了编程语言中最为常见的多类别代数。而在计算机科学中全面引入代数和范畴论技术,应归功于 ADJ 四人帮(J....