免责声明:当你考虑⊥时，很多东西都不太正确，所以为了简单起见，我将公然忽略这一点。

以下几点:

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. Haskell provides that as Void. There are no values whose type is zero, just as there is one value whose type is one.

这里还少了一个大手术，但我一会儿再讲。

正如你可能已经注意到的，Haskell倾向于借用范畴理论的概念，所有这些都有一个非常直接的解释:

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.

乘积和和类型的许多性质都可以从上面得到。注意，任何单例类型都是Hask的终端对象，任何空类型都是初始对象。

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 BA 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 CA × CB = CA+B.

至于为什么这一切都是有意义的——特别是为什么使用幂级数展开是合理的——请注意，为了演示代数行为，上面的许多内容都引用了类型的“居民”(即具有该类型的不同值)。要明确这种观点:

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.

虽然一开始很容易将类型视为集合，但在这种情况下实际上并不是很好——我们有不相交的并集，而不是集合的标准并集，没有交集或许多其他集合操作的明显解释，而且我们通常不关心集合成员关系(把它留给类型检查器)。

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.

编辑:哦，这里有一个快速的额外奖励，我认为它可以很好地说明这一点。你在评论中提到，对于树类型T = 1 + T^2，你可以推导出恒等式T^6 = 1，这显然是错误的。然而，T^7 = T是成立的，树和树的七元组之间的双射可以直接构建，参见Andreas Blass的“七棵树合一”。

Edit×2:关于在其他答案中提到的“类型的导数”结构的主题，您可能也会喜欢同一作者的这篇论文，它进一步建立在这个思想之上，包括除法的概念和其他有趣的东西。

我没有一个完整的答案，但这些操作往往“只是工作”。相关的论文可能是Fiore和Leinster的《作为复数的范畴对象》——我在阅读sigfpe关于相关主题的博客时偶然发现了这篇文章;该博客的其余部分是类似想法的金矿，值得一看!

顺便说一下，您还可以区分数据类型，这将为您提供数据类型的适当拉链!

看起来你所做的只是展开递归关系。

L = 1 + X • L
L = 1 + X • (1 + X • (1 + X • (1 + X • ...)))
  = 1 + X + X^2 + X^3 + X^4 ...

T = 1 + X • T^2
L = 1 + X • (1 + X • (1 + X • (1 + X • ...^2)^2)^2)^2
  = 1 + X + 2 • X^2 + 5 • X^3 + 14 • X^4 + ...

由于对类型的操作规则与算术操作规则类似，因此可以使用代数方法来帮助您确定如何展开递归关系(因为它并不明显)。

免责声明:当你考虑⊥时，很多东西都不太正确，所以为了简单起见，我将公然忽略这一点。

以下几点:

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. Haskell provides that as Void. There are no values whose type is zero, just as there is one value whose type is one.

这里还少了一个大手术，但我一会儿再讲。

正如你可能已经注意到的，Haskell倾向于借用范畴理论的概念，所有这些都有一个非常直接的解释:

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.

乘积和和类型的许多性质都可以从上面得到。注意，任何单例类型都是Hask的终端对象，任何空类型都是初始对象。

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 BA 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 CA × CB = CA+B.

至于为什么这一切都是有意义的——特别是为什么使用幂级数展开是合理的——请注意，为了演示代数行为，上面的许多内容都引用了类型的“居民”(即具有该类型的不同值)。要明确这种观点:

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.

虽然一开始很容易将类型视为集合，但在这种情况下实际上并不是很好——我们有不相交的并集，而不是集合的标准并集，没有交集或许多其他集合操作的明显解释，而且我们通常不关心集合成员关系(把它留给类型检查器)。

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.

编辑:哦，这里有一个快速的额外奖励，我认为它可以很好地说明这一点。你在评论中提到，对于树类型T = 1 + T^2，你可以推导出恒等式T^6 = 1，这显然是错误的。然而，T^7 = T是成立的，树和树的七元组之间的双射可以直接构建，参见Andreas Blass的“七棵树合一”。

Edit×2:关于在其他答案中提到的“类型的导数”结构的主题，您可能也会喜欢同一作者的这篇论文，它进一步建立在这个思想之上，包括除法的概念和其他有趣的东西。

二叉树由类型半环中的方程T=1+XT^2定义。根据构造，T=(1-根号下(1-4X))/(2X)由复数半环中的相同方程定义。既然我们在同一类代数结构中解同一个方程那么我们看到一些相似之处也就不足为奇了。

The catch is that when we reason about polynomials in the semiring of complex numbers we typically use the fact that the complex numbers form a ring or even a field so we find ourselves using operations such as subtraction that don't apply to semirings. But we can often eliminate subtractions from our arguments if we have a rule that allows us to cancel from both sides of an equation. This is the kind of thing proved by Fiore and Leinster showing that many arguments about rings can be transferred to semirings.

这意味着你关于环的许多数学知识可以可靠地转换为类型。因此，一些涉及复数或幂级数的参数(在形式幂级数的环中)可以以完全严格的方式传递到类型中。

然而，故事远不止于此。通过证明两个幂级数相等来证明两种类型相等是一回事。但是您也可以通过检查幂级数中的项来推断类型的信息。我不确定这里的正式声明应该是什么。(我推荐Brent Yorgey关于组合物种的论文，因为一些研究与物种密切相关，但物种与类型并不相同。)

让我非常惊讶的是你的发现可以扩展到微积分。关于微积分的定理可以转化为类型的半环。事实上，即使是关于有限差分的论点也可以转移过来你会发现数值分析中的经典定理在类型论中也有解释。

玩得开心!

通信流程代数(ACP)处理类似类型的流程表达式。 它提供加法和乘法作为选择和序列的操作符，并带有相关的中性元素。 在这些基础上，还有其他构造的运算符，比如并行和中断。 见http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes。网上还有一篇论文叫做“过程代数简史”。

我正在用ACP扩展编程语言。去年4月，我在Scala Days 2012上发表了一篇研究论文，可以在http://code.google.com/p/subscript/上找到

在会议上，我演示了一个调试器运行一个包的并行递归规范:

袋子= A;(个)

其中A和A代表输入和输出动作;分号和&号代表序列和并行性。在SkillsMatter上观看视频，可以从之前的链接获得。

一个袋规格更可比

L = 1 + X•L

将

B = 1 + X&B

ACP使用公理根据选择和顺序定义并行性;参见维基百科的文章。我想知道这个包的比喻是什么意思

L = 1 / (1- x)

ACP风格的编程对于文本解析器和GUI控制器来说非常方便。规范，例如

searchCommand =点击(searchButton) +键(Enter)

cancelCommand =点击(cancelButton) +键(Escape)

通过将“clicked”和“key”隐式化(就像Scala允许的函数一样)，可以更简洁地写下来。因此我们可以这样写:

searchCommand = searchButton +回车

cancelCommand = cancelButton + Escape

右边现在包含的操作数是数据，而不是进程。在这个级别上，没有必要知道哪些隐式细化将这些操作数转换为进程;它们不一定会细化成输入动作;输出动作也将适用，例如在测试机器人的规格中。

进程通过这种方式获得数据作为同伴;因此我创造了“项目代数”这个术语。