二叉树由类型半环中的方程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关于组合物种的论文，因为一些研究与物种密切相关，但物种与类型并不相同。)

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

玩得开心!

二叉树由类型半环中的方程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关于组合物种的论文，因为一些研究与物种密切相关，但物种与类型并不相同。)

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

玩得开心!

我没有一个完整的答案，但这些操作往往“只是工作”。相关的论文可能是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:关于在其他答案中提到的“类型的导数”结构的主题，您可能也会喜欢同一作者的这篇论文，它进一步建立在这个思想之上，包括除法的概念和其他有趣的东西。

微积分和带有类型的麦克劳林级数

这里是另一个小的补充-一个组合的见解，为什么系数在级数展开应该“工作”，特别是关注级数，可以从微积分中使用泰勒-麦克劳林方法推导。注意:你给出的操纵列表类型的级数展开例子是麦克劳林级数。

由于其他答案和评论处理代数类型表达式的行为(和，乘积和指数)，这个答案将省略这个细节，专注于类型“演算”。

你可能会注意到，在这个答案中，倒逗号起了很大的作用。原因有二:

我们从事的工作是从一个领域对另一个领域的实体作出解释，以这种方式界定这样那样的外国概念似乎是合适的。 有些概念可以更严格地形式化，但形状和思想似乎比细节更重要(而且写起来不太占篇幅)。

麦克劳林级数的定义

函数f:ℝ→ℝ的麦克劳林级数定义为

f(0) + f'(0)X + (1/2)f''(0)X² + ... + (1/n!)f⁽ⁿ⁾(0)Xⁿ + ...

f⁽ⁿ⁾表示f的n阶导数。

为了能够理解用类型解释的Maclaurin系列，我们需要了解如何在类型上下文中解释三件事:

一个(可能是多重)导数 将函数应用到0 像(1/n!)

事实证明，从分析中得到的这些概念在类型世界中也有相应的对应。

我所说的“合适的对手”是什么意思?它应该有一种同构的味道——如果我们可以在两个方向上保持真理，那么在一个上下文中可以推导出的事实就可以转移到另一个上下文中。

有类型的微积分

类型表达式的导数是什么意思呢?事实证明，对于一个大型且行为良好(“可微的”)的类型表达式和函子类，存在一个行为足够相似的自然运算，这是一个合适的解释!

To spoil the punchline, the operation analogous to differentiation is that of making 'one-hole contexts'. This is an excellent place to expand on this particular point further but the basic concept of a one-hole context (da/dx) is that it represents the result of extracting a single subitem of a particular type (x) from a term (of type a), preserving all other information, including that necessary to determine the original location of the subitem. For example, one way to represent a one-hole context for a list is with two lists: one for items which came before the extracted one, and one for items which came after.

鉴别这种区分操作的动机来自以下观察结果。da/dx表示a型中有x型洞的单孔环境的类型。

d1/dx = 0
dx/dx = 1
d(a + b)/dx = da/dx + db/dx
d(a × b)/dx = a × db/dx + b × da/dx
d(g(f(x))/dx = d(g(y))/dy[f(x)/a] × df(x)/dx

这里，1和0分别表示恰好为1和恰好为0的居民类型，+和×通常表示和和和产品类型。F和g用于表示类型函数，或类型表达式生成器，[F (x)/a]表示用F (x)替换前面表达式中的每一个a。

这可以用一种无点的方式来写，f'表示类型函数f的导数函数，因此:

(x ↦ 1)' = x ↦ 0
(x ↦ x)' = x ↦ 1
(f + g)' = f' + g'
(f × g)' = f × g' + g × f'
(g ∘ f)' = (g' ∘ f) × f'

这可能更可取。

注意:如果用类型和函子的同构类来定义导数，则可以使等式严格而精确。

现在，我们特别注意到，微积分中有关加法、乘法和复合代数运算的规则(通常称为和、积和链规则)恰好反映在“打洞”运算中。此外，在常数表达式中“挖洞”或术语本身的基本情况也表现为微分，因此通过归纳，我们得到了所有代数类型表达式的类微分行为。

现在我们可以解释微分了，一个类型表达式的n阶导数dⁿe/dxⁿ是什么意思?它是一种表示n个位置上下文的类型:当用n个类型x的项“填充”时，这些项会产生一个e。后面还有一个与'(1/n!)'相关的关键观察结果。

类型函子的不变部分:将函数应用于0

We already have an interpretation for 0 in the type world: an empty type with no members. What does it mean, from a combinatorial point of view, to apply a type function to it? In more concrete terms, supposing f is a type function, what does f(0) look like? Well, we certainly don't have access to anything of type 0, so any constructions of f(x) which require an x are unavailable. What is left is those terms which are accessible in their absence, which we can call the 'invariant' or 'constant' part of the type.

举一个显式的例子，以Maybe函子为例，它可以用代数表示为x↦1 + x。当我们把它应用到0时，我们得到1 + 0 -它就像1:唯一可能的值是None值。对于列表，类似地，我们只得到与空列表对应的项。

当我们把它带回来并将类型f(0)解释为一个数字时，它可以被认为是在不访问x的情况下可以获得多少类型f(x)的项的计数:即“类空”项的数量。

把它放在一起:完整的诠释麦克劳林系列

恐怕我想不出将(1/n!)直接解释为类型的合适方法。

如果我们考虑，但是，根据上述，类型f⁽ⁿ⁾(0)，我们看到它可以被解释为类型f(x)的n个位置上下文的类型，其中不包含x -也就是说，当我们对它们进行n次积分时，结果项恰好有n个xs，不多也不少。然后，将类型f⁽ⁿ⁾(0)解释为一个数字(就像f的麦克劳林级数的系数一样)只是计算有多少这样的空n位上下文。我们就快到了!

但是(1/n!)会在哪里结束呢?检查类型“分化”的过程向我们表明，当应用多次时，它保留了提取子术语的“顺序”。例如，考虑x × x型的术语(x₀，x₁)以及在其上“钻孔”两次的操作。我们得到了两个序列

(x₀, x₁)  ↝  (_₀, x₁)  ↝  (_₀, _₁)
(x₀, x₁)  ↝  (x₀, _₀)  ↝  (_₁, _₀)
(where _ represents a 'hole')

尽管它们都来自同一个词，因为有两个!= 2种从两个元素中取两个元素的方法，保持顺序。一般有n!因此，为了得到一个函子类型有n个元素的配置数的计数，我们必须计算类型f⁽ⁿ⁾(0)并除以n!，和麦克劳林级数的系数一样。

所以除以n!可以简单地解释为它本身。

最后的想法:“递归”定义和分析性

首先是一些观察:

如果一个函数f:ℝ→ℝ有一个导数，这个导数是唯一的 类似地，如果一个函数f:ℝ→ℝ是解析函数，它恰好有一个对应的多项式级数

因为我们有链式法则，我们可以使用隐微分，如果我们把类型导数形式化为同构类。但是隐式微分不需要任何像减法或除法这样的外星操作!所以我们可以用它来分析递归类型定义。以你的列表为例，我们有

L(X) ≅ 1 + X × L(X)
L'(X) = X × L'(X) + L(X)

然后我们可以求值

L'(0) = L(0) = 1

得到麦克劳林级数中X¹的系数。

但是，由于我们确信这些表达式确实是严格的“可微的”，如果只是隐式的，并且由于我们与函数ℝ→ℝ对应，其中导数肯定是唯一的，我们可以放心，即使我们使用“非法”操作获得值，结果也是有效的。

现在，同样地，使用第二个观察结果，由于与函数ℝ→ℝ的对应关系(是否是同态?)，我们知道，只要我们满意一个函数有一个麦克劳林级数，如果我们能找到任何级数，上面列出的原则可以应用于使其严谨。

关于你的函数组合问题，我想链式法则可以给出部分答案。

我不确定这适用于多少haskell风格的adt，但我怀疑它是很多，如果不是全部的话。我发现了一个非常奇妙的证据来证明这一事实，但这页空白处太小了，无法容纳它……

当然，这只是解决问题的一种方法可能还有很多其他方法。

摘要:TL,博士

类型'differentiation'对应于'making a hole'。 将函子应用到0可以得到该函子的“类空”项。 因此，麦克劳林幂级数(在某种程度上)严格对应于枚举具有一定数量元素的函子类型的成员数量。 隐式微分使它更加无懈可击。 导数的唯一性和幂级数的唯一性意味着我们可以篡改细节，这是可行的。