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

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

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

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

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

麦克劳林级数的定义

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

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

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

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

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

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

麦克劳林级数的定义

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

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

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

依赖类型理论和“任意”类型函数

我对这个问题的第一个回答是概念多，细节少，并反映在子问题上，“发生了什么?”这个答案将是相同的，但专注于子问题，“我们可以得到任意类型的函数吗?”

sum和product代数运算的一个扩展是所谓的“大算子”，它表示序列的和和乘积(或者更一般地说，一个域上函数的和和乘积)，通常分别写为Σ和Π。参见Sigma符号。

所以求和

a₀ + a₁X + a₂X² + ...

可以写成

Σ[i ∈ ℕ]aᵢXⁱ

例如，a是一个实数序列。该产品将类似地表示为Π而不是Σ。

当你从远处看时，这种表达式看起来很像X中的“任意”函数;当然，我们仅限于可表示的级数，以及它们相关的解析函数。这是类型理论的一个候选表示吗?当然!

The class of type theories which have immediate representations of these expressions is the class of 'dependent' type theories: theories with dependent types. Naturally we have terms dependent on terms, and in languages like Haskell with type functions and type quantification, terms and types depending on types. In a dependent setting, we additionally have types depending on terms. Haskell is not a dependently typed language, although many features of dependent types can be simulated by torturing the language a bit.

Curry-Howard和依赖型

The 'Curry-Howard isomorphism' started life as an observation that the terms and type-judging rules of simply-typed lambda calculus correspond exactly to natural deduction (as formulated by Gentzen) applied to intuitionistic propositional logic, with types taking the place of propositions, and terms taking the place of proofs, despite the two being independently invented/discovered. Since then, it has been a huge source of inspiration for type theorists. One of the most obvious things to consider is whether, and how, this correspondence for propositional logic can be extended to predicate or higher order logics. Dependent type theories initially arose from this avenue of exploration.

有关简单类型lambda演算的Curry-Howard同构的介绍，请参阅这里。举个例子，如果我们想证明A∧B，我们必须证明A和B;一个组合证明就是一对证明:每个连取一个。

在自然推演中:

Γ ⊢ A    Γ ⊢ B
Γ ⊢ A ∧ B

在简单类型的lambda演算中:

Γ ⊢ a : A    Γ ⊢ b : B
Γ ⊢ (a, b) : A × B

∨、和类型、→、函数类型以及各种消去规则也存在类似的对应关系。

一个不可证明的(直觉错误的)命题对应一个无人居住的类型。

With the analogy of types as logical propositions in mind, we can start to consider how to model predicates in the type-world. There are many ways in which this has been formalised (see this introduction to Martin-Löf's Intuitionistic Type Theory for a widely-used standard) but the abstract approach usually observes that a predicate is like a proposition with free term variables, or, alternatively, a function taking terms to propositions. If we allow type expressions to contain terms, then a treatment in lambda calculus style immediately presents itself as a possibility!

仅考虑构造性证明，∀x∈X.P(x)的证明是什么?我们可以把它看作是一个证明函数，让项(x)证明它们对应的命题(P(x))。因此，类型(命题)∀x: X.P(x)的成员(证明)是“相关函数”，它为x中的每个x给出了类型P(x)的项。

∃x∈X.P(x)呢?我们需要X X中的任意元素，以及P(X)的证明。因此，类型(命题)∃x: X.P(x)的成员(证明)是“依赖对”:x中的区分项x，以及类型P(x)的项。

符号: 我会用

∀x ∈ X...

关于X类成员的实际陈述，以及

∀x : X...

对于类型x上对应于通用量化的类型表达式，∃也是如此。

组合考虑:乘积和

除了类型与命题的Curry-Howard对应之外，我们还有代数类型与数和函数的组合对应，这是这个问题的要点。令人高兴的是，这可以扩展到上面概述的依赖类型!

我用模数表示

|A|

来表示a型的“大小”，以明确问题中概述的类型和数字之间的对应关系。请注意，这是理论之外的一个概念;我并不认为在语言中需要任何这样的运算符。

让我们计算类型的可能(完全简化的，规范的)成员

∀x : X.P(x)

它是依赖函数的类型，将x类型的项x转换为P(x)类型的项。每个这样的函数对于X的每一项都必须有一个输出，并且这个输出必须是特定类型的。对于x中的每一个x，这就给出了|p (x)|个“选项”的输出。

笑点是

|∀x : X.P(x)| = Π[x : X]|P(x)|

当然，如果X是IO()，这没有多大意义，但适用于代数类型。

类似地，类型术语

∃x : X.P(x)

是p: p (x)对(x, p)的类型，因此给定x中的任何x，我们可以与p (x)中的任何成员构造一个适当的对，给| p (x)| '选项'。

因此,

|∃x : X.P(x)| = Σ[x : X]|P(x)|

同样的警告。

这证明了在理论中使用符号Π和Σ来表示依赖类型的共同符号是正确的，事实上，由于上述对应关系，许多理论模糊了“for all”和“product”以及“there is”和“sum”之间的区别。

我们越来越近了!

向量:表示依赖元组

我们现在能像这样编码数值表达式吗

Σ[n ∈ ℕ]Xⁿ

作为类型表达式?

不完全是。虽然我们可以非正式地考虑像Haskell中的Xⁿ这样的表达式的含义，其中X是类型，n是自然数，但这是一种符号滥用;这是一个包含数字的类型表达式:显然不是一个有效的表达式。

另一方面，对于图中的依赖类型，类型包含数字正是关键所在;事实上，依赖元组或“向量”是一个经常被引用的例子，说明依赖类型如何为列表访问等操作提供实用的类型级安全。vector只是一个包含关于其长度的类型级信息的列表:这正是我们对Xⁿ这样的类型表达式所追求的。

在此回答期间，让

Vec X n

x类型值的长度为n的向量的类型。

从技术上讲，这里的n不是一个实际的自然数，而是一个自然数在系统中的表示。我们可以用Peano风格将自然数(Nat)表示为零(0)或另一个自然数的后继数(S)，对于n∈ℕ，我写˻n˼来表示Nat中表示n的项。例如，˻3˼是S (S (S 0))。

然后我们有

|Vec X ˻n˼| = |X|ⁿ

对于任意n∈ℕ。

Nat类型:将ℕ术语提升为类型

现在我们可以像这样编码表达式

Σ[n ∈ ℕ]Xⁿ

作为类型。这个特殊的表达式会产生一种类型，这种类型当然与X的列表类型同构，就像问题中所指出的那样。(不仅如此，从范畴论的观点来看，将X取为上述类型的函子的类型函数与List函子自然同构。)

“任意”函数的最后一个难题是如何编码

f : ℕ → ℕ

表达式如

Σ[n ∈ ℕ]f(n)Xⁿ

所以我们可以把任意系数应用到幂级数上。

我们已经理解了代数类型与数字的对应关系，这使我们能够从类型映射到数字，从类型函数映射到数值函数。我们也可以走另一条路!-取一个自然数，显然有一个可定义的代数类型，有这么多项成员，不管我们是否有依赖类型。我们可以很容易地在类型理论之外用归纳法证明这一点。我们需要的是一种在系统内部从自然数映射到类型的方法。

一个令人高兴的认识是，一旦我们有了依赖类型，归纳证明和递归构造就变得非常相似——事实上，在许多理论中，它们是完全相同的东西。既然我们可以通过归纳法证明满足我们需求的类型是存在的，难道我们就不能构建它们吗?

有几种方法可以在术语级别表示类型。我将在这里使用一个虚构的Haskellish符号*来表示类型的宇宙，它本身通常被认为是依赖设置中的类型

同样地，也有至少和依赖类型理论一样多的方法来标记'ℕ-elimination'。我将使用Haskellish模式匹配符号。

我们需要一个映射，α从Nat到*，带有属性

∀n ∈ ℕ.|α ˻n˼| = n.

下面的伪定义就足够了。

data Zero -- empty type
data Successor a = Z | Suc a -- Successor ≅ Maybe

α : Nat -> *
α 0 = Zero
α (S n) = Successor (α n)

所以我们看到α的作用反映了后继S的行为，使它成为一种同态。继任者是一个类型函数，它将一个类型的成员数量“加1”;也就是说，|继任者a| = 1 + |a|对于任何a具有定义的大小。

例如α˻4˼(即α (S (S (S (S 0)))))))

Successor (Successor (Successor (Successor Zero)))

这种类型的项是

Z
Suc Z
Suc (Suc Z)
Suc (Suc (Suc Z))

正好有四个元素:|α˻4˼| = 4。

同样地，对于任意n∈ℕ，我们有

|α ˻n˼| = n

是必需的。

许多理论要求*的成员仅仅是类型的代表，并且操作提供了从类型*到相关类型的显式映射。其他理论允许文字类型本身是术语级实体。

“任意”功能?

现在我们有了把一个完全一般的幂级数表示为一种类型的仪器!

该系列

Σ[n ∈ ℕ]f(n)Xⁿ

变成类型

∃n : Nat.α (˻f˼ n) × (Vec X n)

其中˻f˼:Nat→Nat是函数f的语言中一些合适的表示。我们可以看到如下。

|∃n : Nat.α (˻f˼ n) × (Vec X n)|
    = Σ[n : Nat]|α (˻f˼ n) × (Vec X n)|          (property of ∃ types)
    = Σ[n ∈ ℕ]|α (˻f˼ ˻n˼) × (Vec X ˻n˼)|        (switching Nat for ℕ)
    = Σ[n ∈ ℕ]|α ˻f(n)˼ × (Vec X ˻n˼)|           (applying ˻f˼ to ˻n˼)
    = Σ[n ∈ ℕ]|α ˻f(n)˼||Vec X ˻n˼|              (splitting product)
    = Σ[n ∈ ℕ]f(n)|X|ⁿ                           (properties of α and Vec)

这有多“武断”?这种方法不仅适用于整数系数，而且适用于自然数。除此之外，f可以是任何东西，给定具有依赖类型的图灵完备语言，我们可以表示任何具有自然数系数的解析函数。

我还没有调查这与，例如，列表X≅1/(1 - X)问题中提供的情况的相互作用，或者这种负的和非整数的“类型”在这个上下文中可能有什么意义。

希望这个答案能在某种程度上帮助我们探索任意类型的函数能走多远。

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

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