依赖类型理论和“任意”类型函数
我对这个问题的第一个回答是概念多，细节少，并反映在子问题上，“发生了什么?”这个答案将是相同的，但专注于子问题，“我们可以得到任意类型的函数吗?”
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)问题中提供的情况的相互作用，或者这种负的和非整数的“类型”在这个上下文中可能有什么意义。
希望这个答案能在某种程度上帮助我们探索任意类型的函数能走多远。
