programming-languages - 为什么语言类型的范畴有态射，而不是函子？

Question

我可能没有很好地表达这个问题，所以请耐心等待我试图解释我的意思。

我正在学习应用于编程的类别理论。到目前为止，我的理解是：

• 一个类别中的对象是“完整的”；你不应该窥视它们的内部结构。
• 任何集合都是一个类别
• 编程语言类型可以被认为是集合。（Bool 是集合 True、False；Int 是所有整数的集合；等等）
• 因此，一种语言中的所有类型都形成了一个集合类别。
• 态射是对象之间的箭头。
• 如果这些对象本身就是类别，那么态射被称为函子。

总之，这意味着从 Int 到 Bool 的函数是函子，因为它是从集合类别 Int 到集合类别 Bool 的映射。

但是，我也在其他地方读过（特别是https://www.johndcook.com/blog/2014/05/10/haskell-category-theory/），这样想是错误的，我们真的不应该谈论语言类型是具有“公正”态射的基本类别。但我不明白这与我以前的逻辑有何关系。

因此，我必须得出结论，我之前的逻辑是错误的，但我不清楚如何或为什么。什么是概念化这个的正确方法？集合只是额外的特殊例外吗？或者这真的只是一个关于如何查看问题空间的任意偏好问题？还是我只是在某个地方完全错了？

标签： programming-languagescategory-theory