算法与计算机科学codewords.recurse.com编辑精选
代数数据类型的代数与微积分
The algebra and calculus of algebraic data types
2015 — 2024，它一次次回到首页
黑点是上首页（≥ 50 分）的那次投稿，空心点是没冲上去的投稿，点越大分数越高。
导读
这篇文章解释代数数据类型（和类型、积类型、函数类型以及递归类型）如何对应代数运算：用类型方程来计数取值个数，并用微积分中的导数来理解“单孔上下文”/zipper。它把 Either、pair、函数和递归类型放进同一套代数/微积分直觉里，是函数式编程里经典的类比文章。
为什么经久不衰：它把抽象的范畴论/类型论直觉压缩成一组可计算的方程，既能解释类型计数，也直接通向 zipper 等实用结构，所以多年后仍常被拿来推荐。
HN 评论精选
生成函数把类型方程变成计数序列，说明 ADT 代数与组合计数相通。
这和生成函数技巧密切相关：把序列元素当作幂级数系数，移位就相当于乘 x。把这个想法搬到代数数据类型上，F(x)=x+xF(x)+x²F(x) 对应 data FibTree a = Leaf a | Pair a (FibTree a) | Triple a a (FibTree a)，含 n 个 a 的 FibTree 个数正好是第 n 个 Fibonacci 数。另一个例子 data Tree = Leaf | Pair Tree Tree 满足 T=1+T²。
gjm11查看英文原文
A few remarks on this stuff. 1. Very closely related is the pure-mathematical technique of generating functions, where you take a sequence (let's say the Fibonacci sequence 0,1,1,2,3,5,8,13,...) and use its elements as coefficients in a power series (0+1x+1x^2+2x^3+3x^4+5x^5+8x^6+13x^7+...) and then notice that (e.g.) shifting the sequence by 1 is the same as multiplying by x, so if F is the series for (f(n)) then x.F is the series for (f(n-1)) and x^2.F is the series for (f(n-2)) apart from some corrections for very small n, which gets you F=(x+x^2)F+x or F = x/(1-x-x^2), and now you can factorize that quadratic and write F in the form p/(1-ax)+q/(1-bx) which immediately gets you an explicit formula for the Fibonacci numbers (the one with all the sqrt(5)s in it). So let's translate this into algebraic data types. We get F(x) = x + x F(x) + x^2 F(x) data FibTree a = Leaf a | Pair a (FibTree a) | Triple a a (FibTree a) and the number of FibTrees with n "a"s in is exactly the nth Fibonacci number. (There is a theoretically important data structure called a Fibonacci heap, but I don't believe there is any connection between these and these "Fibonacci trees" other than that in both cases there is something you can count with Fibonacci numbers.) 2. Suppose you consider a rather boring binary-tree type like this: data Tree = Leaf | Pair Tree Tree whose corresponding identity is T = 1+T^2, or T^2-T+1=0. If you're a mathematician you will quickly see that the solutions (in the complex numbers!) of this are sixth roots of unity; that is, they have T^6=1. This clearly can't hold in terms of types (it would mean an equivalence between 6-tuples of trees and objects of the "unit type", there being only one such object), but it turns out that T^7=T is "true"; you can find an explicit construction for it on page 3 of http://arxiv.org/abs/math/9405205 if you like. 3. It doesn't appear that the author of the OP ever got round to writing about negative and fractional types, but other people have. For instance, this paper http://www.cs.indiana.edu/~sabry/papers/rational.pdf which I have only glanced at (it appears to do this in a more restrictive context where there aren't general ADTs with recursive definitions; negative types seem to involve running computations backwards somehow, and reciprocals are "constraints"). Apologies if I've got my Haskell syntax wrong anywhere.
函数类型的指数律对应 curry/uncurry、Either 消除和记忆化组合子。
数据类型里有一条漂亮的代数律：a -> (b,c) 等于 (a->b, a->c)，即 (b*c)^a = b^a*c^a；它可用于提取公共参数、优化重复函数调用。另一条是 (c^b)^a = c^(b*a)，即 a -> b -> c = (a,b) -> c，也就是 curry/uncurry，范畴论中的积/指数伴随。再看 a^b * a^c = a^(b+c)，即 (b->a, c->a) = Either b c -> a；令 b,c 为 unit，则 ()->a 本质上就是 a，得到 a*a = a² = Bool -> a，这是用 memo-combinators 记忆纯函数技巧的种子。
tel查看英文原文
A nice algebraic law that holds in data types is a -> (b, c) = (a -> b, a -> c) (b * c)^a = b^a * c^a This is useful as common argument factoring and can optimize repeated function calls. Another is the famous (c^b)^a = c^(b * a) a -> b -> c = (a, b) -> c Which is curry/uncurry or the "product/exponential adjunction" in category theory. Finally, consider a^b * a^c = a^(b + c) (b -> a, c -> a) = Either b c -> a Which essentially says that given a tuple of functions we can choose which one we want to evaluate. Choose b and c to be unit and notice that `() -> a` is essentially `a` (after all, a^1 = a) and you'll have a * a = a^2 (a, a) = Bool -> a Which is the seed of a useful way of memorizing pure functions (look up memo-combinators for many more details).
递归类型展开和半环视角解释了 List/Nat 方程及零次幂规则。
如果把 List 的展开写成 L a = 1 + a × (L a) = 1 + a + a² + a³ + …，再令 a=1，就得到 L 1 = 1 + 1 + 1² + 1³ + … = 1 + (L 1)，也就是自然数 N = 1 + N。经典代数里的 x⁰=1 也成立：从空类型 0 到任意类型恰有一个函数。类型上的积与余积构成半环，而 List 是它的闭包。
sjolsen查看英文原文
It's worth noting that if you take the expansion for List: L a = 𝟏 + a × (L a) = 𝟏 + a + a² + a³ + ⋯ and substitute 𝟏 for a: L 𝟏 = 𝟏 + 𝟏 + 𝟏² + 𝟏³ + ⋯ = 𝟏 + 𝟏 + 𝟏 + 𝟏 + ⋯ = 𝟏 + (L 𝟏) you get ℕ: ℕ = 𝟏 + ℕ The zero-power rule (x⁰ = 1) from classic algebra also holds; there is exactly one function from 𝟎 to any type (or in set-theoretic terms, from the empty set to any set). There was an interesting paper on "closed semirings"[0] posted here a few days ago. Clearly, the product and coproduct on types form a semiring, and interestingly, List is the closure! [0] http://www.cl.cam.ac.uk/~sd601/papers/semirings.pdf
评论把类型代数放回 Scott-Strachey 域理论和指称语义的历史中，说明递归类型的数学基础。
这很有趣也略令人意外，但也许不该意外。我想起 Dana Scott 和 Christopher Strachey 用格或完备偏序加一点拓扑来建模程序可能计算的图，像分析中那样定义最小上界/最大下界与连续性，从而为计算构造极限；他们称这种模型为 domain。这部分数学是指称语义的基础，也是必要的，因为集合大体足以支撑代数与分析，却不足以处理部分函数、副作用和变量赋值这类程序中的“麻烦”。我相信 Strachey 和 Scott 也引入了和、积与递归类型的正式概念，并通过 domain 上的极限说明递归类型和函数的定义/模型可以有良基基础。早期技术报告和 David Schmidt 的免费书可作参考。
vajrabum查看英文原文
That's fun and a bit surprising, but maybe it shouldn't be. I'm reminded that Dana Scott with Christopher Strachey showed that by using lattices or complete partial orders with a bit of topology to model graphs of possible computations of a program you could, just as in analysis, define least upper and lower bounds and a notion of continuity to derive a construction of limit for a computation which is analogous to a limit in analysis. They called this model a domain. That bit of of math is the basis of denotational semantics of programming languages and is necessary because sets are largely sufficient as the basis for algebra and analysis but not for programs which have evils like partial functions, side effects and variable assignment. I believe that Christopher Strachey with Scott also introduced the formal notions of sum, product and recusive types. They also showed how definitions or models of recursive types and functions could be well founded through their construction of limits on domains. An early tech report on it can be found here: https://www.cs.ox.ac.uk/files/3228/PRG06.pdf and here's a more recent free book from David Schmidt on the topic: http://people.cs.ksu.edu/~schmidt/text/DenSem-full-book.pdf
历次讨论
同类还值得读
位运算技巧集
Bit Twiddling Hacks
斯坦福页面上的经典位运算技巧合集，收录了 popcount、前导/尾随零、位反转、交换、舍入等大量技巧，并附有解释和性能讨论。
算法与计算机科学上首页 8 次 · 2011–2024graphics.stanford.edu编辑精选如何不按平均评分排序
How Not To Sort By Average Rating
经典文章解释了为什么按平均评分排序不可靠：只有少量评价的条目（比如仅一条五星）会轻易排到最前，而评价数量的差异被忽略。
算法与计算机科学上首页 7 次 · 2009–2024evanmiller.org编辑精选数据结构可视化
Data Structure Visualizations
旧金山大学 David Galles 教授制作的数据结构与算法交互式可视化网站，涵盖 B 树、红黑树、排序、图算法等，可逐步操作观察其运行过程。
算法与计算机科学上首页 6 次 · 2011–2021cs.usfca.edu编辑精选1996 年以来的计算机科学最佳论文奖
Best Paper Awards in Computer Science since 1996
Jeff Huang 维护的一个汇总页面，收录了自 1996 年以来计算机科学各主要会议的“最佳论文奖”获奖名单，并按年份和会议整理，方便读者一站式浏览历届获奖论文。
算法与计算机科学上首页 6 次 · 2010–2018jeffhuang.com编辑精选算法（Jeff Erickson）
Algorithms, by Jeff Erickson
伊利诺伊大学 Jeff Erickson 教授的算法课教材，免费在线开放。
算法与计算机科学上首页 5 次 · 2018–2022jeffe.cs.illinois.edu编辑精选