依赖类型理论和“任意”类型函数
我对这个问题的第一个回答充满了概念，缺乏细节，并反映了子问题：“发生了什么？”；这个答案也是一样的，但专注于子问题：“我们能得到任意类型的函数吗？”。
对于代数运算中的和与积，有一个扩展叫做“大型运算符”，它表示一个序列（或更一般地，域上的一个函数）的和与积，通常分别写作Σ和Π。请参见Sigma Notation。
因此，总和为
a₀ + a₁X + a₂X² + ...
可能会被写成
Σ[i ∈ ℕ]aᵢXⁱ
其中a是一些实数序列，例如。乘积将类似地表示为Π而不是Σ。
当您从远处观看时，这种表达式看起来很像X中的“任意”函数; 当然，我们受限于可表达的级数及其相关的解析函数。这是否是类型理论的一种表示候选？绝对是！
具有这些表达式的直接表示的类型理论类是“依赖”类型理论：具有依赖类型的理论。自然地，我们有依赖于术语的术语，并且在像Haskell这样具有类型函数和类型量化的语言中，还有依赖于类型的术语和类型。在依赖设置中，我们还有依赖于术语的类型。 Haskell不是依赖类型的语言，尽管可以通过折磨语言来模拟许多依赖类型的特性 （链接）。
Curry-Howard和依赖类型
“Curry-Howard同构”最初是一种观察，即简单类型λ演算的术语和类型判断规则与直觉命题逻辑（由Gentzen制定）应用于自然演绎完全对应，其中类型代替命题，术语代替证明，尽管两者是独立发明/发现的。从那时起，它一直是类型理论家的巨大灵感源泉。最明显的考虑之一是这种命题逻辑的对应是否可以扩展到谓词或高阶逻辑，以及如何扩展。依赖类型理论最初就是从这个探索方向出现的。
有关简单类型λ演算的Curry-Howard同构的介绍，请参见
此处。例如，如果我们想要证明
A ∧ B，我们必须证明
A并证明
B；联合证明只是一对证明：每个连结词都有一个。
在自然演绎中：
Γ ⊢ A Γ ⊢ B
Γ ⊢ A ∧ B
在简单类型 λ 演算中：
Γ ⊢ a : A Γ ⊢ b : B
Γ ⊢ (a, b) : A × B
类似的对应关系也存在于
∨ 和和类型、
→ 和函数类型，以及各种消解规则上。
一个不可证明的（直觉上为假的）命题对应于一个无人居住的类型。
考虑到类型与逻辑命题之间的类比，我们可以开始思考如何在类型世界中建模谓词。有许多方式进行形式化（参见 Martin-Löf 直觉型理论的
这个介绍 作为广泛使用的标准），但抽象方法通常观察到，谓词就像具有自由项变量的命题，或者说是将项映射到命题的函数。如果我们允许类型表达式包含项，则 lambda 演算风格的处理方法立即呈现出一种可能性！
考虑仅有建设性证明，那么构成 ∀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。同样适用于
∃。
组合学考虑：积和和
除了类型与命题的柯里-霍华德对应关系外，我们还有代数类型与数字和函数的组合学对应关系，这是本问题的重点。令人高兴的是，这可以扩展到上述依赖类型！
我将使用模数符号。
|A|
“size”是指代类型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)|
“带有相同警告”的意思是相同的限制条件或注意事项。
这证明了在使用符号Π和Σ的理论中，依赖类型的常见表示法，并且确实许多理论模糊了“对于所有”和“乘积”以及“存在”和“总和”之间的区别，因为上述对应关系。
我们快要接近了！
向量：表示依赖元组
现在我们能否编码数值表达式，例如
Σ[n ∈ ℕ]Xⁿ
作为类型表达式吗？
不完全是。虽然我们可以非正式地考虑在 Haskell 中的表达式的含义，例如
Xⁿ，其中
X 是一个类型，
n 是一个自然数，但这是一种滥用符号的方式；这是包含数字的类型表达式：明显不是有效的表达式。
另一方面，有了依赖类型的概念，包含数字的类型恰恰是重点；事实上，依赖元组或“向量”是如何提供
类似于列表访问的实用类型级安全性 的常见示例。向量只是列表以及关于其长度的类型级信息：这正是我们想要的类型表达式，例如
Xⁿ。
在本答案的持续时间中，让我们将其定义为：
Vec X n
这是一种长度为 n 的 X 类型值向量。在技术上，n 并不是一个实际的自然数，而是自然数系统中的一个表示。我们可以用 Peano 风格来表示自然数（Nat），其中零（0）或另一个自然数的后继（S）。对于 n ∈ ℕ，我用 ˻n˼ 来表示代表 n 的 Nat 项。例如，˻3˼ 是 S (S (S 0))。
因此，我们有
|Vec X ˻n˼| = |X|ⁿ
对于任何自然数
n ∈ ℕ。
Nat 类型：将 ℕ 项提升为类型
现在我们可以编码像这样的表达式：
Σ[n ∈ ℕ]Xⁿ
类型。这个特定的表达式会产生一个类型，当然是同构于问题中所识别的
X列表类型。（不仅如此，从范畴论的角度来看，将
X带入上述类型的类型函数 - 即一个函子 - 是与List函子
自然地同构的。）
对于“任意”函数的最后一块拼图是如何编码的。
f : ℕ → ℕ
expressions like
Σ[n ∈ ℕ]f(n)Xⁿ
为了能够将任意系数应用于幂级数。
我们已经理解了代数类型与数字之间的对应关系，使我们能够从类型映射到数字和类型函数映射到数字函数。我们还可以反过来！ - 给定一个自然数，无论是否有依赖类型，显然都有一个可定义的具有那么多项成员的代数类型。我们可以在类型理论之外轻松地通过归纳证明这一点。我们需要的是一种从自然数到类型的映射方法，在系统内部。
一个令人愉悦的认识是，一旦我们拥有了依赖类型，归纳证明和递归构造变得密切相似 - 在许多理论中它们实际上是完全相同的东西。既然我们可以通过归纳证明存在满足我们需求的类型，那么我们不应该能够构造它们吗？
在术语层面上表示类型的几种方法。我将使用一个想象中的 Haskell 风格符号，用“*”表示类型宇宙，本身通常在依赖设置中被认为是一种类型。
同样，表示'ℕ-消除'的记法至少有与依赖类型理论相同的数量。我将使用 Haskell 风格的模式匹配符号。
我们需要一个映射，从Nat到*的α，满足以下条件。
∀n ∈ ℕ.|α ˻n˼| = n.
以下的伪定义足以说明。
data Zero
data Successor a = Z | Suc a
α : Nat -> *
α 0 = Zero
α (S n) = Successor (α n)
因此，我们看到
α的操作镜像了后继函数
S的行为，使其成为一种同态。
Successor是一种类型函数，它将一个类型的成员数加1; 也就是说，对于任何定义大小的
a，
| Successor a | = 1 + | 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)
这到底有多“任意”？通过这种方法，我们不仅受限于整数系数，还受限于自然数。除此之外，对于给定的
Turing Complete依赖类型语言，
f可以是任何函数，我们可以用自然数系数来表示任何解析函数。
我还没有研究过这个与问题中提供的
List X ≅ 1/(1 - X)的交互作用，或者在这种情况下这些负数和非整数“类型”可能具有什么可能的意义。
希望这个答案能够探讨我们可以通过任意类型函数走多远。
Branch x (Branch y Nil Nil) Nil，要么是Branch x Nil (Branch y Nil Nil)。 - Chris Taylor