haskell - 数据类型的复杂区分是否明智？

Question

pig 工曾经问过how to express that a type is infinitely differentiable .这个问题让我想起了这样一个事实:在复分析中，一个可微分的函数(在一个开集上)必须是无限可微的(在那个集上)。有没有办法谈论数据类型的复杂区分？如果是这样，类似的定理是否成立？

Answer 1

不是一个真正的答案......但这个咆哮太长了，无法发表评论。

我发现认为复杂的可微性只是意味着无限的可微性有点误导。它实际上比这要强得多:如果一个函数是复可微的，那么它在任意点的导数 determine the entire function .而且因为无限可微性给了你一个完整的泰勒级数，你有一个解析函数，它等于你的函数，即你的函数本身。所以，从某种意义上说，复杂的可微函数是解析的……因为它们是解析的。

从(标准)微积分的角度来看，实数 diff'ability 和复数 diff'ability 之间的主要对比是，在实数中，只有一个方向可以取差商的极限(f(x+δ) - f x)/δ。您只需要左极限等于右极限。但是因为这是限制后的相等，所以这只在局部有效果。 (从拓扑上讲，约束只是比较两个离散值，所以它根本不真正处理连续性属性。)
OTOH，对于复可微性，如果我们从整个复平面中的任何方向接近 x，我们要求差商的极限是相同的。这是一个受约束的整个连续自由度。然后，您可以继续执行拓扑技巧(本质上是柯西积分)以将约束“传播”到整个域。

我认为这在哲学上有点问题。 全纯函数根本不是真正的函数 ，例如:它们不是由它们在整个域中的全部结果值定义的，而是通过某种方式用解析公式(即可能无限的代数表达式/多项式)编写它们。

大多数数学家和物理学家显然非常喜欢这种表达方式——这种表达方式正是他们通常编写函数的方式。
我真的一点也不喜欢它:对我来说，函数应该是函数，由单个值定义的东西，比如可以在空间中测量的场强或可以在 Haskell 中定义的结果。
反正我跑题了...

如果我们将这个问题从数字函数转换为 Haskell 类型的仿函数，我想结果是复杂的 diff'ability 仅意味着:一个类型可以写成(可能是无限的？)ADT 多项式。 the post you linked to 中显示了如何获得此类 ADT 的无限可微性。 .

另一个旋转......也许更接近答案。

Haskell 类型的这些“导数”并不是微积分意义上的真正导数。就像，他们不是受小扰动响应分析的概念驱动的†。碰巧你可以在数学上证明，对于一类非常特殊的函数——那些由代数表达式定义的函数——微积分导数可以再次以简单的代数方式编写(由众所周知的微分规则给出)。这意味着您可以经常进行无限微分。

这种符号区分的有用性也促使人们将其视为一种更抽象的操作。当您区分 Haskell 类型时，主要只是您要追求的这个代数定义，而不是原始的微积分定义。

这很好……但是一旦你在做代数而不是微积分，区分“真实”和“复杂”就没有多大意义了——实际上两者都不是，因为你处理的不是值，而是值的符号表示。一种无类型的语言，如果你愿意的话(事实上，Haskell 的类型语言仍然是无类型的，所有东西都有类型 * )。

†无论是传统的收敛极限还是NSA -无穷小。