Ответ 1

(Я буду использовать слова с их значением из теории математики/категории, а не программирования, если только я 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 не является.

Знают ли значения даже в категории Хаска (или в общей теории категорий)?

Категории не имеют значений в теории категорий, они просто имеют объекты и морфизмы, которые рассматриваются как вершины и направленные ребра. Объекты не должны иметь значений, а значения не являются частью теории категорий.

Ответ 2

Как я прокомментировал ответ Andrew (что в противном случае очень хорошо), вы можете рассматривать значения в типе как объекты этого типа как категории и рассматривать функции как функторы. Для полноты здесь есть два пути:

Устанавливает как расточные категории

Одним из наиболее часто используемых инструментов в математике является "сетоид", т.е. набор с отношением эквивалентности по нему. Мы можем думать об этом категорически через понятие "группоид". Группоид - это категория, где каждый морфизм имеет обратный такой, что 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, когда он встречает один, либо должен дать тот же ответ, независимо от того, что ему было дано. Вам остается показать, что на самом деле это функтор.

Ответ 3

В то время как есть некоторые другие, довольно замечательные ответы, здесь все они несколько упускают ваш первый вопрос. Чтобы быть ясным, ценности просто не существуют и не имеют никакого значения в категории Hask. Это просто не то, о чем Хаск говорит.

Вышеизложенное кажется немного глупым, чтобы сказать или почувствовать, но я его поднимаю, потому что важно отметить, что теория категорий предоставляет только один объектив для изучения гораздо более сложных взаимодействий и структур, доступных в чем-то сложном, как язык программирования. Неплохо ожидать, что вся эта структура будет включена в довольно простое понятие категории. [1]

Другой способ сказать это то, что мы пытаемся проанализировать сложную систему, и иногда полезно рассматривать ее как категорию, чтобы искать интересные шаблоны. Именно это мышление позволяет нам ввести Hask, убедитесь, что оно действительно образует категорию, заметим, что Maybe, кажется, ведет себя как Functor, а затем использует все эти механики для записи условий согласованности.

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, исследуя отображение стрелки нашего endofunctor Maybe. Здесь нам нужен способ сопоставить стрелки Хаска со стрелками Хаска. Предположим теперь, что это не функция Хаскелла - это не обязательно, чтобы подчеркнуть ее, мы будем писать ее по-другому. Если f является функцией Хаскелла a -> b, то Maybe [f] является некоторой другой функцией Haskell Maybe a -> Maybe b.

Теперь трудно не перескакивать вперед и просто начинать с вызова Maybe [ f] "fmap f", но мы можем сделать немного больше работы, прежде чем совершать этот переход. Возможно, [f] должен иметь определенные условия согласованности. В частности, для любого типа a в Hask мы имеем стрелку id. В нашем метаязыке мы могли бы назвать это id [a], и мы знаем, что это также имя Haskell id :: a -> a. В целом, мы можем использовать их для формулировки условий когерентности эндонуктора:

Для всех объектов в Hask a мы имеем, что Maybe [id [a]] = id [Maybe a]. Для любых двух стрелок в Hask f и g мы имеем, что Maybe [f . g] = Maybe [f]. Может быть, [g].

Последний шаг - заметить, что Maybe [_] просто реализуется как функция Haskell как значение объекта Hask forall a b . (a -> b) -> (Maybe a -> Maybe b). Это дает нам Functor.

В то время как вышеизложенное было довольно техническим и сложным, важно отметить, что понятия Хаска и категориальных эндофунторов прямо и отдельно от их экземпляра Haskell. В частности, мы можем обнаружить всю эту структуру, не введя необходимость существования fmap в качестве реальной функции Хаскеля. Hask - это категория, не представляющая ничего на уровне значений.

То, где живет реальное бьющееся сердце зрения Хаска как категории. Обозначение, которое идентифицирует endofunctors на Hask с Functor, требует гораздо большего размытия строки.

Это размытие строки оправдано, потому что Hask имеет экспоненты. Это сложный способ сказать, что существует объединение между целыми пучками категориальных стрелок и особыми специальными объектами в Hask.

Чтобы быть более явным, мы знаем, что для любых двух объектов Hask, скажем a и b, мы можем говорить о стрелках между этими двумя объектами, которые часто обозначаются как Hask (a, b). Это всего лишь математический набор, но мы знаем, что в Hask есть еще один тип, который тесно связан с Hask (a, b): (a -> b)!

Так странно.

Я изначально заявил, что общие значения Хаскелла абсолютно не представлены в категорическом представлении Хаска. Затем я продолжил демонстрировать, что мы можем многое сделать с Hask, используя только его категориальные понятия и фактически не вставляя эти фрагменты внутри Haskell в качестве значений.

Но теперь я отмечаю, что значения типа типа a -> b действительно существуют как все стрелки в металингвистическом наборе Hask (a, b). Это довольно трюк, и именно это металингвистическое размытие делает категории с экспонентами настолько интересными.

Мы можем сделать немного лучше, хотя! Hask также имеет терминальный объект. Мы можем говорить об этом металингвистически, называя его 0, но мы также знаем об этом как тип Haskell (). Если мы посмотрим на любой объект Hask a, мы знаем, что в Hask имеется целый набор категориальных стрелок ((), a). Далее, мы знаем, что они соответствуют значениям типа () -> a. Наконец, поскольку мы знаем, что при любой функции f :: () -> a мы можем сразу получить a, применив (), можно сказать, что категориальные стрелки в Hask ((), a) - это точно значения Haskell типа a.

Который должен либо быть совершенно запутанным, либо невероятно умопомрачительным.

Я собираюсь положить конец этому несколько философски, придерживаясь моего первоначального заявления: Hask вообще не говорит о значениях Haskell. Это действительно не так, как чистая категория --- категории интересны именно потому, что они очень просты и, следовательно, не нужны все эти экстра-категориальные понятия типов и значений и включение typeOf и т.п.

Но я также, возможно, плохо показал, что даже в качестве строго определенной категории у Hask есть что-то похожее, очень похожее на все значения Haskell: стрелки Hask ((), a) для каждого объекта Hask a.

Философски мы можем утверждать, что эти стрелки на самом деле не являются значениями Haskell, которые мы ищем - они просто stand-ins, категоричные издевательства. Вы можете утверждать, что это разные вещи, но просто встречаются друг с другом со значениями Haskell.

Я действительно думаю, что действительно важная идея иметь в виду. Эти две вещи разные, они просто ведут себя одинаково.

Очень похоже. Любая категория позволяет вам составлять стрелки, поэтому предположим, что мы выбираем некоторую стрелку в Hask (a, b) и некоторую стрелку в Hask ((), a). Если мы объединим эти стрелки с категорией, получим стрелку в Hask ((), b). Перевернув все это на его голове немного, мы могли бы сказать, что то, что я только что сделал, это найти значение типа a -> b, значение типа a, а затем объединить их для создания значения типа b.

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

Вот что делает такие категории, как Хаск, настолько интересными. В широком смысле такие категории называются декартовыми закрытыми категориями или CCC. Из-за наличия как исходных объектов, так и экспонент (которые также требуют продуктов) у них есть структуры, которые полностью моделируют типизированное лямбда-исчисление.

Но они все еще не имеют значений.

[1] Если вы читаете это, прежде чем читать остальную часть своего ответа, продолжайте читать. Оказывается, хотя абсурдно ожидать, что это произойдет, на самом деле это действительно так. Если вы читаете это после прочтения всего моего ответа, тогда давайте просто подумаем о том, насколько классны CCC.

Ответ 4

Есть несколько способов поставить вещи с точки зрения категорий. Специально языки программирования, которые оказываются очень богатыми конструкциями.

Если мы выберем категорию Hask, мы просто установим уровень абстракции. Уровень, где не так удобно говорить о значениях.

Однако константы могут быть смоделированы в Hask как стрелка от конечного объекта() до соответствующего типа. Затем, например:

• True:() → Bool
• 'a':() → Char

Вы можете проверить: Barr, Wells - Теория категорий для вычислений, раздел 2.2.

Ответ 5

Любая категория с терминальным объектом (или с терминальным объектом * 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 с разумной логикой).

Кроме того, значения Type Theory синтаксически представлены как термины, которые снова имеют аналогичную категориальную семантику.

И если мы говорим о "платоническом" (т.е. total, 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