为什么在 Haskell 中为 Curry 类考虑局部小笛卡尔封闭类别是公平的？

Question

Control.Category.Constrained是一个非常有趣的项目，它展示了笛卡尔封闭类别的类 - Curry.

然而，我不明白为什么我们会想到所有允许curry和uncurry（Hom(X * Y, Z) ? Hom(X, Z^Y)就范畴论而言）的笛卡尔封闭范畴。维基百科说这种性质只适用于局部小的笛卡尔封闭类别。在这个帖子下，很多人建议Hask本身并不小（另一方面，每个人都说Hask不是笛卡尔封闭类别，我认为这是一种纯粹且无趣的形式主义）。

在Math.SE上的这篇文章中，假设所有类别都在本地较小。但它是从我们讨论属性的数学角度给出的。我想知道为什么我们决定专注于和as的方法。是不是因为几乎每个了解 Haskell 的人也都知道这些函数？还是有其他原因？curryuncurryCurry

Answer 1

我想知道为什么我们决定专注于curry和uncurryasCurry的方法。是不是因为几乎每个了解 Haskell 的人也都知道这些函数？

作为图书馆的作者，我可以自信地回答这个问题，答案是肯定的：这是因为curry并且uncurry是 Haskell 白话的一部分。constrained-categories从来没有打算从根本上改变 Haskell 和/或使其在某种意义上在数学上更可靠，而是巧妙地概括现有的类层次结构——主要是为了允许定义无法给定Prelude.Functor实例的函子等。

Curry坦率地说，我不知道是否可以根据本地小规模进行正式化。我也不确定这个和其他“数学基础”方面是否可以在 Haskell 库的上下文中进行有意义的讨论。^{_{前面有点跑题}}了 Haskell 是一种非完整语言，这只是一个事实，是的，这意味着几乎任何公理都可能被某些undefined攻击所挫败。但我也不认为这是一个问题。许多人似乎认为 Haskell 是一种恐怖谷：在实际应用中使用限制太多，但没有任何东西可以被正确证明。我的看法正好相反：Haskell 有一个足够强大的类型系统来表达对现实世界的应用程序有用的数学思想，而不会使其价值语义在底层基础中陷入太深而无法在现实世界中实际使用。（也就是说，你不会经常花几周时间证明一些“显然这是真的……”定理。我在看着你，Coq……）
我们没有写出 100% 严格的证明，而是尽可能地缩小类型尽可能，然后使用 QuickCheck 来查看某些东西是否通常按数学要求工作。

不要误会我的意思，我认为形式化基础也很重要，依赖类型的总语言很棒，但是所有这些都有些忽略了 Haskell 的潜力真正所在的点。至少它不是在那里我的目标是我的Haskell的发展，包括constrained-categories。如果有人对纯数学有更深入的了解，我很高兴听到这个消息。