滥用代数数据类型的代数 - 为什么这会起作用？ [英] Abusing the algebra of algebraic data types - why does this work?

问题描述

代数数据类型的代数表达式对于具有数学背景的人来说看起来非常具有启发性。让我试着解释我的意思。

定义了基本类型

• 产品•


• 联盟 +


• 单身 X


• 单位 1





并使用简写X²用于 X•X X + X 等，我们可以定义代数表达式，例如c>和 2X 链接列表



数据List a = Nil |缺点a（列表a）↔ L = 1 + X•L





和二叉树：





数据树a =无|分支a（树a）（树a）↔ T = 1 + X•T²





现在，作为数学家的第一本能就是坚持使用这些表达式，并试着解决 L 和 T 。我可以通过反复替换来做到这一点，但似乎更容易滥用记法，并假装我可以随意重新排列它。例如，对于一个链表：



L = 1 + X•L



（1 - X）•L = 1




L = 1 /（1-X）= 1 + X + X 2 + X 3 + ...





以一种完全没有道理的方式扩展 1 /（1-X）以获得一个有趣的结果，即 L type是 Nil ，或者它包含1个元素，或者它包含2个元素，或者3等。



<如果我们为二叉树做这件事情，它会变得更有趣：



T = 1 + X•T²





X•T² - T + 1 = 0





T =（1 - √（1 - 4•X））/（2•X）



T = 1 + X + 2•X²+ 5•X³+ 14•X₄+ ...



使用幂级数展开（用 Wolfram Alpha ） 。这表达了对我而言非常明显的事实，即只有一个元素的二叉树，有两个元素的二叉树（第二个元素可以在左边或右边的分支上），5个具有三个元素的二叉树等。



所以我的问题是 - 我在这里做什么？这些操作似乎是不合理的（无论如何，代数数据类型的平方根究竟是什么？），但它们会导致明显的结果。两个代数数据类型的商是否在计算机科学中具有任何意义？或者它只是符号的诡计？



或许更有趣的是，是否有可能扩展这些想法？是否存在类型代数的理论，例如允许类型上的任意函数，或类型是否需要幂级数表示？如果你可以定义一个类的函数，那么函数的组合是否有任何意义？ 解决方案

免责声明：很多这样做当你解释⊥时，你确实没什么问题，所以为了简单起见，我会公然无视这一点。



一些初始点：$ b​​
$ b

• 请注意，union可能并非A + B的最佳术语 - 这是专门一个不相交的联盟这两种类型，因为即使它们的类型相同，双方也是有区别的。对于它的价值，更常见的术语就是总和类型。单元类型实际上是所有的单元类型。
  

• 它们在代数操作下的表现完全相同，更重要的是，信息量仍然保留。

你可能也想要一个零类型。没有标准的名称，但最常见的名称是 Void 。没有任何值的类型为零，就像存在一个类型为1的值一样。

主要操作在这里不见了，但我马上就会回到这一点。

正如你可能已经注意到的，Haskell倾向于借用分类理论的概念，上面有一个非常直接的解释：

• 给定 Hask 中的对象A和B，他们的产品A×B是允许两个投影的唯一（最多同构）类型：A×B→A和 snd ：A×B→B，其中给定任何类型C和函数 f ：C→A， g ：C→B您可以定义配对 f&&& g ：C→A×B，使得 fst <（f&&& g） = f EM>。参数性自动保证了通用属性，而我的名字的低微选择应该给你这个想法。顺便说一句，（&&）运算符在 Control.Arrow 中定义。




• 上面的对偶是带有注入的副产品A + B inl ：A→A + B和 inr ：B→A + B，其中给定任意类型C和函数 f ：A→C， g ：B→C，可以定义共同的 f ||| g ：A + B→C，使得明显的等价性成立。同样，参数化可以自动保证大部分棘手的部件。在这种情况下，标准注入只是 Left 和 Right ，并且共同作用是任何。

产品和总和类型的许多属性都可以从以上。请注意，任何singleton类型都是 Hask 的终端对象，任何空类型都是初始对象。

返回上述缺失操作，在笛卡尔封闭类别 指数对象，它们对应于类别的箭头。我们的箭头是函数，我们的对象是类型 * ，类型 A - > B 在类型的代数操作的上下文中确实表现为B ^A 。如果这不是明显的原因，请考虑类型 Bool - > A 。只有两个可能的输入，该类型的函数同构于 A 类型的两个值，即（A，A）。对于 Maybe Bool - >一个我们有三个可能的输入，依此类推。另外，请注意，如果我们将上面的共同定义重新定义为使用代数符号，我们可以得到C = >

至于为什么这一切都是有道理的 - 特别是为什么你使用幂级数展开是合理的 - 注意上面的大部分指的是某种类型的居民（即，具有这种类型的不同值），以展示代数行为。为了使该透视明确：

• 产品类型（A，B）表示来自 A 和 B 的独立值。因此，对于任何固定值 a :: A ，每个居民有一个类型（A，B）的值 B 。这当然是笛卡尔产品，而产品类型的居民数量是这些因素的居民数量的乘积。




• 总和类型 AB 代表来自 A 或 B 的值，与左右分支区分开来。正如前面提到的，这是一个不相交的联盟，而和类型的居民人数是和命令的居民人数的总和。

指数型 B - > 表示从 B> 类型值到 A 类型值的映射。对于任何固定参数 b :: B ，任何 A 值都可以赋值给它;类型的值 B - >一个为每个输入选择一个这样的映射，相当于 A 的许多副本的产品，如 B 有居民，因此是指数。

尽管它首先将类型视为集，在这种情况下实际上并不能很好地工作 - 我们使用联合而不是标准的联合集合，对交集或其他集合操作没有明显的解释，我们通常不关心集合成员（离开那到类型检查器）。另一方面，上面的建筑花费了大量时间来讨论计数居民，并且 列举了一种类型的可能值在这里是一个有用的概念。这很快使我们能够枚举组合，如果您查阅链接的维基百科文章，您会发现它所做的第一件事情之一就是通过生成函数，然后使用与您所做的完全相同的技术对与Haskell列表相同的序列做同样的处理。

---

编辑：哦，这里有一个很快的奖励，我认为这一点非常明显。您在评论中提到，对于树型 T = 1 + T ^ 2 ，您可以导出标识 T ^ 6 = 1 ，这显然是错误的。然而， T ^ 7 = T does 成立，并且可以直接构造树和七元组树之间的双射。 Andreas Blass的七棵树在一起。

编辑×2：关于其他答案中提到的类型派生构造的主题，您可能还会喜欢本文来自同一作者，它进一步构建了这个想法，包括分裂的概念和其他有趣的东西。

The 'algebraic' expression for algebraic data types looks very suggestive to someone with a background in mathematics. Let me try to explain what I mean.

Having defined the basic types

• Product •
• Union +
• Singleton X
• Unit 1

and using the shorthand X² for X•X and 2X for X+X et cetera, we can then define algebraic expressions for e.g. linked lists

data List a = Nil | Cons a (List a) ↔ L = 1 + X • L

and binary trees:

data Tree a = Nil | Branch a (Tree a) (Tree a) ↔ T = 1 + X • T²

Now, my first instinct as a mathematician is to go nuts with these expressions, and try to solve for L and T. I could do this through repeated substitution, but it seems much easier to abuse the notation horrifically and pretend I can rearrange it at will. For example, for a linked list:

L = 1 + X • L

(1 - X) • L = 1

L = 1 / (1 - X) = 1 + X + X² + X³ + ...

where I've used the power series expansion of 1 / (1 - X) in a totally unjustified way to derive an interesting result, namely that an L type is either Nil, or it contains 1 element, or it contains 2 elements, or 3, etc.

It gets more interesting if we do it for binary trees:

T = 1 + X • T²

X • T² - T + 1 = 0

T = (1 - √(1 - 4 • X)) / (2 • X)

T = 1 + X + 2 • X² + 5 • X³ + 14 • X⁴ + ...

again, using the power series expansion (done with Wolfram Alpha). This expresses the non-obvious (to me) fact that there is only one binary tree with 1 element, 2 binary trees with two elements (the second element can be on the left or the right branch), 5 binary trees with three elements etc.

So my question is - what am I doing here? These operations seem unjustified (what exactly is the square root of an algebraic data type anyway?) but they lead to sensible results. does the quotient of two algebraic data types have any meaning in computer science, or is it just notational trickery?

And, perhaps more interestingly, is it possible to extend these ideas? Is there a theory of the algebra of types that allows, for example, arbitrary functions on types, or do types require a power series representation? If you can define a class of functions, then does composition of functions have any meaning?

解决方案

Disclaimer: A lot of this doesn't really work quite right when you account for ⊥, so I'm going to blatantly disregard that for the sake of simplicity.

A few initial points:

• Note that "union" is probably not the best term for A+B here--that's specifically a disjoint union of the two types, because the two sides are distinguished even if their types are the same. For what it's worth, the more common term is simply "sum type".

• Singleton types are, effectively, all unit types. They behave identically under algebraic manipulations and, more importantly, the amount of information present is still preserved.

• You probably want a zero type as well. There isn't a standard one, but the most common name is Void. There are no values whose type is zero, just as there is one value whose type is one.

There's still one major operation missing here but I'll get back to that in a moment.

As you've probably noticed, Haskell tends to borrow concepts from Category Theory, and all of the above has a very straightforward interpretation as such:

• Given objects A and B in Hask, their product A×B is the unique (up to isomorphism) type that allows two projections fst : A×B → A and snd : A×B → B, where given any type C and functions f : C → A, g : C → B you can define the pairing f &&& g : C → A×B such that fst ∘ (f &&& g) = f and likewise for g. Parametricity guarantees the universal properties automatically and my less-than-subtle choice of names should give you the idea. The (&&&) operator is defined in Control.Arrow, by the way.

• The dual of the above is the coproduct A+B with injections inl : A → A+B and inr : B → A+B, where given any type C and functions f : A → C, g : B → C, you can define the copairing f ||| g : A+B → C such that the obvious equivalences hold. Again, parametricity guarantees most of the tricky parts automatically. In this case, the standard injections are simply Left and Right and the copairing is the function either.

Many of the properties of product and sum types can be derived from the above. Note that any singleton type is a terminal object of Hask and any empty type is an initial object.

Returning to the aforementioned missing operation, in a cartesian closed category you have exponential objects that correspond to arrows of the category. Our arrows are functions, our objects are types with kind *, and the type A -> B indeed behaves as B^A in the context of algebraic manipulation of types. If it's not obvious why this should hold, consider the type Bool -> A. With only two possible inputs, a function of that type is isomorphic to two values of type A, i.e. (A, A). For Maybe Bool -> A we have three possible inputs, and so on. Also, observe that if we rephrase the copairing definition above to use algebraic notation, we get the identity C^A × C^B = C^A+B.

As for why this all makes sense--and in particular why your use of the power series expansion is justified--note that much of the above refers to the "inhabitants" of a type (i.e., distinct values having that type) in order to demonstrate the algebraic behavior. To make that perspective explicit:

• The product type (A, B) represents a value each from A and B, taken independently. So for any fixed value a :: A, there is one value of type (A, B) for each inhabitant of B. This is of course the cartesian product, and the number of inhabitants of the product type is the product of the number of inhabitants of the factors.

• The sum type Either A B represents a value from either A or B, with the left and right branches distinguished. As mentioned earlier, this is a disjoint union, and the number of inhabitants of the sum type is the sum of the number of inhabitants of the summands.

• The exponential type B -> A represents a mapping from values of type B to values of type A. For any fixed argument b :: B, any value of A can be assigned to it; a value of type B -> A picks one such mapping for each input, which is equivalent to a product of as many copies of A as B has inhabitants, hence the exponentiation.

While it's tempting at first to treat types as sets, that doesn't actually work very well in this context--we have disjoint union rather than the standard union of sets, there's no obvious interpretation of intersection or many other set operations, and we don't usually care about set membership (leaving that to the type checker).

On the other hand, the constructions above spend a lot of time talking about counting inhabitants, and enumerating the possible values of a type is a useful concept here. That quickly leads us to enumerative combinatorics, and if you consult the linked Wikipedia article you'll find that one of the first things it does is define "pairs" and "unions" in exactly the same sense as product and sum types by way of generating functions, then does the same for "sequences" that are identical to Haskell's lists using exactly the same technique you did.

---

Edit: Oh, and here's a quick bonus that I think demonstrates the point strikingly. You mentioned in a comment that for a tree type T = 1 + T^2 you can derive the identity T^6 = 1, which is clearly wrong. However, T^7 = T does hold, and a bijection between trees and seven-tuples of trees can be constructed directly, cf. Andreas Blass's "Seven Trees in One".

Edit×2: On the subject of the "derivative of a type" construction mentioned in other answers, you might also enjoy this paper from the same author which builds on the idea further, including notions of division and other interesting whatnot.

这篇关于滥用代数数据类型的代数 - 为什么这会起作用？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！