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

从基础的角度来看，我想看看 Haskell 中所谓的函数。

看，明确地说，有一些“事物”可以关联地组成，具有恒等函数，从理论上讲，这就足够了。

但是每个人都试图说服我这不是函数的定义方式。一个函数被定义（他们说）为一组来自两个集合（域和 codoman）的元素对，满足某些条件。这意味着一个函数只是一个集合。你不能在不是集合的东西上定义一个函数。

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

我宁愿扩展函数的概念以适用于我们在 Haskell 中的内容。

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

有任何想法吗？考虑因素？

标签： haskelllogiccategory-theoryset-theory

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

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

为了克服这种指称语义，有人提出了在某些“数学”模型中逐段解释语法的方法。许多不同的程序（句法表达式）可能映射到相同的解释（“语义”）。

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

这里有一些例子。

如果我们（非常好！）将 Haskell 限制为一个终止的、简单类型的核，那么我们所需要的只是一个（双）笛卡尔闭范畴，集合的范畴就足够了，它的乘积、联积和指数。

然而，Haskell 没有终止，并且具有一般递归，所以我们需要固定点。通常这可以通过转移到完全偏序类别（通常介于 omega-CPO 或 DCPO 之间）来解决。

然后我们需要类型级别的不动点，因此我们需要考虑一个具有初始 F 代数的类别（至少对于表现良好的函子 F）。这严重地使事情变得更加复杂。

我们还没有添加多态性！这尤其棘手，因为 Reynolds 证明了多态性不能用集合简单地建模（“多态性不是集合论”是主要参考论文）。所以我们现在有 PER 模型和 Coherent 模型（都是类别）作为为多态性提供语义的一些尝试。

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

在实践中，我们不需要这种复杂程度。在编程时，我们通常会处理有限数量的功能，所以我们对自己“撒谎”，并经常假装一切都像一组一样工作，或者足够接近。然后，如果确实需要，我们会增加复杂性。