滥用代数数据types的代数 – 为什么这会起作用？

代数数据types的“代数”expression式对于具有math背景的人来说看起来非常具有启发性。 让我试着解释我的意思。

定义了基本types

• 产品•
• 联盟+
• 辛格尔顿X
• 第一单元

对X+X使用简写X²代表X•X和2X ，然后我们可以定义代数expression式，例如链表

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

和二叉树：

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

现在，作为一个math家，我的第一本能就是坚持这些expression式，并试着解决L和T 我可以通过反复的replace来做到这一点，但是这样做似乎更容易滥用这个表示法，并假装我可以随意重新排列它。 例如，对于一个链表：

L = 1 + X • L

(1 - X) • L = 1

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

我已经用完全不合理的方式使用1 / (1 - X)的幂级数展开来得到一个有趣的结果，即一个Ltypes是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完成）。 这表示了对于一个元素只有一个二叉树，有两个元素的两个二叉树（第二个元素可以在左边或右边的分支上），具有三个元素的5个二叉树等非显而易见的事实。

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

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

Answer 1

免责声明：当你对⊥进行解释时，很多事情并不是很正确，所以为了简单起见，我会公然地忽视这一点。

几个初始点：

• 请注意，“联合”在这里可能不是A + B的最佳术语 – 这就是两种types的不相交联合 ，因为即使types相同，双方也是有区别的。 对于什么是值得的，更常见的术语是“总和types”。

• 单身types实际上是所有单位types。 它们在代数操作下performance相同，更重要的是，信息量仍然保留。

• 你可能也想要一个零types。 没有一个标准的，但最常见的名字是Void 。 没有types为零的值，就像有一个types为1的值。

这里仍然有一个重大的操作，但我会立即回到这一点。

正如你可能已经注意到的那样，Haskell倾向于借用分类理论中的概念，所有上述都有一个非常直接的解释：

• 给定Hask中的对象A和B，其产品A×B是允许两个投影fst ：A×B→A和snd ：A×B→B的唯一（同构）types，其中给定任意typesC和函数f ：C→A， g ：C→B你可以定义配对f &&& g ：C→A×B使得fst∘（f &&& g） = f ，同样对于g 。 参数性自动保证了通用属性，而我对名称的低微select应该给你一个想法。 (&&&)运算符在Control.Arrow定义。

• 上面的对偶是A + B的副产品，其中A→A + B和inr ：B→A + B，其中给定任意typesC和函数f ：A→C， g ：B→C，可以定义共同的f

Answer 2

g ：A + B→C使得明显的等价性成立。 同样，参数保证了大部分棘手的部分。 在这种情况下，标准注射只是Left和Right ，并且共同作用也是。

产品和总和types的许多属性可以从上面得出。 请注意，任何单身types都是Hask的terminal对象，任何空types都是初始对象。

回到前面提到的缺失操作，在笛卡儿式封闭的类别中，您有对应于类别箭头的指数对象 。 我们的箭头是函数，我们的对象是带有*的types，而typesA -> B在types的代数操作的上下文中确实performance为B ^A。 如果不明显，为什么这应该保持，考虑typesBool -> A 只有两个可能的input，这种types的函数是同构于A型A两个值，即(A, A) 。 对于Maybe Bool -> A我们有三个可能的input，依此类推。 另外，请注意，如果我们将上面的共同定义改为使用代数符号，我们可以得到C ^A ×C ^B = C ^{A + B}的标识。

至于为什么这一切都是有道理的 – 特别是为什么你使用幂级数展开是合理的 – 注意，上面的大部分指的是一种types的“居民”（即，具有这种types的不同值）展示代数行为。 为了明确这个观点：

• 产品types(A, B)代表A和B各自独立的值。 因此，对于任何固定值a :: A ，每个B居民有一个types的值(A, B) 。 这当然是笛卡儿的产品，而产品types的居民数是这些因素的居民人数的乘积。

• 总和typesEither AB表示来自A或者B的值，左边和右边的分支被区分。 如前所述，这是一个不相交的联盟，而和types的居民的数目是被征求人的总和。

• 指数typesB -> A表示从typesB的值到typesA值的映射。 对于任何固定参数b :: B ， A任何值都可以赋值给它; 一个B -> Atypes的值B -> A为每个inputselect一个这样的映射，相当于B有居民的A许多拷贝的乘积，因此取幂。

尽pipe首先将types视为集合是诱人的，但在这种情况下实际上并不能很好地工作 – 我们有联合而不是标准的联合集合，对交集或其他集合操作没有明显的解释。通常不关心设置的成员（把它留给types检查器）。

另一方面，上面的build筑花费了大量时间来谈论居民的数量 ， 列举一种types的可能的价值在这里是一个有用的概念。 这很快将我们引向枚举组合 ，如果你参考链接的维基百科文章，你会发现它所做的第一件事情之一是定义“对”和“联合”与产品和总和types完全一样的意义上，通过生成函数 ，然后使用与您所做的相同的技术对与Haskell列表相同的“序列”执行相同的操作。

---

编辑：噢，这里有一个快速的奖金，我认为这一点显而易见。 你在评论中提到，对于树型T = 1 + T^2你可以推导出T^6 = 1的标识，这显然是错误的。 然而， T^7 = T 确实成立，并且可以直接构build树与七元组之间的双射。 安德烈亚斯·布拉斯的“七树一体” 。

编辑×2：关于其他答案中提到的“types派生”构造的主题，你也可以从同一作者那里得到本文的进一步构思，包括分裂的概念和其他有趣的东西。

Answer 3

二叉树由types的半环中的方程T=1+XT^2定义。 通过构造， T=(1-sqrt(1-4X))/(2X)由复数半数中的相同方程定义。 所以考虑到我们在相同的代数结构类中解决同样的方程，我们看到一些相似之处实际上不应该是令人惊讶的。

值得注意的是，当我们推导复数的半环上的多项式时，我们通常使用复数形成一个环或甚至一个场的事实，所以我们发现我们使用了不适用于半环的减法等操作。 但是，如果我们有一条规则允许我们从等式的两边取消，我们通常可以从我们的论点中消除相减。 这是Fiore和Leinstercertificate的那种事实，表明关于戒指的许多争论可以转化为半环。

这意味着你很多关于环的math知识都可以可靠地转换成types。 因此，一些涉及复数或幂级数的论证（在正式幂级数的环中）可以以完全严格的方式inheritance到types。

然而，这个故事还有更多。 通过certificate两个幂级数是相等的，certificate两种types是平等的（比如说）是一回事。 但是，您也可以通过检查幂级数中的术语来推断有关types的信息。 我不确定这里的正式声明应该是什么。 （我推荐Brent Yorgey关于组合物种的论文 ，关于一些与物种密切相关的工作，但是物种与types不一样。）

我发现令人兴奋的是，你发现的东西可以扩展到微积分。 微积分的定理可以转移到types的半环上。 事实上，即使有关有限差异的争论也可以被转移，你会发现数值分析中的经典定理在types理论中有解释。

玩的开心！

Answer 4

看来，你所做的只是扩大重复关系。

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

而且由于这些types的操作规则就像算术运算的规则一样工作，所以可以用代数的方法来帮助你找出如何扩大recursion关系（因为它并不明显）。

Answer 5

我没有一个完整的答案，但这些操纵往往是“正常工作”。 一篇相关的论文可能是Fiore和Leinster的复数分类对象 – 我在阅读sigfpe关于相关主题的博客时偶然发现了这个问题 。 该博客的其余部分是类似的想法的金矿，值得一试！

您还可以区分数据types，顺便说一句 – 这将为您提供相应的数据types的Zipper！

Answer 6

通信过程代数（ACP）处理类似的过程expression式。 它提供了加法和乘法作为运算符的select和顺序，以及相关的中性元素。 基于这些，还有其他构造的运算符，比如并行和中断。 请参阅http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes 。 网上也有一篇名为“进程代数简史”的论文。

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

在会议上，我演示了一个运行并行recursion规范的debugging器：

袋= A; （袋及一）

A和A为投入和产出行动的立场; 分号和符号代表序列和并行性。 在SkillsMatter上查看video，从上一个链接可以find。

一个袋子规格更可比

L = 1 + X·L

将会

B = 1 + X＆B

ACP根据select和使用公理的顺序来定义并行性; 看维基百科的文章。 我想知道这个包的类比是什么

L = 1 /（1-X）

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

searchCommand =点击（searchButton）+键（回车）

cancelCommand =点击（cancelButton）+键（Escape）

可以通过使两个优化“点击”和“键”隐式（比如Scala允许的function）更简洁地写下来。 因此，我们可以写：

searchCommand = searchButton + Enter

cancelCommand = cancelButton + Escape

现在右侧包含的操作数是数据，而不是进程。 在这个级别上，不需要知道隐式优化将把这些操作数转化为进程; 他们不一定会完善投入行动; 输出动作也将适用，例如在testing机器人的规格中。

进程以这种方式获取数据作为同伴; 因此我硬币术语“项目代数”。

Answer 7

微积分和Maclaurin系列与types

这里还有一个小小的补充 – 组合深入理解为什么系列扩展中的系数应该“起作用”，特别是关注可以使用泰勒 – 麦考林方法从微积分得出的系列。 注意：你给出的操纵列表types的例子系列扩展是Maclaurin系列。

由于其他答案和评论涉及代数typesexpression式（和，产品和指数）的行为，所以这个答案将会忽略这个细节，并把重点放在types“微积分”上。

你可能会注意到在这个答案中引用一些重要的引号。 有两个原因：

• 我们从事的是从一个领域向另一个领域的解释，而用这种方式划定这种外来的概念似乎是恰当的。
• 一些概念将能够更加严格地forms化，但形状和想法似乎比细节更重要（并且占用更less的空间）。

Maclaurin系列的定义

Maclaurin系列函数f : ℝ → ℝ被定义为

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

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

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

• （可能是多个）派生
• 将一个函数应用到0
• 像(1/n!)

事实certificate，这些来自分析的概念在types世界中是适合的。

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

微积分与types

那么typesexpression式的派生意味着什么呢？ 事实certificate，对于一个typesexpression式和函数类的一个大而良好的（可区分的）类，有一个自然的操作，其行为足够类似，是一个合适的解释！

为了破解这个问题，类似于差异化的操作就是创造“单一场景”。 这是进一步扩展这个特定点的一个很好的地方，但是单孔上下文（ da/dx ）的基本概念是它表示从一个术语中提取一个特定types（ x ）的单个子项的结果键入a ），保留所有其他信息，包括确定子项目原始位置所需的信息。 例如，表示单列上下文的一种方法是使用两个列表：一个用于在提取之前出现的项目，另一个用于之后出现的项目。

鉴别这种手术的动机来自以下观察。 我们写da/dx来表示types为x的types为a的types的单孔上下文。

 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表示一个居民恰好为零的types， +和×表示照常和的产品types。 f和g用于表示types函数或typesexpression式的forms， [f(x)/a]表示在前面的expression式中用f(x)代替每个a的操作。

这可以写成一个无点式的风格，用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' 

这可能是优选的。

注意，如果我们使用types和函子的同构类来定义导数，那么等式可以做得严格和精确。

现在，我们特别注意到，关于加法，乘法和合成（通常称为和，产品和链规则）的代数运算的微积分规则恰恰反映在“造一个洞”的操作中。 此外，“打洞”的基本情况是一个常量expression式，或者x本身也performance为分化，所以通过归纳我们可以得到所有代数typesexpression式的类微分行为。

现在我们可以解释分化了，一个typesexpression式的第n个“导数”是什么意思呢， dⁿe/dxⁿ是什么意思？ 它是一个代表n -place上下文的types：当用n条件“填充”时产生一个e 。 还有一个关于“ (1/n!) ”的重要观察。

types函数的不变部分：将函数应用于0

我们已经在types世界中有一个0的解释：一个没有成员的空types。 从组合的angular度来看，是什么意思，把一个types函数应用到它呢？ 更具体地说，假设f是一个types函数， f(0)什么样的？ 那么我们当然不能访问types0任何东西，所以任何需要x的f(x)构造都是不可用的。 剩下的就是那些在不存在的情况下可以访问的术语，我们可以称之为“不变”或“常量”的部分。

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

当我们把这个typesf(0)作为一个数字来解释时，它可以被认为是在不访问x情况下可以得到多less个typesf(x) （对于任何x ）的计数 ：即，“空”一词的数量。

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

恐怕我不能想象(1/n!)作为一种适当的直接解释。

但是，如果我们考虑f⁽ⁿ⁾(0)的types，我们可以看到它可以被解释为types为f(x)的n context的types，它还不包含一个 x – 也就是说，当我们把它们“整合” n次时，结果项恰好是 n x s，不多不less。 然后，将typesf⁽ⁿ⁾(0)为一个数字（如在Maclaurin系列f中的系数），只是一个这样的空n场所的上下文的计数。 我们快到了！

但是(1/n!)到哪里去了？ 检查“差异化”types的过程向我们展示，当多次应用时，它保留提取子项的“顺序”。 例如，考虑x × xtypes(x₀, x₁)和两次“打孔”操作。 我们得到两个序列

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

即使两者来自相同的期限，因为有2! = 2 2! = 2从两个方面取两个元素，维持秩序。 一般来说， 有n! 从n获得n n元素的方法 所以为了得到具有n元素的函数types的configuration数，我们必须计算f⁽ⁿ⁾(0)的types并除以n! ， 正如 Maclaurin系列的系数一样。

所以除以n! 原来只是本身的解释。

最后的想法：“recursion”的定义和分析

首先，一些观察：

• 如果函数f：ℝ→ℝ具有导数，则这个导数是唯一的
• 同样，如果一个函数f：ℝ→ℝ是parsing的，它恰好有一个对应的多项式系列

因为我们有链式规则，所以如果我们把types导数forms化为同构类，我们可以使用隐式微分 。 但隐含的分化并不需要像减法或分裂这样的外来手段！ 所以我们可以用它来分析recursiontypes定义。 拿你的榜样，我们有

 L(X) ≅ 1 + X × L(X) L'(X) = X × L'(X) + L(X) 

然后我们可以评估

 L'(0) = L(0) = 1 

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

但是由于我们确信这些expression式确实是严格“可微分的”，所以如果只是隐含的，并且由于我们与函数correspondence→correspondence的对应关系，其中衍生物当然是唯一的，我们可以放心，即使我们用“非法“行动，结果是有效的。

现在，类似地，使用第二个观察，由于与函数ℝ→ℝ的对应关系（是同态？），我们知道，只要我们满意函数具有 Maclaurin级数，如果我们能够在所有上述原则都可以用来使其严格。

至于你关于函数构成的问题，我想连锁规则提供了一个部分答案。

我不确定这适用了多less个Haskell风格的ADT，但是我怀疑它有很多，如果不是全部的话。 我已经发现了这个事实的一个非常奇妙的certificate，但是这个边界太小而不能包含它…

现在，这只是解决这个问题的唯一方法，而且还有很多其他的方法。

总结：TL; DR

• types“分化”对应于“ 打洞 ”。
• 将一个函子应用到0 ，我们得到了这个函数的“空”一词。
• 因此， Maclaurin幂级数（有点）严格对应枚举具有一定数量的元素的函子types的成员的数目。
• 隐含的分化使得这更加水密。
• 衍生物的独特性和幂级数的唯一性意味着我们可以细化和细化它的工作。

Answer 8

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

我对这个问题的第一个回答是很高的概念，低的细节，并反映在“正在发生什么？”这个子问题上。 这个答案将是相同的，但重点是子问题，“我们可以得到任意types的函数吗？”。

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

所以总和

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

可能会写

 Σ[i ∈ ℕ]aᵢXⁱ 

例如， a是一些实数序列。 该产品将用Π而不是Σ来表示。

当你从远处看时，这种expression看起来很像X一个“任意”函数; 我们当然限于可expression的序列及其相关的分析function。 这是一个types理论中的表示的候选人吗？ 非也！

具有这些expression的直接performanceforms的types理论是一类“依赖”型理论：具有相关types的理论。 当然，我们有术语依赖于术语，像Haskell这样的语言，types的function和types的量化，术语和types取决于types。 在依赖设置中，我们还根据条款另外有types。 Haskell不是一种依赖types的语言，尽pipe依赖types的许多特征可以通过折磨语言来模拟。

咖喱霍华德和依赖types

“咖喱霍华德同构”（Curry-Howard isomorphism）起源于一种观察，即简单types的lambda演算的条款和types判断规则恰好对应于直觉主义命题逻辑的自然演绎（由Gentzen提出），types取代了命题以及代替certificate的条款，尽pipe这两者是独立发明的。 从那时起，它一直是types理论家的一个巨大的灵感来源。 要考虑的最明显的事情之一是命题逻辑的这种对应关系是否可扩展到谓词逻辑或更高阶的逻辑。 依赖型理论起源于这条探索之路。

有关简单typeslambda微积分的Curry-Howard同构的介绍，请参见此处 。 作为一个例子，如果我们想certificateA ∧ B我们必须certificateA并certificateB ; 联合certificate只是一对certificate：每一个合并certificate。

在自然演绎中：

 Γ ⊢ A Γ ⊢ B Γ ⊢ A ∧ B 

在简单的lambda演算中：

 Γ ⊢ a : A Γ ⊢ b : B Γ ⊢ (a, b) : A × B 

∨和求和types和函数types以及各种消除规则存在类似的对应关系。

一个无法certificate的（直觉上错误的）命题对应于一个无人居住的types。

将types作为逻辑命题的类比，我们可以开始考虑如何在types世界中对谓词进行build模。 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!

Considering only constructive proofs, what constitutes a proof of ∀x ∈ XP(x) ? We can think of it as a proof function, taking terms ( x ) to proofs of their corresponding propositions ( P(x) ). So members (proofs) of the type (proposition) ∀x : XP(x) are 'dependent functions', which for each x in X give a term of type P(x) .

What about ∃x ∈ XP(x) ? We need any member of X , x , together with a proof of P(x) . So members (proofs) of the type (proposition) ∃x : XP(x) are 'dependent pairs': a distinguished term x in X , together with a term of type P(x) .

Notation: I will use

 ∀x ∈ X... 

for actual statements about members of the class X , and

 ∀x : X... 

for type expressions corresponding to universal quantification over type X . Likewise for ∃ .

Combinatorial considerations: products and sums

As well as the Curry-Howard correspondence of types with propositions, we have the combinatorial correspondence of algebraic types with numbers and functions, which is the main point of this question. Happily, this can be extended to the dependent types outlined above!

I will use the modulus notation

 |A| 

to represent the 'size' of a type A , to make explicit the correspondence outlined in the question, between types and numbers. Note that this is a concept outside of the theory; I do not claim that there need be any such operator within the language.

Let us count the possible (fully reduced, canonical) members of type

 ∀x : XP(x) 

which is the type of dependent functions taking terms x of type X to terms of type P(x) . Each such function must have an output for every term of X , and this output must be of a particular type. For each x in X , then, this gives |P(x)| 'choices' of output.

The punchline is

 |∀x : XP(x)| = Π[x : X]|P(x)| 

which of course doesn't make huge deal of sense if X is IO () , but is applicable to algebraic types.

Similarly, a term of type

 ∃x : XP(x) 

is the type of pairs (x, p) with p : P(x) , so given any x in X we can construct an appropriate pair with any member of P(x) , giving |P(x)| 'choices'.

Hence,

 |∃x : XP(x)| = Σ[x : X]|P(x)| 

with the same caveats.

This justifies the common notation for dependent types in theories using the symbols Π and Σ , and indeed many theories blur the distinction between 'for all' and 'product' and between 'there is' and 'sum', due to the above-mentioned correspondences.

We are getting close!

Vectors: representing dependent tuples

Can we now encode numerical expressions like

 Σ[n ∈ ℕ]Xⁿ 

as type expressions?

不完全的。 While we can informally consider the meaning of expressions like Xⁿ in Haskell, where X is a type and n a natural number, it's an abuse of notation; this is a type expression containing a number: distinctly not a valid expression.

On the other hand, with dependent types in the picture, types containing numbers is precisely the point; in fact, dependent tuples or 'vectors' are a very commonly-cited example of how dependent types can provide pragmatic type-level safety for operations like list access . A vector is just a list along with type-level information regarding its length: precisely what we are after for type expressions like Xⁿ .

For the duration of this answer, let

 Vec X n 

be the type of length- n vectors of X -type values.

Technically n here is, rather than an actual natural number, a representation in the system of a natural number. We can represent natural numbers ( Nat ) in Peano style as either zero ( 0 ) or the successor ( S ) of another natural number, and for n ∈ ℕ I write ˻n˼ to mean the term in Nat which represents n . For example, ˻3˼ is S (S (S 0)) .

Then we have

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

for any n ∈ ℕ .

Nat types: promoting ℕ terms to types

Now we can encode expressions like

 Σ[n ∈ ℕ]Xⁿ 

as types. This particular expression would give rise to a type which is of course isomorphic to the type of lists of X , as identified in the question. (Not only that, but from a category-theoretic point of view, the type function – which is a functor – taking X to the above type is naturally isomorphic to the List functor.)

One final piece of the puzzle for 'arbitrary' functions is how to encode, for

 f : ℕ → ℕ 

expressions like

 Σ[n ∈ ℕ]f(n)Xⁿ 

so that we can apply arbitrary coefficients to a power series.

We already understand the correspondence of algebraic types with numbers, allowing us to map from types to numbers and type functions to numerical functions. We can also go the other way! – taking a natural number, there is obviously a definable algebraic type with that many term members, whether or not we have dependent types. We can easily prove this outside of the type theory by induction. What we need is a way to map from natural numbers to types, inside the system.

A pleasing realisation is that, once we have dependent types, proof by induction and construction by recursion become intimately similar – indeed they are the very same thing in many theories. Since we can prove by induction that types exist which fulfil our needs, should we not be able to construct them?

There are several ways to represent types at the term level. I will use here an imaginary Haskellish notation with * for the universe of types, itself usually considered a type in a dependent setting. ¹

Likewise, there are also at least as many ways to notate ' ℕ -elimination' as there are dependent type theories. I will use a Haskellish pattern-matching notation.

We need a mapping, α from Nat to * , with the property

 ∀n ∈ ℕ.|α ˻n˼| = n. 

The following pseudodefinition suffices.

 data Zero -- empty type data Successor a = Z | Suc a -- Successor ≅ Maybe α : Nat -> * α 0 = Zero α (S n) = Successor (α n) 

So we see that the action of α mirrors the behaviour of the successor S , making it a kind of homomorphism. Successor is a type function which 'adds one' to the number of members of a type; that is, |Successor a| = 1 + |a| for any a with a defined size.

For example α ˻4˼ (which is α (S (S (S (S 0)))) ), is

 Successor (Successor (Successor (Successor Zero))) 

and the terms of this type are

 Z Suc Z Suc (Suc Z) Suc (Suc (Suc Z)) 

giving us exactly four elements: |α ˻4˼| = 4 .

Likewise, for any n ∈ ℕ , we have

 |α ˻n˼| = n 

as required.

1. Many theories require that the members of * are mere representatives of types, and an operation is provided as an explicit mapping from terms of type * to their associated types. Other theories permit the literal types themselves to be term-level entities.

'Arbitrary' functions?

Now we have the apparatus to express a fully general power series as a type!

The series

 Σ[n ∈ ℕ]f(n)Xⁿ 

becomes the type

 ∃n : Nat.α (˻f˼ n) × (Vec X n) 

where ˻f˼ : Nat → Nat is some suitable representation within the language of the function f . We can see this as follows.

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

Just how 'arbitrary' is this? We are limited not only to integer coefficients by this method, but to natural numbers. Apart from that, f can be anything at all, given a Turing Complete language with dependent types, we can represent any analytic function with natural number coefficients.

I haven't investigated the interaction of this with, for example, the case provided in the question of List X ≅ 1/(1 - X) or what possible sense such negative and non-integer 'types' might have in this context.

Hopefully this answer goes some way to exploring how far we can go with arbitrary type functions.