В статьях о функциональном программировании много упоминаний о вселенной. Я читаю книгу «Теория категорий для программистов» Бартоша Милевски, и он также много раз упоминал о вселенной. Вопрос в том, что означает вселенная в контексте функционального программирования и теории категорий?
Что означает вселенная?
comment
en.m.wikipedia.org/wiki/Universe_(математика)
- person Fogmeister schedule 18.09.2019
comment
Я предлагаю процитировать отрывок из Теории категорий для программистов, в котором вселенная используется так, как вы думаете, ради более точного ответа.
- person duplode schedule 18.09.2019
comment
В контексте FP я бы сказал, что это просто означает все, что выходит за рамки вашей чисто функциональной программы, то есть этот термин используется в метафорическом смысле.
- person Iven Marquardt schedule 18.09.2019
comment
@bob: Это чаще называют окружающей средой или миром. Вселенная в том смысле, о котором спрашивает ОП, имеет точно определенное значение и связана с понятием вселенной дискурса в философии. Так что в некотором смысле это прямо противоположно тому, что вы говорите: это все, что есть в рамках программы.
- person Jörg W Mittag schedule 18.09.2019
Ответы (1)
В контексте теории категорий вселенные были введены для того, чтобы обойти парадоксы теории множеств. Например, Set — это категория наборов, поэтому его объекты соответствуют наборам. Набор всех объектов в этой категории будет набором всех наборов. Но нет набора всех наборов! Гротендик представил идею вселенных, чтобы справиться с этим. По сути, множество всех множеств в данной вселенной — это не множество в этой вселенной — это множество в следующей большей вселенной.
В программировании нам приходится иметь дело с полиморфными функциями, то есть функциями, определенными для всех типов. Но все типы не образуют множество. Таким образом, такие языки, как Agda, позволяют работать с типами внутри данная вселенная. Они называют низшую вселенную Set, но сам Set является членом Set1 и так далее.
person
Bartosz Milewski
schedule
18.09.2019
