Являются ли функции arity-n действительно просто n-категорией из-за каррирования? Могут ли они быть превращены в 1-категорию?

Этот вопрос имеет длинную прелюдию, прежде чем я могу спросить об этом:)

Пусть говорят, что типы A и B представляют категории, то функция

f:: B → A

является морфизмом между двумя категориями. Мы можем создать новую категорию с A и B как объекты и f как стрелку, подобную этой:

Теперь введем новую категорию C и функцию g:

g:: C → B → A

Я хотел бы иметь возможность добавлять C и g в свою категорию выше, но я не уверен, как это сделать. Интуитивно, я хочу что-то похожее на это:

Но я никогда не видел ничего подобного на диаграмме категории раньше. Чтобы сделать это кошерным, я мог бы ввести фиктивную стрелку g 'и построить 2-категорию, подобную этой:

Но это кажется тупой картиной. (Мы могли бы, конечно, использовать картинку, которую я нарисовал выше, как сокращение для правильного.) Кроме того, теперь не совсем ясно, что такое g и g '. g уже не является функцией, которая принимает в качестве входной категории категорию C и возвращает морфизм:: B → A. Вместо этого

g ':: (C → C)

g:: (C → C) → (B → A)

Если мы передадим g тождеству, тогда все будет работать нормально. Но если мы передадим ему какую-то другую функцию, то кто знает, что может случиться?

Итак, мой вопрос: есть ли n-стрелка внутри n-категории, как мы должны думать о функциях с arity n? Или есть ли более простой способ представить эту функцию в стандартную категорию, которую я пропустил?

Ответ 1

Говоря о "морфизмах между категориями", здесь звучит как возможная ошибка категории (га, га). В Haskell мы чаще всего говорим о предполагаемой категории Hask, которая представляет собой некорректно идеализированную версию категории ⁽⁰⁾ объекты которой являются типами вида *, а морфизмы функции. Неясно, какие "функции" между категориями будут здесь, если они не являются морфизмами Hask.

С другой стороны, в более общей настройке вы можете определенно определить категорию, объектами которой являются другие категории ⁽¹⁾ с любыми морфизмами, которые вы хотите, чтобы удовлетворялись необходимые свойства. Обычным примером этого является Cat, категория небольших категорий, морфизмы которых являются функторами.

Тем не менее, в любом случае ответ на ваш вопрос по сути тот же. Говорить о наборе морфизмов между двумя объектами, как будто эта коллекция сама по себе является объектом, то есть в качестве источника или места назначения других морфизмов, вам нужен объект для заполнения этой роли и некоторый способ косвенно говорить о морфизмах, чтобы вы может переводить назад и вперед.

Один из способов сделать это, если у нас уже есть способ поговорить о парах объектов как о едином объекте (обычно называемом "продуктом" какого-то рода), заключается в определении эквивалентности между совокупностью морфизмов A⊗B → C и набор морфизмов A → C ^B что позволяет объекту C ^B встать для набора морфизмов B → C.

Если рассматриваемые "пары объектов" являются категориальным продуктом, мы имеем декартовую замкнутую категорию, которые имеют как Хаск, так и Cat. В Haskell приведенная выше эквивалентность - это функции curry и uncurry ⁽²⁾.

Это не единственный способ поговорить о морфизмах как о объектах, конечно. Общая концепция просто называется "закрытой категорией". Но если вы думаете с точки зрения функций более высокого порядка и функционального программирования, то декартовая закрытая категория, вероятно, вы имеете в виду.

(0) Это обычно включает в себя такие вещи, как притворство ⊥, не существует (так что все функции являются полными) и обработки функций, которые производят одинаковый вывод как идентичный (например, игнорируя различия в производительности).

(1) Но не пытайтесь говорить о категории, чьи объекты есть все категории, или Бертран Рассел даст вам бизнес.

(2) Именован, конечно, логик Haskell Curry.

Ответ 2

Я довольно нелюбимый в теории категорий, но:

В программировании Haskell мы часто (притворяемся, что мы) работаем с категорией Hask, объектами которой являются типы и морфизмы Haskell, являются функциями Haskell.

Применяя это понимание к вашему примеру, я вижу, что B и A являются объектами, а f является морфизмом между ними.

g, однако, не морфизм между C и f, поэтому не следует пытаться рисовать g как стрелку между C и f стрелка.

Если применить правую ассоциативность конструктора типа ->, мы получим g :: C -> (B -> A). B -> A сам является типом Haskell и поэтому должен быть объектом Hask самостоятельно. f, однако, не, этот объект; это одно конкретное значение в типе B -> A, но объектом B -> A будет сам тип.

Это также имеет смысл думать исключительно в терминах Хаскелла. Просто потому, что g применяется к значению типа C, дает нам некоторую функцию типа B -> A, что не означает, что g возвращаемое значение имеет какое-либо отношение к f, что является некоторой другой функцией типа B -> A.

Таким образом, мы получаем f как морфизм между объектом B и объектом A и g как морфизм, нарисованный между объектом C и объектом B -> A.

Здесь, где мое знание теории теории ломается. Кажется очевидным, что между f и объектом B -> A должна быть какая-то связь, так как в Haskell f есть значение в типе B -> A. Я не знаю, что это за отношения в категориях теории.

С. Ответ А. Макканна звучит так, как будто вам нужно справиться с такими "дополнительными" отношениями, которые не моделируются непосредственно категорией. Что касается категории, объект B -> A также можно назвать D; он не имеет никакого отношения ни к чему другому, кроме как в силу морфизмов, соединяющих его с другими объектами. Это только в сочетании с другой информацией из категории "снаружи", которую мы можем идентифицировать, между A, B, f и D (действительно B -> A). Но я могу не понимать это описание.