scala - 宇宙是什么意思？

Question

关于函数式编程的文章，很多都提到了宇宙。我正在阅读 Bartosz Milewski 的《程序员类别理论》一书，他也多次提到宇宙。问题是，在函数式编程和范畴论的背景下，宇宙意味着什么？

标签： scalahaskellfunctional-programmingterminologycategory-theory

Answer 1

在范畴论的背景下，引入宇宙是为了绕过集合论的悖论。例如，Set 是集合的范畴，所以它的对象对应于集合。此类别中所有对象的集合将是所有集合的集合。但是没有所有集合的集合！格洛腾迪克引入了宇宙的概念来解决这个问题。本质上，给定宇宙中所有集合的集合不是那个宇宙中的集合——它是下一个更大宇宙中的集合。

在编程中，我们必须处理多态函数，它们是为所有类型定义的函数。但并非所有类型都形成一个集合。所以像Agda这样的语言可以让你在给定的宇宙中使用类型。他们称最低宇宙集，但集本身是集₁的成员，依此类推。