haskell - Haskell 中函数的理论定义是什么

Question

我想从基础的角度了解 Haskell 中所谓的函数。

从理论上看，有些“事物”以关联方式组合，具有身份函数，这在理论上就足够了。

但是每个人都试图说服我函数不是这样定义的。函数被定义(他们说)为来自两个集合(域和密码子)的一组元素对，满足特定条件。这意味着一个函数只是一个集合。你不能在不是集合的东西上定义函数。

如果我们将这种方法应用于 Haskell，我看到的是 Hask 类别只是 Sets 的子类别，这对我来说看起来很奇怪。

我宁愿将函数的概念扩展到我们在 Haskell 中的应用。

Here在评论中，这个问题被切线地触及，但不是很深。我想听到一个明确的说法，比如“但实际上它们都是集合”，或者“不，我们与集合论无关”。

有什么想法吗？注意事项？

Answer 1

这是一个非常复杂的话题。为了保持简单和易于管理，我们经常偷工减料，经常“撒谎”。

Haskell 和所有编程语言一样，有自己的语法和求值规则(操作语义)。但是，仅从操作的角度考虑编程语言可能会非常局限和麻烦。当我们调用 factorial 函数时，我们不关心它是如何实现的，也不关心它提供结果所需的确切评估步骤数。

为了克服这个问题，提出了指称语义，其中句法在某些“数学”模型中逐段解释。许多不同的程序(句法表达式)可能映射到相同的解释(“语义”)。

据我所知，整个 Haskell 语言的指称语义从未被定义过。不过，有 Haskell 片段的模型。这些模型通常是类别。

这里有几个例子。

如果我们(非常好!)将 Haskell 限制为一个终止的、简单类型的核心，那么我们所需要的只是一个(双)笛卡尔闭范畴，集合的范畴及其积、余积和指数就足够了。

但是，Haskell 没有终止，并且具有一般递归，所以我们需要不动点。通常这可以通过移至完全部分订单类别(通常介于 omega-CPO 或 DCPO 之间)来解决。

然后我们需要类型级别的不动点，因此我们需要考虑具有初始 F 代数的类别(至少对于行为良好的仿函数 F)。这严重地使事情变得更加复杂。

我们还没有添加多态性!这是特别棘手的，因为雷诺兹证明了多态性不能简单地用集合建模(“多态性不是集合论”是主要引用论文)。所以我们现在有 PER 模型和 Coherent 模型(都是类别)作为为多态性提供语义的一些尝试。

然后我们需要类型类、GADT、更高等级、更高种类……

在实践中，我们不需要这种复杂程度。在编程时，我们通常会处理有限数量的特性，因此我们会“欺骗”自己，并经常假装一切都像一个集合一样工作，或者足够接近。然后，如果确实需要，我们会增加复杂性。