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

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

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

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

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

玩得开心!