Где значения вписываются в категорию Hask?
Итак, у нас есть категория Hask, где:
- Типы являются объектами категории
- Функции - это морфизмы от объекта к объекту в категории.
Аналогично для Functor у нас есть:
- Конструктор типов как отображение объектов из одной категории в другую
fmapдля отображения морфизмов из одной категории в другую.
Теперь, когда мы пишем программу, мы в основном преобразуем значения (не типы), и кажется, что категория Hask вообще не говорит о значениях. Я попытался вписать значения во все уравнение и пришел к следующему наблюдению:
- Каждый тип является самой категорией. Пример: Int - это категория всех целых чисел.
- Функции от значения к другому значению того же типа являются морфизмом категории. Например:
Int -> Int - Функции от одного значения к другому значению другого типа являются функтором для отображения значений одного типа другому.
Теперь мой вопрос - имеют ли значения вообще смысл в категории Хаск (или в общей теории категорий)? Если да, то любая ссылка, чтобы прочитать об этом, ИЛИ если нет, то любая причина для этого.
Надеюсь вопрос имеет смысл:)
5 ответов
(Я буду использовать слова с их значением из математики / теории категорий, а не программирования, если я mark it as code.)
Одна категория за раз
Одна из главных идей теории категорий состоит в том, чтобы рассматривать большие сложные вещи как точку, поэтому правильное формирование множества / группы / кольца / класса / категории всех целых считается одной точкой, когда вы думаете о категории Hask,
Точно так же вы могли бы иметь очень сложную функцию для целых чисел, но она просто считается одним элементом (точка / стрелка) из коллекции (набор / класс) морфизмов.
Первое, что вы делаете в теории категорий, это игнорируете детали. Таким образом, категория Hask не заботится о том, что Int можно считать категорией - это на другом уровне. Int - это просто точка (объект) в Hask.
Один уровень вниз
Каждый моноид - это категория с одним объектом. Давайте использовать это.
Как целые категории категории?
На это есть более одного ответа (поскольку целые числа являются моноидами при сложении и моноидами при умножении). Давайте сделаем дополнение:
Вы можете рассматривать целые числа как категорию с одним объектом, а морфизмы - это такие функции, как (+1), (+2), (вычитание 4).
Вы должны держать в голове, что я рассматриваю целое число 7 как число 7, но использую представление (+7), чтобы сделать его категорией. Законы теории категорий сознательно не говорят, что ваши морфизмы должны быть функциями, но более ясно, что что-то является категорией, если оно имеет структуру набора функций, содержащих тождество и замкнутых по составу.
Любой моноид создает категорию одного объекта так же, как мы только что сделали с целыми числами.
Функторы от целых чисел?
Функция f из целых чисел как категория под операцию +к какому-то другому типу с операцией £ которая формирует категорию, может быть только функтором, если у вас есть f(x+y) = f(x) £ f(y), (Это называется моноидным гомоморфизмом). Большинство функций не являются морфизмами.
Пример морфизма
Stringс моноид под ++так что они категория.
len :: String -> Int
len = length
len является моноидным морфизмом из String в Int, так как len (xs ++ ys) = len xs + len ysтак что если вы рассматриваете (String,++) а также (Int,+) как категория, len это функтор
Пример неморфизма
(Bool,||) является моноидом, с False как личность, так что это категория с одним объектом. Функция
quiteLong :: String -> Bool
quiteLong xs = length xs > 10
не морфизм, потому что quiteLong "Hello " является False а также quiteLong "there!" это также False, но quiteLong ("Hello " ++ "there!") является True, а также False || False не является True,
Так как quiteLong это не морфизм, это не функтор.
Что ты думаешь, Эндрю?
Я хочу сказать, что некоторые типы Haskell можно считать категориями, но не все функции между ними являются морфизмами.
Мы не думаем о категориях на разных уровнях в одно и то же время (если только вы не используете обе категории для какой-то странной цели), и теоретически не существует теоретически никакого взаимодействия между уровнями, потому что нет намеренно никакой детализации объектов и морфизмов.
Это отчасти потому, что теория категорий взяла курс на математику, чтобы обеспечить язык для описания прекрасного взаимодействия теории Галуа между конечными группами / подгруппами и полями / расширениями полей, двумя, очевидно, совершенно разными структурами, которые оказываются тесно связанными. Позднее теория гомологии / гомотопии сделала функторы между топологическими пространствами и группами, которые оказываются одновременно увлекательными и полезными, но суть в том, что объектам и морфизмам позволено сильно отличаться друг от друга в двух категориях функтора.,
(Обычно теория категорий приходит в Haskell в форме функтора от Hask к Hask, поэтому на практике в функциональном программировании две категории одинаковы.)
Итак... что именно является ответом на оригинальный вопрос?
- Каждый тип является самой категорией. Пример: Int - это категория всех целых чисел.
Если вы думаете о них определенным образом. Смотрите ответ PhilipJF для деталей.
- Функции от значения к другому значению того же типа являются морфизмом категории. Например:
Int -> Int
Я думаю, что вы перепутали два уровня. Функции могут быть морфизмами в Hask, но не все функции Int -> Int Функторы под структурой сложения, например f x = 2 * x + 10 не является функтором между Int и Int, поэтому это не морфизм категории (еще один способ сказать функтор) из (Int,+) к (Int,+) но это морфизм Int -> Int в категории Hask.
- Функции от одного значения к другому значению другого типа являются функтором для отображения значений одного типа другому.
Нет, не все функции являются, например, функторами quiteLong нет.
Имеют ли смысл значения в категории Хаск (или в общей теории категорий)?
Категории не имеют значений в теории категорий, они просто имеют объекты и морфизмы, которые рассматриваются как вершины и направленные ребра. Объекты не должны иметь значения, а значения не являются частью теории категорий.
Как я прокомментировал ответ Эндрю (что в противном случае очень хорошо), вы можете рассматривать значения в типе как объекты этого типа как категорию и рассматривать функции как функторы. Для полноты, здесь есть два способа:
Устанавливается как скучные категории
Одним из наиболее часто используемых инструментов в математике является "сетоид", то есть набор с отношением эквивалентности над ним. Мы можем думать об этом категорически через понятие "группоид". Группоид - это категория, в которой каждый морфизм имеет обратное значение, так что f . (inv f) = id а также (inv f) . f = id,
Почему это отражает идею отношения эквивалентности? Что ж, отношение эквивалентности должно быть рефлексивным, но это просто категорическое утверждение о том, что оно имеет идентичные стрелки, и оно должно быть транзитивным, но это просто композиция, в конце концов, она должна быть симметричной (именно поэтому мы добавили инверсии).
Обычное понятие равенства в математике на любом множестве, таким образом, приводит к группоидной структуре, а именно к той, где единственными стрелками являются стрелки идентичности! Это часто называют "дискретной категорией".
Читателю оставлено в качестве упражнения показать, что все функции являются функторами между дискретными категориями.
Если вы серьезно относитесь к этой идее, вы начинаете задумываться о типах с "равенством", которые не являются просто идентичностью. Это позволило бы нам кодировать "фактор-типы". Более того, структура группоидов имеет еще несколько аксиом (ассоциативность и т. Д.), Которые являются утверждениями о "равенстве доказательств равенства", которое ведет по пути n-группоидов и теории более высоких категорий. Это классная штука, хотя для того, чтобы быть полезной, вам нужны зависимые типы и некоторые не полностью проработанные биты, и когда это наконец превращается в языки программирования, это должно позволить
data Rational where
Frac :: Integer -> Integer -> Rational
SameRationa :: (a*d) ~ (b*c) -> (Frac a b) ~ (Frac c d)
Таким образом, что каждый раз, когда вы сопоставляете шаблон, вам также нужно будет сопоставить аксиому дополнительного равенства и, таким образом, доказать, что ваша функция уважает отношение эквивалентности RationalНо не беспокойся об этом. Дело лишь в том, что интерпретация "Дискретная категория" является совершенно хорошей.
Денотационные подходы
Каждый тип в Haskell населяется дополнительным значением, а именно undefined, Что происходит с этим? Ну, мы могли бы определить частичный порядок для каждого типа, связанный с тем, как "определено" значение, так что
forall a. undefined <= a
но и такие вещи, как
forall a a' b b'. (a <= a') /\ (b <= b') -> ((a,b) <= (a',b'))
Undefined менее определен тем, что относится к значению, которое не заканчивается (на самом деле, undefined Функция реализована путем выдачи исключения в каждом haskell, но давайте притворимся, что это было undefined = undefined, Вы не можете быть уверены, что что-то не заканчивается. Если вам дают undefined все, что вы можете сделать, это подождать и посмотреть. Таким образом, это может быть что угодно.
Частичный порядок порождает категорию стандартным способом.
Таким образом, каждый тип порождает категорию, где значения являются объектами таким образом.
Почему функции функторы? Ну, функция не может сказать, что она получила undefined из-за проблемы остановки. Как таковой, он либо должен вернуть undefined когда он сталкивается с кем-то, или он должен дать тот же ответ, независимо от того, что ему дали. Вам остается показать, что на самом деле это функтор.
Хотя здесь есть и другие, довольно замечательные ответы, все они несколько упускают ваш первый вопрос. Чтобы быть понятным, значения просто не существуют и не имеют никакого значения в категории Hask. Это не то, о чем говорит Хаск.
Вышеприведенное кажется немного глупым, чтобы сказать или почувствовать, но я поднимаю его, потому что важно отметить, что теория категорий предоставляет только один объектив для изучения гораздо более сложных взаимодействий и структур, доступных в чем-то столь же сложном, как язык программирования. Не стоит ожидать, что вся эта структура будет отнесена к достаточно простому понятию категории. [1]
Еще один способ сказать, что мы пытаемся проанализировать сложную систему, и иногда полезно рассматривать ее как категорию для поиска интересных закономерностей. Именно это мышление позволяет нам представить Hask, убедиться, что оно действительно формирует категорию, заметить, что Maybe похоже, ведет себя как функтор, а затем использует всю эту механику для записи условий когерентности.
fmap id = id
fmap f . fmap g = fmap (f . g)
Эти правила имеют смысл независимо от того, представляем ли мы Hask, но, рассматривая их как простые следствия простой структуры, которую мы можем обнаружить в Haskell, мы понимаем их важность.
Как техническое примечание, весь этот ответ предполагает, что Hask на самом деле является "платоническим" Hask, то есть мы игнорируем дно (undefined и не прекращение) так, как нам нравится. Без этого почти весь аргумент разваливается чуть-чуть.
Давайте рассмотрим эти законы более внимательно, так как они, кажется, почти противоречат моему первоначальному утверждению - они явно работают на уровне значений, но "значений в Hask не существует", верно?
Ну, один из ответов - поближе познакомиться с категориальным функтором. Явно, это отображение между двумя категориями (скажем, C и D), которое переводит объекты C в объекты D и стрелки C в стрелки D. Стоит отметить, что в общем случае эти "отображения" не являются категориальными стрелками - они просто образуют отношения между категориями и не обязательно разделяют по структуре с категориями.
Это важно, потому что даже учитывая Haskell Functor s, endofunctors в Hask, мы должны быть осторожны. В Hask объекты имеют типы Haskell, а стрелки - это функции Haskell между этими типами.
Давайте посмотрим на Maybe снова. Если это будет endofunctor в Hask, то нам нужен способ перевести все типы в Hask на другие типы в Hask. Это отображение не является функцией Haskell, хотя может выглядеть так: pure :: a -> Maybe a не подходит, потому что он работает на уровне стоимости. Вместо этого наше сопоставление объектов Maybe сам: для любого типа a мы можем сформировать тип Maybe a,
Это уже подчеркивает ценность работы в Hask без значений - мы действительно хотим изолировать понятие Functor который не зависит от pure,
Мы разработаем остальную часть Functor изучив отображение стрелок нашего Maybe endofunctor. Здесь нам нужен способ сопоставить стрелки Хаск со стрелами Хаск. Давайте пока предположим, что это не функция Haskell - это необязательно - поэтому, чтобы подчеркнуть ее, мы напишем ее по-другому. Если f это функция Haskell a -> b тогда может быть [ f ] - это другая функция Haskell Maybe a -> Maybe b,
Теперь трудно не пропустить и просто начать звонить Возможно [ f ] " fmap f ", но мы можем сделать немного больше работы, прежде чем сделать этот прыжок. Может быть, [ f ] должны иметь определенные условия согласованности. В частности, для любого типа a в Hask у нас есть стрелка id. В нашем метаязыке мы можем назвать это id [ a ] и мы знаем, что это также идет под именем Haskell id :: a -> a, В целом, мы можем использовать их для определения условий когерентности эндофунктора:
Для всех объектов в Hask a у нас есть что может [id [ a ]] = id [ Maybe a ]. Для любых двух стрелок в Hask f а также g у нас есть что может [ f . g ] = Может быть [ f ]. Может быть[ g ].
Последний шаг заключается в том, чтобы заметить, что Maybe[_] может быть реализован как функция Haskell, так и как значение объекта Hask. forall a b . (a -> b) -> (Maybe a -> Maybe b), Это дает нам Functor,
Хотя вышесказанное было довольно техническим и сложным, есть важный момент в том, чтобы сохранить понятия Хаск и категориальных эндофункторов прямыми и отделенными от их реализации в Хаскеле. В частности, мы можем обнаружить всю эту структуру, не вводя необходимость fmap существовать как настоящая функция Haskell. Hask - это категория, которая вообще ничего не вводит на уровне ценности.
Вот где живет настоящее бьющееся сердце просмотра Hask как категории. Обозначение, которое идентифицирует endofunctors на Hask с Functor требует гораздо большего размытия линий.
Размытие этой линии оправдано, потому что Hask имеет экспоненты. Это хитрый способ сказать, что в Hask есть объединение целых пучков категориальных стрелок и конкретных специальных объектов.
Чтобы быть более точным, мы знаем, что для любых двух объектов Hask, скажем, a а также b мы можем говорить о стрелках между этими двумя объектами, часто обозначаемыми как Hask (a, b). Это просто математический набор, но мы знаем, что в Hask есть еще один тип, тесно связанный с Hask (a, b): (a -> b)!
Так что это странно.
Первоначально я заявил, что общие значения Haskell абсолютно не представлены в категориальном представлении Hask. Затем я продолжил демонстрировать, что мы можем многое сделать с Hask, используя только его категоричные понятия и фактически не вставляя эти части в Haskell в качестве значений.
Но теперь я отмечаю, что значения типа, как a -> b на самом деле существуют как все стрелки в металингвистическом наборе Хаск (a, b). Это хитрость, и именно это металингвистическое размытие делает категории с экспонентами такими интересными.
Мы можем сделать немного лучше, хотя! У Hask также есть конечный объект. Мы можем говорить об этом металингвистически, называя его 0, но мы также знаем об этом как тип Хаскелла. (), Если мы посмотрим на любой объект Hask a мы знаем, что в Hask есть целый набор категориальных стрелок ((), a). Кроме того, мы знаем, что они соответствуют значениям типа () -> a, Наконец, так как мы знаем, что дана любая функция f :: () -> a мы можем сразу получить a применяя () Можно сказать, что категоричные стрелки в Hask ((), a) являются в точности значениями типа Haskell a,
Что должно быть либо крайне запутанным, либо невероятно умопомрачительным.
Я собираюсь закончить это несколько философски, придерживаясь моего первоначального утверждения: Хаск вообще не говорит о ценностях Хаскеля. На самом деле это не просто категория - категории интересны именно потому, что они очень просты и, следовательно, не нуждаются во всех этих вне-категориальных понятиях типов и значений и typeOf включение и тому подобное.
Но я также, возможно, плохо показал, что, даже будучи строго строгой категорией, в Hask есть нечто, очень похожее на все значения Haskell: стрелки Hask ((), a) для каждого объекта Hask a,
С философской точки зрения мы можем утверждать, что эти стрелки на самом деле не являются значениями Haskell, которые мы ищем, - они просто заменители, категоричные насмешки. Вы можете возразить, что это разные вещи, но они просто соответствуют друг другу со значениями в Haskell.
Я действительно думаю, что это действительно важная идея, чтобы иметь в виду. Эти две вещи разные, они просто ведут себя одинаково.
Очень похоже. Любая категория позволяет вам составлять стрелки, поэтому давайте предположим, что мы выбрали стрелку в Hask (a, b) и стрелка в Hask ((), a). Если мы объединим эти стрелки с составом категории, мы получим стрелку в Hask ((), b). Если немного перевернуть все это, мы можем сказать, что я только что нашел значение типа a -> b, значение типа a, а затем объединили их для получения значения типа b,
Другими словами, если мы посмотрим на вещи в сторону, то увидим категориальную композицию стрелок как обобщенную форму приложения функции.
Это то, что делает такие категории, как Hask, такими интересными. В целом, эти виды категорий называются декартовыми закрытыми категориями или CCC. Из-за наличия как начальных объектов, так и экспонент (которые также требуют продуктов) они имеют структуры, которые полностью моделируют типичное лямбда-исчисление.
Но у них все еще нет ценностей.
[1] Если вы читаете это до прочтения оставшейся части моего ответа, продолжайте читать. Оказывается, что абсурдно ожидать, что это произойдет, на самом деле это действительно так. Если вы читаете это после прочтения всего моего ответа, давайте просто поразмышляем о том, насколько классны CCC.
Есть несколько способов обозначить вещи категориями. Специально языки программирования, которые оказываются очень богатыми конструкциями.
Если мы выбираем категорию Hask, мы просто устанавливаем уровень абстракции. Уровень, на котором не очень удобно говорить о ценностях.
Однако константы могут быть смоделированы в Hask как стрелка от объекта терминала () к соответствующему типу. Тогда, например:
- True: () -> Bool
- 'a': () -> Char
Вы можете проверить: Барр, Уэллс - Теория категорий для вычислений, раздел 2.2.
Любая категория с терминальным объектом (или с терминальным объектом *s*) имеет так называемые глобальные элементы (или точки, или константы, также в Википедии), подробнее можно найти, например, в книге Awoday по теории категорий, см. 2.3. Обобщенные элементы) объектов, которые мы можем назвать значениями этих объектов здесь, принимая глобальные элементы как естественное и универсальное категориальное понятие для "значений".
Например, Set имеет обычные элементы (наборов, объектов Set) как глобальные элементы, что означает, что элементы любого набора A можно рассматривать как разные функции (морфизмы Set) {⋆} → A из набора единиц {⋆} к этому набору A, Для конечного множества A с |A| = n имеются n такие морфизмы, для пустого множества {} нет таких морфизмов {⋆} → {} в Set, чтобы {} "не имеет элементов" и |{}| = 0для одиночных наборов {⋆} ≊ {+} однозначно, так что |{⋆}| = |{+}| = 1, и так далее. Элементы или "значения" наборов на самом деле являются просто функциями из одноэлементного набора (1конечный объект в Set), поскольку существует изоморфизм A ≊ Hom(1, A) в Set (который CCC, чтобы Hom здесь и внутри Hom(1, A) это объект).
Так что глобальные элементы являются обобщением этого понятия элементов в Set в любую категорию с терминальными объектами. Он может быть обобщен далее с помощью обобщенных элементов (в категории множеств, множеств или пространств морфизмы определяются действиями над точками, но это не всегда так в общей категории). В общем, как только мы превращаем "значения" (элементы, точки, константы, термины) в стрелки рассматриваемой категории, мы можем рассуждать о них, используя язык этой конкретной категории.
Схожий, в Haskу нас есть, например,trueкак⊤ → Bool а также false как ⊤ → Bool:
true :: () -> Bool
true = const True
false :: () -> Bool
false = const Frue
true ≠ falseв обычном смысле, у нас также есть семья ⊥как⊤ → Bool(undefined, error "...",fix, общая рекурсия и тд)
bottom1 :: () -> Bool
bottom1 = const undefined
bottom2 :: () -> Bool
bottom2 = const $ error "..."
bottom3 :: () -> Bool
bottom3 = const $ fix id
bottom4 :: () -> Bool
bottom4 = bottom4
bottom5 :: () -> Bool
bottom5 = const b where b = b
...
⊥ ≠ false ≠ trueи это все, мы не можем найти другие морфизмы вида⊤ → Bool, чтобы⊥, falseа также trueэто единственные значения Bool который можно различить экстенсивно. Обратите внимание, что в Hask любой объект имеет значения, т.е. обитаемый, так как всегда есть морфизмы ⊤ → A для любого типа A, это делает Hask отличный от Setили любой другой нетривиальный CCC (его внутренняя логика довольно скучна, это то, о чем говорится в статье " Быстрые и бесполезные рассуждения" с точки зрения морали, нам нужно найти подмножество Haskell, которое имеет хороший CCC со здравой логикой).
Кроме того, в теории типов значения синтаксически представлены в виде терминов, которые также имеют аналогичную категориальную семантику.
И если мы говорим о "платоническом" (то есть всего, BiCCC) Haskтогда вот тривиальное доказательство A ≊ Hom(1, A) в Агде (которая хорошо отражает эту платоническую черту):
module Values where
open import Function
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality
_≊_ : Set → Set → Set
A ≊ B = ∃ λ (f : A → B) → ∃ λ (f⁻¹ : B → A) → f⁻¹ ∘ f ≡ id × f ∘ f⁻¹ ≡ id
iso : ∀ {A} → A ≊ (⊤ → A)
iso = const , flip _$_ tt , refl , refl