滥用代数数据类型的代数——为什么会这样?

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

已经定义了基本类型

  • 产品•
  • 联盟+
  • 单例X
  • 单位1

用X²表示X•X，用2X表示X+X等等，我们就可以为链表定义代数表达式

__abc0↔__abc1

二叉树:

__abc0↔__abc1

现在，作为一名数学家，我的第一直觉是对这些表达式着迷，并试图求解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个有2个元素的二叉树(第二个元素可以在左边或右边分支)，5个有3个元素的二叉树等等。

我的问题是，我在这里做什么?这些操作似乎不合理(代数数据类型的平方根到底是什么?)，但它们会导致合理的结果。两种代数数据类型的商在计算机科学中有什么意义吗，还是只是符号技巧?

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

30422 次浏览
小开

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

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

小开

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

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 + ...

由于对类型的操作规则与算术操作规则类似，因此可以使用代数方法来帮助您确定如何展开递归关系(因为它并不明显)。

小开
最佳答案

免责声明:当你考虑⊥时，很多东西都不太正确，所以为了简单起见，我将公然忽略这一点。

以下几点:

  • 注意，“并集”可能不是这里A+B的最佳术语——具体来说是< A href="http://en.wikipedia.org/wiki/Disjoint_union" rel="noreferrer"> A 不连接并集这两种类型，因为即使它们的类型相同，双方也可以区分。更常见的术语是简单的“和类型”。

  • 单例类型实际上是所有的单元类型。它们在代数操作下表现相同，更重要的是，存在的信息量仍然被保留。

  • 你可能也想要一个零类型。Haskell将其提供为Void。没有类型为0的值，就像只有一个类型为1的值一样。

这里还少了一个大手术，但我一会儿再讲。

正如你可能已经注意到的，Haskell倾向于借用范畴理论的概念，所有这些都有一个非常直接的解释:

  • 给定对象A和B在Hask中，它们的乘积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) < / em > = < em > < / em >和< em >同样g < / em >。参数性自动保证了通用属性，我选择的不太微妙的名称应该能让您了解这个概念。顺便说一下，(&&&)操作符是在Control.Arrow中定义的。

  • 上述对偶是A+B与注入inl: A→A+B和inr: B→A+B，其中给定任何类型C和函数f: A→C， g: B→C，您可以定义配合f ||| g: A+B→C，使明显等价保持。同样，参数性保证了大多数棘手的部分自动完成。在本例中，标准注入就是Left和Right，而copairing是函数either。

乘积和和类型的许多性质都可以从上面得到。注意，任何单例类型都是Hask的终端对象，任何空类型都是初始对象。

回到前面提到的缺少的操作，在笛卡尔封闭范畴中，你有指数函数对象对应于类别的箭头。箭头是函数，对象是类型为*的类型，并且类型A -> B在类型的代数操作上下文中确实表现为B一个。如果这不是很明显的原因，考虑类型Bool -> A。在只有两个可能输入的情况下，该类型的函数与两个类型为A的值同构，即(A, A)。对于Maybe Bool -> A，我们有三个可能的输入，依此类推。另外，如果我们将上面的copairing定义改写为使用代数符号，我们会得到C一个 × CA -> B0 = CA -> B1。

至于为什么，这一切都是有意义的——特别是为什么你使用幂级数展开是合理的——注意，上面的很多内容都是指一个类型的“居民”(即，具有该类型的不同值)，以演示代数行为。要明确这种观点:

  • 产品类型(A, B)表示分别来自A和B的值。因此，对于任何固定值a :: A，对于B的每个居住者都有一个类型为(A, B)的值。这当然是笛卡尔积，产品类型的居住者数量是各因子的居住者数量的乘积。

  • 和类型Either A B表示来自A或B的值，左分支和右分支是有区别的。如前所述，这是一个不相交的并集，sum类型的居民数量是总和类型的居民数量的总和。

  • 指数类型B -> A表示从类型B的值到类型A的值的映射。对于任何固定实参b :: B，可以将A的任何值赋给它;类型为B -> A的值为每个输入选择一个这样的映射，这相当于A的副本的乘积，与B的常驻数相同，因此是取幂。

虽然一开始很容易将类型视为集合，但在这种情况下实际上并不是很好——我们有不相交的并集，而不是集合的标准并集，没有交集或许多其他集合操作的明显解释，而且我们通常不关心集合成员关系(把它留给类型检查器)。

另一方面，上面的构造花了很多时间讨论计数常驻对象，而列举类型的可能值在这里是一个有用的概念。这很快将我们引导到列举的组合，如果你查阅维基百科的链接文章，你会发现它所做的第一件事是通过生成函数定义“对”和“并”，其意义与乘积和类型完全相同，然后使用完全相同的技术对与Haskell的列表相同的“序列”做同样的事情。

编辑:哦，这里有一个快速的奖金，我认为可以惊人地证明这一点。你在评论中提到，对于树类型T = 1 + T^2，可以推导出标识T^6 = 1，这显然是错误的。然而，T^7 = T 做保留，并且树和树的七元组之间的双射可以直接构造，参见安德烈亚斯·布拉斯的《七棵树合一》。

编辑×2:关于在其他答案中提到的“类型的导数”结构的主题，你可能也喜欢本文来自同一作者，它进一步建立在这个思想上，包括除法的概念和其他有趣的东西。

小开

二叉树由类型半环中的方程T=1+XT^2定义。在构造上，T=(1-sqrt(1-4X))/(2X)由复数半环中的相同方程定义。既然我们在同一类代数结构中解同一个方程那么我们看到一些相似之处也就不足为奇了。

问题是，当我们在复数的半环中推理多项式时，我们通常使用复数构成一个环甚至一个域的事实，因此我们发现自己使用的减法等运算不适用于半环。但是，如果我们有一个规则，允许我们从方程两边消去，我们通常可以从我们的论证中消去减号。这就是菲奥雷和伦斯特所证明的东西，它表明许多关于环的参数可以转换为半环。

这意味着你关于环的许多数学知识可以可靠地转换为类型。因此，一些涉及复数或幂级数的参数(在形式幂级数的环中)可以以完全严格的方式传递到类型中。

然而，故事远不止于此。通过证明两个幂级数相等来证明两种类型相等是一回事。但是您也可以通过检查幂级数中的项来推断类型的信息。我不确定这里的正式声明应该是什么。(我推荐Brent Yorgey在组合物种上的纸，用于一些密切相关的工作，但物种不与类型相同。)

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

玩得开心!

小开
通信进程代数(ACP)处理类似类型的进程表达式。 它提供加法和乘法作为选择和序列的操作符，并带有相关的中性元素。 在这些基础上，还有其他构造的运算符，比如并行和中断。 看到http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes。网上还有一篇论文叫《过程代数简史》

我正在用ACP扩展编程语言。去年4月，我在Scala Days 2012上发表了一篇研究论文，可以在http://code.google.com/p/subscript/上找到

在会议上，我演示了一个调试器运行一个包的并行递归规范:

袋子= A;(Bag&一个)

其中A和A代表输入和输出动作;分号和&号代表序列和并行性。在SkillsMatter上观看视频，可以从之前的链接获得。

一个袋规格更可比

L = 1 + x•L

将

B = 1 + x

ACP使用公理根据选择和顺序定义并行性;参见维基百科的文章。我想知道这个包的比喻是什么意思

L = 1 / (1- x)

ACP风格的编程对于文本解析器和GUI控制器来说非常方便。规范，例如

searchCommand =点击(searchButton) +键(Enter)

cancelCommand =点击(cancelButton) +键(Escape)

通过将“clicked”和“key”隐式化(就像Scala允许的函数一样)，可以更简洁地写下来。因此我们可以这样写:

searchCommand = searchButton +回车

cancelCommand = cancelButton + Escape

右边现在包含的操作数是数据，而不是进程。在这个级别上，没有必要知道哪些隐式细化将这些操作数转换为进程;它们不一定会细化成输入动作;输出动作也将适用，例如在测试机器人的规格中。

进程通过这种方式获得数据作为同伴;因此我创造了“项目代数”这个术语。

小开

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

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

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

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

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

麦克劳林级数的定义

函数f : ℝ → ℝ的麦克劳林级数定义为

f(0) + f'(0)X + (1/2)f''(0)X² + ... + (1/n!)f⁽ⁿ⁾(0)Xⁿ + ...

其中f⁽ⁿ⁾表示f的__abc1阶导数。

为了能够理解用类型解释的Maclaurin系列，我们需要了解如何在类型上下文中解释三件事:

  • 一个(可能是多重)导数
  • 将函数应用到0
  • 像(1/n!)这样的术语

事实证明，从分析中得到的这些概念在类型世界中也有相应的对应。

我所说的“合适的对手”是什么意思?它应该有一种同构的味道——如果我们可以在两个方向上保持真理，那么在一个上下文中可以推导出的事实就可以转移到另一个上下文中。

有类型的微积分

类型表达式的导数是什么意思呢?事实证明，对于一个大型且行为良好(“可微的”)的类型表达式和函子类，存在一个行为足够相似的自然运算，这是一个合适的解释!

为了破坏笑点，与微分类似的操作是制造“单孔上下文”。这是进一步扩展这一点的好地方，但单孔上下文(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分别表示恰好为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'

这可能更可取。

注意:如果用类型和函子的同构类来定义导数，则可以使等式严格而精确。

现在，我们特别注意到，微积分中有关加法、乘法和复合代数运算的规则(通常称为和、积和链规则)恰好反映在“打洞”运算中。此外，在常数表达式或术语__abc0本身中“挖一个洞”的基本情况也表现为微分，因此通过归纳，我们得到了所有代数类型表达式的类微分行为。

现在我们可以解释微分了，类型表达式dⁿe/dxⁿ的nth '导数'是什么意思?它是一个表示n-place上下文的类型:术语，当被类型为x的n术语“填充”时，将产生e。后面还有一个与'(1/n!)'相关的关键观察结果。

类型函子的不变部分:将函数应用于0

我们已经在类型世界中有了0的解释:一个没有成员的空类型。从组合的角度来看，对它应用类型函数意味着什么?更具体地说，假设f是一个类型函数，f(0)是什么样子的?好吧，我们当然不能访问类型为0的任何东西，因此任何需要x的f(x)结构都不可用。剩下的是那些在没有它们的情况下可以访问的术语，我们可以称之为类型的“不变”或“常数”部分。

对于一个显式的例子，以Maybe函子为例，它可以用代数表示为x ↦ 1 + x。当我们将此应用于0时，我们得到1 + 0——它就像1:唯一可能的值是None值。对于列表，类似地，我们只得到与空列表对应的项。

当我们把它带回来并将类型f(0)解释为一个数字时，它可以被认为是在不访问x的情况下可以获得多少类型为f(x)(对于任何x)的项的数:即“类空”项的数量。

把它放在一起:完整的诠释麦克劳林系列

恐怕我想不出将(1/n!)直接解释为类型的合适方法。

但是，如果我们根据上述考虑f⁽ⁿ⁾(0)类型，我们可以看到它可以被解释为类型为f(x)的n0 x的n-位置上下文的类型——也就是说，当我们对它们进行n次“积分”时，结果项具有n1 n xs，不多不少。然后，将类型f⁽ⁿ⁾(0)解释为一个数字(就像在f的Maclaurin系列的系数中一样)只是计算有多少这样的空__abc1位上下文。我们就快到了!

但是(1/n!)在哪里结束?检查类型“分化”的过程向我们表明，当应用多次时，它保留了提取子术语的“顺序”。例如，考虑类型为x × x的术语(x₀, x₁)和在其上“打洞”两次的操作。我们得到了两个序列

(x₀, x₁)  ↝  (_₀, x₁)  ↝  (_₀, _₁)
(x₀, x₁)  ↝  (x₀, _₀)  ↝  (_₁, _₀)
(where _ represents a 'hole')

尽管它们都来自同一个术语，因为有2! = 2种方法可以从两个元素中取两个元素，从而保持顺序。通常，有n!方法从n中获取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

得到Maclaurin级数中X¹的系数。

但是，由于我们确信这些表达式确实是严格的“可微的”，如果只是隐式的，并且由于我们与函数ℝ→ℝ对应，其中导数肯定是唯一的，我们可以放心，即使我们使用“非法”操作获得值，结果也是有效的。

现在，类似地，使用第二个观察结果，由于函数ℝ→ℝ的对应关系(它是同态吗?)，我们知道，只要我们满意函数有是麦克劳林级数，如果我们能找到任何级数都可以，上面列出的原则可以应用于使其严谨。

关于你的函数组合问题，我想链式法则可以给出部分答案。

我不确定这适用于多少haskell风格的adt，但我怀疑它是很多，如果不是全部的话。我发现了一个非常奇妙的证据来证明这一事实，但这页空白处太小了，无法容纳它……

当然，这只是解决问题的一种方法可能还有很多其他方法。

摘要:TL,博士

  • 类型'differentiation'对应于'打洞'。
  • 对0应用函子可以得到该函子的“类空”项。
  • 因此，麦克劳林幂级数(在某种程度上)严格对应于枚举具有一定数量元素的函子类型的成员数量。
  • 隐函数微分使这个更加水密。
  • 导数的唯一性和幂级数的唯一性意味着我们可以篡改细节，这是可行的。
小开

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

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

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

所以求和

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

可以写成

Σ[i ∈ ℕ]aᵢXⁱ

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

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

对这些表达式有直接表示的类型理论是“相关”类型理论:具有相关类型的理论。当然，我们有依赖于术语的术语，在Haskell等语言中，有类型函数和类型量化，术语和类型依赖于类型。在依赖设置中，我们还有依赖于术语的类型。Haskell不是一种依赖类型语言，尽管依赖类型的许多特性可以模拟通过稍微折磨一下语言。

Curry-Howard和依赖型

“Curry-Howard同构”最初是作为一种观察，即简单类型lambda演算的术语和类型判断规则完全对应于应用于直觉命题逻辑的自然演绎(由Gentzen制定)，类型取代命题，术语取代证明，尽管这两者是独立发明/发现的。从那时起，它一直是类型理论家的巨大灵感来源。要考虑的最明显的事情之一是，命题逻辑的这种对应是否以及如何可以扩展到谓词或更高阶逻辑。依赖类型理论最初产生于这一探索途径。

有关简单类型lambda演算的Curry-Howard同构的介绍，请参见在这里。举个例子，如果我们想证明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)的证明由什么组成?我们可以把它看作是一个证明函数，用terms (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)的术语。

< p >符号: 我将使用

∀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)

是(x, p)和p : P(x)对的类型，因此给定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是一个自然数，但这是一种符号滥用;这是一个包含数字的类型表达式:不显然是一个有效的表达式。

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

在此回答期间，让

Vec X n

__abc1类型值的长度为-n向量的类型。

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

然后我们有

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

对于任何n ∈ ℕ。

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

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

Σ[n ∈ ℕ]Xⁿ

作为类型。这个特殊的表达式会产生一个类型，当然它与问题中确定的X的列表类型同构。(不仅如此，从范畴论的角度来看，类型函数——它是一个函子——将X转换为上面的类型就是< em > < / em >自然同构转换为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的行为，使其成为一种同态。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

是必需的。

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

“任意”功能?

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

该系列

Σ[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可以是任何东西，给定具有依赖类型的图灵完全的语言，我们可以表示任何具有自然数系数的分析函数。

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

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


提交答案