宇宙是什么意思？
What does the universe mean?
关于函数式编程的文章，很多都提到了宇宙。
我正在读 Bartosz Milewski 的书"Category Theory for Programmers"，他也多次提到宇宙。
问题是，宇宙在函数式编程和范畴论的背景下意味着什么？
在范畴论的背景下，引入了全域以绕过集合论的悖论。例如，Set是集合的范畴，所以它的对象对应于集合。此类别中所有对象的集合将是所有集合的集合。但是没有一套所有的套！ Grothendieck 引入了宇宙的概念来处理这个问题。本质上，给定宇宙中所有集合的集合不是该宇宙中的集合——它是下一个更大宇宙中的集合。
在编程中，我们必须处理多态函数，这是为所有类型定义的函数。但并非所有类型都构成一个集合。所以像 Agda 这样的语言可以让你在给定的宇宙中处理类型。他们称最低宇宙为Set，但Set本身是Set1的成员，依此类推
关于函数式编程的文章，很多都提到了宇宙。 我正在读 Bartosz Milewski 的书"Category Theory for Programmers"，他也多次提到宇宙。 问题是，宇宙在函数式编程和范畴论的背景下意味着什么？
在范畴论的背景下，引入了全域以绕过集合论的悖论。例如，Set是集合的范畴，所以它的对象对应于集合。此类别中所有对象的集合将是所有集合的集合。但是没有一套所有的套！ Grothendieck 引入了宇宙的概念来处理这个问题。本质上，给定宇宙中所有集合的集合不是该宇宙中的集合——它是下一个更大宇宙中的集合。
在编程中，我们必须处理多态函数，这是为所有类型定义的函数。但并非所有类型都构成一个集合。所以像 Agda 这样的语言可以让你在给定的宇宙中处理类型。他们称最低宇宙为Set，但Set本身是Set1的成员，依此类推