滥用代数数据类型的代数
代数数据类型的“代数”表达式对于具有数学背景的人来说非常具有启发性。 让我试着解释我的意思。
定义了基本类型
• + X 1 并且使用简写X²代替X•X和2X代替X+X等等，我们可以定义代数表达式，例如链表
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²
现在，作为一名数学家，我的第一本能就是坚持用这些表达式，并尝试解决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完成）。 这表达了对我而言非常明显的事实，即只有一个元素的二叉树，有两个元素的二叉树（第二个元素可以在左边或右边的分支上），具有三个元素的5个二叉树等。
所以我的问题是 - 我在这里做什么？ 这些操作似乎是不合理的（无论如何，代数数据类型的平方根究竟是什么？），但它们会导致明显的结果。 两个代数数据类型的商是否在计算机科学中具有任何意义，还是仅仅是符号的诡计？
或许更有趣的是，是否有可能扩展这些想法？ 是否存在类型代数的理论，例如允许类型上的任意函数，或类型是否需要幂级数表示？ 如果你可以定义一类函数，那么函数的组合是否有任何意义？
免责声明：当你对⊥进行解释时，很多情况并不适用，所以为了简单起见，我会公然无视这一点。
几个初始点：
请注意，“联合”在这里可能不是A + B的最佳术语 - 这是特别的两种类型的不相交联合，因为即使它们的类型相同，双方也是有区别的。 对于它的价值，更常见的术语就是“总和类型”。
单身类型实际上是所有单位类型。 它们在代数操作下表现相同，更重要的是，信息量仍然保留。
你可能也想要一个零类型。 没有标准的名称，但最常见的名称是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定义。
上面的对偶是A + B的副产品，其中A→B→A→B→B→A + B，其中给定任意类型C和函数f：A→C，g：B→C，你可以定义共同的f ||| g：A + B→C，使得明显的等价性成立。 同样，参数化可以自动保证大部分棘手的部件。 在这种情况下，标准的注射是简单的Left和Right与copairing是功能either 。
产品和总和类型的许多属性都可以从上面得出。 请注意，任何单例类型都是Hask的终端对象，任何空类型都是初始对象。
回到前面提到的缺失操作，在笛卡儿式封闭类别中，您有与该类别的箭头对应的指数对象。 我们的箭头是函数，我们的对象是带有*的类型，并且类型A -> B在类型的代数操作的上下文中确实表现为BA。 如果这不是明显的原因，考虑类型Bool -> A 只有两个可能的输入，该类型的函数同构于A类型A两个值，即(A, A) 。 对于Maybe Bool -> A我们有三个可能的输入，依此类推。 另外，请注意，如果我们将上面的共同定义改为使用代数符号，我们可以得到身份CA×CB = CA + B。
至于为什么这一切都是有道理的 - 特别是为什么你使用幂级数展开是合理的 - 请注意，上面的大部分指的是一种类型的“居民”（即，具有该类型的不同值）展示代数行为。 为了明确这个观点：
产品类型(A, B)表示A和B各自独立的值。 因此，对于任何固定值a :: A ，每个B居民有一个类型的值(A, B) 。 这当然是笛卡尔产品，而产品类型的居民人数是这些因素的居民人数的乘积。
总和类型A或Either AB表示来自A或B的值，并区分左侧和右侧分支。 如前所述，这是一个不相交的联盟，而和类型的居民人数是被征求人的总人数。
指数型B -> A表示从类型B的值到类型A值的映射。 对于任何固定的参数b :: B ， A任何值都可以赋值给它; 类型B -> A的值为每个输入选择一个这样的映射，这相当于B具有居民的A许多拷贝的乘积，因此取幂。
虽然首先将类型视为集合是诱人的，但在这种情况下实际上并不能很好地工作 - 我们有联合而不是标准联合集合，对交集或其他集合操作没有明显的解释，而我们通常不关心设置成员（将其留给类型检查器）。
另一方面，上面的建筑花费了大量的时间来谈论居民的数量，并且列举一种类型的可能值在这里是一个有用的概念。 这很快将我们引向枚举组合，如果您参考链接的维基百科文章，您会发现它所做的第一件事情之一是通过以下方式定义“对”和“联合”，其与产品和总和类型完全相同：生成函数，然后对与Haskell列表相同的“序列”使用完全相同的技术执行相同的操作。
编辑：哦，这里有一个快速的奖金，我认为这一点显着地证明了这一点。 您在评论中提到，对于树型T = 1 + T^2您可以导出标识T^6 = 1 ，这显然是错误的。 然而， T^7 = T确实成立，并且可以直接构建树与树的七元组之间的双射。 安德烈亚斯布拉斯的“七树一体”。
编辑×2：关于其他答案中提到的“类型派生”构造的主题，您可能还会从同一作者那里欣赏这篇文章，这个作者进一步构思了这个想法，包括分裂的概念和其他有趣的东西。
二进制树由类型的半环中的方程T=1+XT^2定义。 通过构造， T=(1-sqrt(1-4X))/(2X)由复数半环上的相同方程定义。 所以考虑到我们正在同一类代数结构中求解相同的方程，我们看到一些相似之处实际上并不令人惊讶。
值得注意的是，当我们推论复数中半多项式的多项式时，我们通常使用复数形成环或甚至场的事实，因此我们发现自己使用了不适用于半环的操作，如减法。 但是，如果我们有一条规则允许我们从等式两边消除，我们通常可以从我们的论点中消除减法。 这是Fiore和Leinster证明的那种事实，表明许多关于戒指的论点可以转化为半环。
这意味着你对环的大量数学知识可以可靠地转换为类型。 因此，涉及复数或幂级数（在正式幂级数环中）的一些论点可以以完全严格的方式继承到类型。
然而，这个故事不仅仅是这个。 通过证明两个幂级数是相等的，证明两种类型是平等的（比如说）是一回事。 但是你也可以通过检查幂级数中的术语来推断出类型的信息。 我不确定这里的正式声明应该是什么。 （我建议Brent Yorgey关于组合物种的论文关于一些密切相关的工作，但物种与类型不一样。）
我发现令人兴奋的是，你发现的东西可以扩展到微积分。 关于微积分的定理可以转移到类型的半环上。 事实上，即使有关有限差异的争论也可以转移，你会发现数值分析的经典定理在类型理论中有解释。
玩的开心！
看来你所做的只是扩大循环关系。
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 + ...
由于这些类型的操作规则就像算术操作的规则一样工作，所以可以使用代数方法来帮助您找出如何扩展递归关系（因为它不明显）。
链接地址: http://www.djcxy.com/p/33625.html