滥用代数数据类型的代数 - 为什么这有效？-Java 学习之路

267

代数数据类型的“代数”表达式对于具有数学背景的人来说非常具有启发性 . 让我试着解释一下我的意思 .

定义了基本类型

产品 •
联盟 +
Singleton X
单位 1

并使用 X² 用于 X•X 和 2X 用于 X+X 等等，然后我们可以定义代数表达式，例如链表

data List a = Nil | Cons a (List a) ↔ L = 1 + X • L

和二叉树：

data Tree a = Nil | Branch a (Tree a) (Tree a) ↔ T = 1 + X • T²

现在，我作为数学家的第一直觉是坚持使用这些表达式，并试图解决 L 和 T . 我可以通过重复替换来做到这一点，但似乎更容易滥用符号，并假装我可以随意重新排列 . 例如，对于链接列表：

L = 1 + X • L

(1 - X) • L = 1

L = 1 / (1 - X) = 1 + X + X² + X³ + ...

我使用 1 / (1 - X) 的幂级数展开以完全不合理的方式得出一个有趣的结果，即 L 类型是 Nil ，或者它包含1个元素，或者它包含2个元素，或3等 .

如果我们为二叉树做它会变得更有趣：

T = 1 + X • T²

X • T² - T + 1 = 0

T = (1 - √(1 - 4 • X)) / (2 • X)

T = 1 + X + 2 • X² + 5 • X³ + 14 • X⁴ + ...

再次，使用电源系列扩展（使用Wolfram Alpha完成） . 这表达了非显而易见（对我来说）的事实，即只有一个二元树有1个元素，2个二叉树有两个元素（第二个元素可以在左边或右边的分支上），5个二叉树有三个元素等 .

所以我的问题是 - 我在这做什么？这些操作似乎是不合理的（无论如何，代数数据类型的平方根究竟是什么？）但它们会产生明显的结果 . 两种代数数据类型的商是否在计算机科学中有任何意义，还是仅仅是符号诡计？

而且，或许更有趣的是，是否可以扩展这些想法？是否存在类型代数的理论，例如，允许类型上的任意函数，或类型是否需要幂级数表示？如果你可以定义一类函数，那么函数的组合是否有任何意义？

7 回答

129
免责声明：当你考虑到⊥时，很多这种方法并没有真正起作用，所以为了简单起见，我会公然无视这一点 .

一些初步要点：
- 注意"union"可能不是这里A B的最佳术语 - 这两种类型的具体是a disjoint union，因为即使它们的类型相同，双方也是相同的 . 对于它的 Value ，更常见的术语是"sum type" .
- 单身类型实际上是所有单位类型 . 它们在代数操作下的行为相同，更重要的是，仍然保留了存在的信息量 .
- 您可能也想要零类型 . 没有标准的，但最常见的名称是 Void . 没有类型为零的值，就像有一个类型为1的值一样 .
这里仍然缺少一个主要的操作，但我马上回过头来看看 .

正如您可能已经注意到的那样，Haskell倾向于从类别理论中借用概念，并且所有上述内容都具有非常直接的解释：
- 给定 Hask 中的对象A和B，它们的乘积A×B是唯一的（直到同构）类型，允许两个投影fst：A×B→A和snd：A×B→B，其中给出任何类型C和函数f：C→A，g：C→B你可以定义配对f &&& g：C→A×B，使得fst∘（f &&&g）= f，同样g . 参数化自动保证了通用属性，而我不太精确的名称选择应该会给你一个想法 . 顺便说一句， (&&&) 运算符在 Control.Arrow 中定义 .
- 以上的对偶是具有注射inl的副产品AB：A→AB和inr：B→AB，其中给出任何类型C和函数f：A→C，g：B→C，您可以定义共同的f | || g：A B→C使得明显的等价性成立 . 同样，参数化自动保证了大部分棘手的部分 . 在这种情况下，标准注射只是 Left 和 Right ，而copairing是函数 either .
产品和总和类型的许多属性可以从上面得出 . 请注意，任何单例类型都是 Hask 的终端对象，任何空类型都是初始对象 .

返回上述缺失的操作，在cartesian closed category中，您有exponential objects，对应于该类别的箭头 . 我们的箭头是函数，我们的对象是类型 * 的类型，类型 A -> B 在类型的代数操作的上下文中确实表现为BA . 如果为什么这应该成立并不明显，请考虑类型 Bool -> A . 只有两个可能的输入，该类型的函数与两个 A 类型的值同构，即 (A, A) . 对于 Maybe Bool -> A ，我们有三个可能的输入，依此类推 . 另外，请注意，如果我们将上面的共同定义改为使用代数表示法，我们得到身份CA×CB = CA B.

至于为什么这一切都有意义 - 特别是为什么你使用幂级数扩展是合理的 - 注意上面的大部分内容是指一种类型的"inhabitants"（即具有该类型的不同值）以便证明代数行为 . 为了使这个观点明确：
- 产品类型 (A, B) 表示独立于 A 和 B 的值 . 因此，对于任何固定值 a :: A ， B 的每个居民都有一个类型为 (A, B) 的值 . 这当然是笛卡儿产品，产品类型的居民数量是因素居民数量的乘积 .
- 和类型 Either A B 表示来自 A 或 B 的值，左右分支可区分 . 如前所述，这是一个不相交的联盟，总和类型的居民数量是总和的居民数量的总和 .
- 指数类型 B -> A 表示从类型 B 的值到类型 A 的值的映射 . 对于任何固定参数 b :: B ，可以为其分配 A 的任何值;类型为 B -> A 的值为每个输入选择一个这样的映射，这相当于 A 的多个副本的产品，因为 B 具有居民，因此取幂 .
虽然最初将类型视为集合很诱人，但在这种情况下实际上并不能很好地工作 - 我们有不相交的联合而不是集合的标准联合，对交集或许多其他集合操作没有明显的解释，我们通常不关心集合成员资格（将其留给类型检查器） .

另一方面，上面的结构花了很多时间讨论计算居民，并且枚举类型的可能值是一个有用的概念 . 这很快就会引导我们enumerative combinatorics，如果你查阅链接的维基百科文章，你会发现它所做的第一件事就是通过generating functions定义"pairs"和"unions"与产品和总和类型完全相同，然后执行对于"sequences"来说，它与Haskell的列表完全相同，使用了与您完全相同的技术 .

Edit: 哦，这是一个快速的奖金，我认为这一点非常引人注目 . 您在评论中提到，对于树类型 T = 1 + T^2 ，您可以派生标识 T^6 = 1 ，这显然是错误的 . 但是， T^7 = T 确实存在，并且可以直接构建树和七元组树之间的双射，参见Andreas Blass's "Seven Trees in One" .

Edit×2: 关于其他答案中提到的"derivative of a type"构造的主题，你可能也会喜欢this paper from the same author，它 Build 在这个想法的基础上，包括分裂的概念和其他有趣的东西 .
回复于 2024-04-26T11:14:18+08:00
41

在类型的半环中，二进制树由等式 T=1+XT^2 定义 . 通过构造， T=(1-sqrt(1-4X))/(2X) 在复数的半环中由相同的等式定义 . 因此，鉴于我们看到一些相似之处，我们感到惊讶 .

问题在于，当我们在复杂数字的半环中推理多项式时，我们通常使用复数形成环或甚至是场的事实，因此我们发现自己使用不适用于半环的操作，例如减法 . 但是如果我们有一条允许我们从方程的两边取消的规则，我们通常可以从我们的论证中消除减法 . 这是Fiore and Leinster证明了许多关于环的争论可以转移到半环的事情 .

这意味着您对戒指的大量数学知识可以可靠地转移到类型 . 因此，一些涉及复数或幂级数的论证（在正式权力系列的环中）可以以完全严格的方式转移到类型 .

然而，有一件事要证明两种类型相等（说）通过显示两个幂级数是相等的 . 但您也可以通过检查电源系列中的术语来推断有关类型的信息 . 我_8008221_在combinatorial species对于一些密切相关但物种与类型不同的工作 . ）

我发现完全令人兴奋的是你发现的东西可以扩展到微积分 . 关于微积分的定理可以转移到类型的半环节 . 实际上，甚至关于有限差分的论证都可以转移，你会发现数值分析中的经典定理在类型理论中有解释 .

玩得开心！

回复于 2024-04-26T11:14:18+08:00
3
似乎你所做的只是扩展递归关系 .
```
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 + ...
```
由于类型操作的规则就像算术运算规则一样，你可以使用代数方法来帮助你弄清楚如何扩展递归关系（因为它并不明显） .
回复于 2024-04-26T11:14:18+08:00
18

我没有't have a complete answer, but these manipulations tend to '只是工作' . 相关论文可能是Objects of Categories as Complex Numbers by Fiore and Leinster - 我在阅读sigfpe's blog on a related subject时遇到过那篇论文 . 该博客的其余部分是一个金矿的类似想法，值得一试！

顺便说一下，您还可以区分数据类型 - 这将为您提供适合数据类型的Zipper！

回复于 2024-04-26T11:14:18+08:00
10

通信过程代数（ACP）处理类似的过程表达式 . 它提供了加法和乘法作为选择和序列的运算符，以及相关的中性元素 . 基于这些，有其他构造的运算符，例如并行和中断 . 见http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes . 还有一篇名为"A Brief History of Process Algebra"的在线论文 .

我正致力于使用ACP扩展编程语言 . 去年四月，我在2012年Scala Days上发表了一篇研究论文，发表于http://code.google.com/p/subscript/

在 Session 上，我演示了一个运行并行递归规范的调试器：

Bag = A; （袋及一）

其中A和a代表输入和输出动作;分号和＆符号代表顺序和并行 . 查看SkillsMatter上的视频，可从上一个链接访问 .

一个袋子规格更可比

L = 1 X•L

将会

B = 1 X＆B

ACP使用公理在选择和顺序方面定义并行性;请参阅维基百科文章 . 我想知道包包的类比是什么

L = 1 /（1-X）

ACP样式编程对于文本解析器和GUI控制器很方便 . 规格如

searchCommand = clicked（searchButton）键（回车）

cancelCommand = clicked（cancelButton）键（Escape）

可以通过使两个细化“clicked”和“key”隐含（比如Scala允许的函数）来更简洁地写下来 . 因此我们可以写：

searchCommand = searchButton输入

cancelCommand = cancelButton Escape

右侧现在包含作为数据的操作数，而不是进程 . 在这个级别，没有必要知道隐式改进将把这些操作数转换为进程;他们不一定会改进投入行动;输出动作也适用，例如在测试机器人的规范中 .

进程以数据的形式获得数据;因此，我称之为“项代数” .

回复于 2024-04-26T11:14:18+08:00
6
微积分和Maclaurin系列的类型

这是另一个次要的补充 - 组合扩展中为什么系列扩展中的系数应该是'work'，特别是关注可以使用微积分的Taylor-Maclaurin方法得出的系列 . 注意：您给出的操纵列表类型的示例系列扩展是Maclaurin系列 .

由于其他答案和评论涉及代数类型表达式（总和，产品和指数）的行为，因此这个答案将忽略该细节并专注于类型“微积分” .

在这个答案中你可能会注意到引号中的引号很重要 . 有两个原因：
- 我们的业务是从一个域向另一个域的实体提供解释，并且以这种方式划分这样的外国概念似乎是恰当的 .
- 一些概念将能够更严格地形式化，但形状和想法似乎比细节更重要（并且占用更少的空间） .
Maclaurin系列的定义

函数 f : ℝ → ℝ 的Maclaurin series定义为
```
f(0) + f'(0)X + (1/2)f''(0)X² + ... + (1/n!)f⁽ⁿ⁾(0)Xⁿ + ...
```
其中 f⁽ⁿ⁾ 表示 f 的 n 衍生物 .

为了能够理解用类型解释的Maclaurin系列，我们需要理解我们如何在类型上下文中解释三件事：
- 一个（可能是多个）衍生物
- 将函数应用于 0
- 像 (1/n!) 这样的术语
事实证明，这些来自分析的概念在类型世界中具有合适的对应物 .

“合适的对手”是什么意思？它应该具有同构的味道 - 如果我们能够在两个方向上保存真理，那么在一个上下文中可导出的事实可以转移到另一个上下文中 .

微积分与类型

那么类型表达式的导数是什么意思呢？事实证明，对于一个大型且表现良好（“可微分”）类型的表达式和仿函数，有一种自然操作，其行为类似于足以成为合适的解释！

为了破坏妙语，类似于差异化的操作是制作'one-hole contexts' . This是进一步扩展这一特定点的绝佳场所，但单洞上下文（ da/dx ）的基本概念是它表示从一个术语（类型 a ）中提取特定类型（ x ）的单个子项目的结果 . ），保留所有其他信息，包括确定子项目原始位置所必需的信息 . 例如，表示列表的单孔上下文的一种方法是使用两个列表：一个用于在提取的一个之前的项目，一个用于之后的项目 .

通过区分识别该操作的动机来自以下观察 . 我们写 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 表示只有一个和的类型确切地说是零居民，而 + 和 × 像往常一样代表总和和产品类型 . f 和 g 用于表示类型函数或类型表达形式， [f(x)/a] 表示在前面的表达式中为 a 替换 f(x) 的操作 .

这可以用无点样式编写，编写 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'
```
这可能是优选的 .

注意，如果我们使用类型和仿函数的同构类来定义导数，则可以使等式变得严格和精确 .

现在，我们特别注意到微积分中有关加法，乘法和组合的代数运算的规则（通常称为求和，产品和链规则）完全由'making a hole'的操作反映出来 . 此外，常量表达式中'making a hole'的基本情况或术语 x 本身也表现为微分，因此通过归纳，我们得到所有代数类型表达式的类似区分的行为 .

现在我们可以解释分化， n 的'derivative'是什么类型表达式， dⁿe/dxⁿ 是什么意思？它是一个表示 n -place contexts的类型：当'filled'与 n 类型 x 的条款产生 e 时，这些术语 . 还有另一个与“ (1/n!) ”相关的重要观察结果 .

类型仿函数的不变部分：将函数应用于0

我们已经在类型世界中对 0 进行了解释：没有成员的空类型 . 从组合的角度来看，将类型函数应用于它是什么意思？更具体地说，假设 f 是一个类型函数， f(0) 是什么样的？好吧，我们当然无法访问 0 类型的任何内容，因此任何需要 x 的 f(x) 构造都不可用 . 剩下的是那些在他们缺席时可以访问的术语，我们可以将其称为该类型的'invariant'或'constant'部分 .

对于一个明确的例子，取 Maybe 仿函数，它可以代数表示为 x ↦ 1 + x . 当我们将其应用于 0 时，我们得到 1 + 0 - 它就像 1 ：唯一可能的值是 None 值 . 对于列表，类似地，我们只获得对应于空列表的术语 .

当我们将它返回并将类型 f(0) 解释为数字时，可以将其视为可以在不访问 x 的情况下获得 f(x) （对于任何 x ）类型的条数的计数：即'empty-like'条款的数量 .

把它放在一起：完整解释Maclaurin系列

我'm afraid I can' t想到 (1/n!) 作为一种适当的直接解释 .

但是，如果我们根据上述情况考虑类型 f⁽ⁿ⁾(0) ，我们会看到它可以被解释为类型为 f(x) 的 n -place上下文的类型，它不包含 x - 也就是说，当我们'integrate'时他们 n 次，由此产生的期限恰好是 n x ，不多也不少 . 然后将类型 f⁽ⁿ⁾(0) 解释为数字（如Maclaurin系列的 f 的系数）只是计算出有多少这样的空 n -place上下文 . 我们快到了！

但 (1/n!) 最终会在哪里？检查'differentiation'类型的过程向我们显示，当多次应用时，它会保留'order'，其中提取了子项 . 例如，考虑 x × x 类型的术语 (x₀, x₁) 和两次'making a hole'的操作 . 我们得到两个序列
```
(x₀, x₁)  ↝  (_₀, x₁)  ↝  (_₀, _₁)
(x₀, x₁)  ↝  (x₀, _₀)  ↝  (_₁, _₀)
(where _ represents a 'hole')
```
即使两者都来自同一个词，因为有两种方法可以从两个中取两个元素，保留顺序 . 一般来说，there are n!方法从 n 获取 n 元素 . 因此，为了获得具有 n 元素的仿函数类型的配置数量，我们必须计算类型 f⁽ⁿ⁾(0) 并除以 n! ，与Maclaurin系列的系数完全相同 .

因此，除以 n! 就可以简单地解释为自身 .

最后的想法：'递归'定义和解析性

首先，一些观察：
- 如果函数f：ℝ→ℝ具有导数，则该导数是唯一的
- 类似地，如果函数f：ℝ→ℝ是解析的，它只有一个相应的多项式系列
由于我们有链规则，我们可以使用implicit differentiation，如果我们将类型导数形式化为同构类 . 但隐式分化不需要任何外来机动，如减法或除法！所以我们可以用它来分析递归类型定义 . 以列表为例，我们有
```
L(X) ≅ 1 + X × L(X)
L'(X) = X × L'(X) + L(X)
```
然后我们可以评估
```
L'(0) = L(0) = 1
```
在Maclaurin系列中获得 X¹ 的系数 .

但是因为我们确信这些表达式确实是严格“可区分的”，如果只是隐含的，并且因为我们与函数ℝ→ℝ有对应关系，其中衍生品当然是独一无二的，我们可以放心，即使我们使用“非法”操作获得 Value ，结果也是有效的 .

现在，类似地，使用第二个观察，由于函数ℝ→correspondence的对应关系（它是同态吗？），我们知道，如果我们对函数具有Maclaurin系列感到满意，如果我们可以找到任何系列总而言之，上述原则可以应用于严谨 .

至于你关于函数组合的问题，我认为链规则提供了部分答案 .

我不确定这适用于多少Haskell风格的ADT，但我怀疑它有很多，如果不是全部的话 . 我发现了这个事实的一个真正奇妙的证据，但是这个边际太小而不能包含它......

现在，当然这只是解决这里发生的事情的一种方法，可能还有很多其他方法 .

摘要：TL; DR
- type 'differentiation'对应'making a hole' .
- 将一个仿函数应用于 0 ，获取该仿函数的'empty-like'条款 .
- Maclaurin幂系列因此（有些）严格对应于枚举具有一定数量元素的仿函数类型的成员数 .
- implicit differentiation使这更加无懈可击 .
- 衍生物的独特性和幂级数的独特性意味着我们可以捏造细节并且它起作用 .
回复于 2024-04-26T11:14:18+08:00
20
依赖型理论和'任意'型函数

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

sum和product的代数运算的一个扩展是所谓的'large operators'，它代表序列的总和和乘积（或者更一般地说，是域上函数的和与乘积），通常分别写成 Σ 和 Π . 见Sigma Notation .

所以总和
```
a₀ + a₁X + a₂X² + ...
```
可能是写的
```
Σ[i ∈ ℕ]aᵢXⁱ
```
例如， a 是一些实数序列 . 该产品将使用 Π 而不是 Σ 来表示 .

当你从远处看时，这种表达式看起来很像 X 中的'arbitrary'函数;我们当然限于可表达系列及其相关的分析功能 . 这是类型理论中的表示的候选者吗？非也！

具有这些表达式的直接表征的类型理论类是'dependent'类型理论的类别：具有依赖类型的理论 . 当然，我们的术语依赖于术语，并且在Haskell等语言中具有类型函数和类型量化，术语和类型取决于类型 . 在依赖设置中，我们还根据术语具有类型 . Haskell不是依赖类型的语言，尽管可以模拟依赖类型的许多功能by torturing the language a bit .

Curry-Howard和依赖类型

“库里 - 霍华德同构”开始的生活是一种观察，即简单类型的lambda演算的术语和类型判断规则完全对应于应用于直觉主义命题逻辑的自然演绎（由Gentzen制定），类型代替命题尽管两者是独立发明/发现的，但代替证据的术语 . 从那以后，它一直是类型理论家的巨大灵感来源 . 要考虑的最明显的事情之一是命题逻辑的这种对应关系是否以及如何可以扩展到谓词或更高阶逻辑 . 依赖型理论最初源于这种探索途径 .

有关简单类型lambda演算的Curry-Howard同构的介绍，请参阅here . 举个例子，如果我们要证明 A ∧ B ，我们必须证明 A 并证明 B ;合并证明只是一对证明：每个合并一个 .

在自然演绎中：
```
Γ ⊢ A    Γ ⊢ B
Γ ⊢ A ∧ B
```
在简单类型的lambda演算中：
```
Γ ⊢ a : A    Γ ⊢ b : B
Γ ⊢ (a, b) : A × B
```
∨ 和和类型， → 和函数类型以及各种消除规则存在类似的对应关系 .

无法证实的（直觉上错误的）命题对应于无人居住的类型 .

通过类型作为逻辑命题的类比，我们可以开始考虑如何在类型世界中建模谓词 . 有许多方法可以形式化（对于广泛使用的标准，参见Martin-Löf的直觉类型理论），但抽象方法通常观察到谓词就像一个带有自由项变量的命题，或者，将命题用于命题 . 如果我们允许类型表达式包含术语，那么lambda演算风格的处理立即呈现为一种可能性！

只考虑建设性的证据，是什么构成 ∀x ∈ X.P(x) 的证明？我们可以将其视为证明函数，将术语（ x ）作为其相应命题的证明（ P(x) ） . 所以类型的成员（证明）（命题） ∀x : X.P(x) 是'dependent functions'，其中 x 中的每个 x 都给出 P(x) 类型的术语 .

∃x ∈ X.P(x) 怎么样？我们需要 X ， x 的任何成员以及 P(x) 的证明 . 所以类型（命题） ∃x : X.P(x) 的成员（证明）是'dependent pairs'： X 中的一个杰出术语 x ，以及 P(x) 类型的术语 .

符号：我会用
```
∀x ∈ X...
```
关于类 X 的成员的实际陈述，以及
```
∀x : X...
```
对于与 X 类型的通用量化相对应的类型表达式 . 同样适用于 ∃ .

组合注意事项：产品和总和

除了与命题类型的Curry-Howard对应，我们还有代数类型与数字和函数的组合对应，这是这个问题的主要观点 . 令人高兴的是，这可以扩展到上面列出的依赖类型！

我将使用模数表示法
```
|A|
```
表示 A 类型的'size'，以明确问题中列出的对应关系，类型和数字之间的对应关系 . 请注意，这是理论之外的概念;我并不声称语言中需要任何此类运算符 .

让我们计算一下类型的可能（完全简化的，规范的）成员
```
∀x : X.P(x)
```
这是将 X 类型的术语 x 与 P(x) 类型的术语相关联的函数类型 . 每个此类函数必须具有 X 的每个项的输出，并且此输出必须是特定类型 . 对于 X 中的每个 x ，然后，这将给出 |P(x)| 'choices'的输出 .

妙语是
```
|∀x : X.P(x)| = Π[x : X]|P(x)|
```
如果 X 是 IO () ，这当然没有多大意义，但适用于代数类型 .

同样，一个类型的术语
```
∃x : X.P(x)
```
是 (x, p) 与 p : P(x) 的对的类型，所以在 X 中给出任何 x ，我们可以与 P(x) 的任何成员构造一个合适的对，给出 |P(x)| 'choices' .

因此，
```
|∃x : X.P(x)| = Σ[x : X]|P(x)|
```
同样的警告 .

这证明了使用符号 Π 和 Σ 的理论中依赖类型的通用符号，并且由于上述对应关系，实际上许多理论模糊了'for all'和'product'之间以及'there is'和'sum'之间的区别 .

我们越来越近了！

Vectors：表示依赖元组

我们现在可以编码数字表达式
```
Σ[n ∈ ℕ]Xⁿ
```
作为类型表达式？

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

另一方面，对于图片中的从属类型，包含数字的类型恰恰是重点;事实上，依赖元组或'vectors'是一个非常常见的例子，说明依赖类型如何提供pragmatic type-level safety for operations like list access . 向量只是一个列表以及有关其长度的类型级别信息：正是我们所追求的类型表达式如 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 带到上面的类型是naturally isomorphic到List函子 . ）

“任意”功能的最后一个难题是如何进行编码
```
f : ℕ → ℕ
```
表达式如
```
Σ[n ∈ ℕ]f(n)Xⁿ
```
这样我们就可以将任意系数应用于幂级数 .

我们已经理解了代数类型与数字的对应关系，允许我们从类型映射到数字，并将类型函数映射到数字函数 . 我们也可以走另一条路！ - 采用自然数，显然有一个可定义的代数类型，有许多术语成员，无论我们是否有依赖类型 . 我们可以通过归纳在类型理论之外轻松证明这一点 . 我们需要的是一种从系统内部的自然数字到类型进行映射的方法 .

一个令人愉快的认识是，一旦我们有依赖类型，通过归纳证明和通过递归构造变得非常相似 - 实际上它们在许多理论中是完全相同的 . 因为我们可以通过归纳证明存在类型如果我们无法构建它们，那么它们能满足我们的需求吗？

有几种方法可以在术语级别表示类型 . 我将在这里使用带有 * 的虚构Haskellish表示法作为类型的宇宙，它本身通常被认为是依赖环境中的一种类型 .

同样，至少还有尽可能多的方法来表示“ ℕ -消除”，因为存在依赖类型理论 . 我将使用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 的行为，使其成为一种同态 . Successor 是一个类型函数，其中'adds one'为一个类型的成员数;也就是说， |Successor 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)
```
这是怎么回事'arbitrary'？我们不仅限于这种方法的整数系数，而且还限于自然数 . 除此之外， f 可以是任何东西，给定具有依赖类型的Turing Complete语言，我们可以用自然数系数表示任何分析函数 .

我没有调查过这种情况的相互作用，例如 List X ≅ 1/(1 - X) 问题中提供的情况，或者在这种情况下可能有什么意义，如负面和非整数'types' .

希望这个答案在某种程度上可以探索我们可以使用任意类型函数 .
回复于 2024-04-26T11:14:18+08:00

滥用代数数据类型的代数 - 为什么这有效？

7 回答

微积分和Maclaurin系列的类型

Maclaurin系列的定义

微积分与类型

类型仿函数的不变部分：将函数应用于0

把它放在一起：完整解释Maclaurin系列

最后的想法：'递归'定义和解析性

摘要：TL; DR

依赖型理论和'任意'型函数

Curry-Howard和依赖类型

组合注意事项：产品和总和

Vectors：表示依赖元组

Nat类型：促进ℕ术语到类型

'任意'功能？

相关问题