Что именно является категорией?

Question

Я читаю Теорию категорий для программистов и не могу понять, что именно представляет собой категория.

Давайте рассмотрим Bool тип. Является Bool категория и True или же False объекты (жители)?

Answer 1

Одна из причин, по которой вы получаете много потенциально непонятных ответов, заключается в том, что ваш вопрос немного похож на вопрос: "Давайте рассмотрим футбольный мяч. Является ли футбольный мяч" игрой "с черно-белыми полигонами и" кусочками "?"

Ответом может быть ответ @arrowd: "Нет, вы перепутали игру в футбол (Hask) со своим мячом (Bool) и полигоны (True а также False) не имеет значения."Или, это может быть ответ @freestyle:" Да, мы, безусловно, могли бы создать игру с использованием футбольного мяча и назначить одного игрока черным полигонам, а другого - белым ", но каковы будут правила? быть? "Или, это может быть ответ @Yuval Itzchakov:" Формально, "игра" - это набор из одного или нескольких игроков, ноль или более фигур, и набор правил, таких как, и т. д., и т. д."

Итак, позвольте мне добавить к путанице еще один (очень длинный) ответ, но, возможно, он ответит на ваш вопрос чуть более прямо.

Да, но это скучная категория

Вместо того, чтобы говорить о типе Haskell Bool Давайте просто поговорим об абстрактной концепции булевой логики и булевых значениях true и false. Можем ли мы сформировать категорию с абстрактными значениями "истина" и "ложь" в качестве объектов?

Ответ определенно да. Фактически, мы можем сформировать (бесконечно) много таких категорий. Все, что нам нужно сделать, это объяснить, что такое "объекты", что такое "стрелки" (иногда называемые морфизмами), и убедиться, что они подчиняются формальным математическим правилам для категорий.

Вот одна категория: пусть "объекты" будут "истинными" и "ложными", и пусть будут две "стрелки":

true -> true
false -> false

Примечание: не путайте это -> запись с функциями Haskell. Эти стрелки еще ничего не "значат", они просто абстрактные связи между объектами.

Теперь я знаю, что это категория, потому что она включает в себя обе стрелки идентичности (от объекта к себе), и она удовлетворяет свойству композиции, которое в основном говорит, что если я могу следовать за двумя стрелками из a -> b -> c тогда должна быть прямая стрелка a -> c представляя их "состав". (Опять же когда пишу a -> b -> c Я не говорю о типе функции здесь - это абстрактные стрелки, соединяющие a в b а потом b в c.) Во всяком случае, у меня недостаточно стрелок, чтобы слишком беспокоиться о композиции для этой категории, потому что у меня нет никаких "путей" между различными объектами. Я назову это "Дискретная логическая" категория. Я согласен, что это в основном бесполезно, так же как игра, основанная на многоугольниках футбольного мяча, была бы довольно глупой.

Да, но это не имеет ничего общего с логическими значениями

Вот немного более интересная категория. Позвольте объектам быть "истиной" и "ложью", и пусть стрелки будут двумя стрелками идентичности выше плюс:

false -> true

Это тоже категория. В нем есть все стрелки идентичности, и он удовлетворяет композиции, потому что, игнорируя стрелки идентичности, единственный интересный "путь", по которому я могу идти, - от "ложного" к "истинному", и мне больше некуда идти, поэтому я до сих пор не могу действительно достаточно стрелок, чтобы беспокоиться о правиле композиции.

Есть еще пара категорий, которые вы можете записать здесь. Посмотрим, сможешь ли ты найти его.

К сожалению, эти последние две категории не имеют ничего общего со свойствами булевой логики. Это правда, что false -> true выглядит немного как not операция, но тогда как мы могли бы объяснить false -> false или же true -> true и почему нет true -> false там тоже?

В конечном счете, мы могли бы так же легко назвать эти объекты "foo" и "bar" или "A" и "B" или даже не удосужиться назвать их, и категории были бы такими же действительными. Итак, хотя технически это категории с "истиной" и "ложью" в качестве объектов, они не отражают ничего интересного в булевой логике.

Быстро в стороне: несколько стрел

Я еще не упомянул о том, что категории могут содержать несколько разных стрелок между двумя объектами, поэтому могут быть две стрелки из a в b, Чтобы выделить их, я мог бы дать им имена, например:

u : a -> b
v : a -> b

Я мог бы даже иметь стрелу отдельно от личности от b к себе:

w : b -> b      -- some non-identity arrow

Правило композиции должно удовлетворяться всеми различными путями. Итак, потому что есть путь u : a -> b и путь w : b -> b (хотя он никуда не уходит), там должна быть стрелка, представляющая композицию u с последующим w от a -> b, Его значение может снова быть равно "u", или "v", или это может быть какая-то другая стрелка из a -> b, Часть описания категории объясняет, как все стрелки образуют и демонстрирует, что они подчиняются законам категории (единичный закон и ассоциативный закон, но давайте не будем беспокоиться об этих законах здесь).

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

Вроде того, если вы используете более сложные объекты

Вот более интересная категория, которая отражает некоторые "значения" логической логики. Это сложно объяснить, так что терпите меня.

Пусть объекты будут логическими выражениями с нулевым или большим количеством логических переменных:

true
false
not x
x and y
(not (y or false)) and x

Мы будем рассматривать выражения "всегда одинаковые" как один и тот же объект, поэтому y or false а также y являются одним и тем же объектом, так как независимо от значения y есть, они имеют одинаковое логическое значение. Это означает, что последнее выражение выше могло быть написано (not y) and x вместо.

Пусть стрелки представляют акт установки нуля или более логических переменных к определенным значениям. Мы пометим эти стрелки небольшими аннотациями, чтобы стрелка {x=false,y=true} представляет акт установки двух переменных, как указано. Предположим, что настройки применяются по порядку, поэтому стрелка {x=false,x=true} будет иметь такое же влияние на выражение, как {x=false} даже если они разные стрелки. Это означает, что у нас есть стрелки вроде:

{x=false} : not x -> true
{x=true,y=true} : x and y -> true

У нас также есть:

{x=false} : x and y -> false and y  -- or just "false", the same thing

Технически, две стрелки обозначены {x=false} разные стрелки. (Они не могут быть одной и той же стрелкой, потому что они являются стрелками между различными объектами.) В теории категорий очень часто используют одно и то же имя для разных стрелок, как это, если они имеют одинаковое "значение" или "интерпретацию", как эти одни делают.

Мы определим композицию стрелок, которая будет являться актом применения последовательности настроек в первой стрелке, а затем применения настроек из второй стрелки, поэтому композиция:

{x=false}: x or y -> y     and    {y=true} : y -> true

это стрелка:

{x=false,y=true}: x or y -> true

Это категория. Он имеет идентичные стрелки для каждого выражения, состоящие из отсутствия установки переменных:

{} : true -> true
{} : not (x or y) and (u or v) -> not (x or y) and (u or v)

Он определяет композицию для каждой пары стрелок, а композиции подчиняются единичным и ассоциативным законам (опять же, давайте не будем беспокоиться об этой детали здесь).

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

Эй смотри! Функтор!

У этого также есть несколько интересный функтор, который мы могли бы назвать "Отрицательным". Я не буду объяснять, что здесь за функтор. Я просто скажу, что Негейт отображает эту категорию на себя:

• принимая каждый объект (логическое выражение) к его логическому отрицанию
• перевод каждой стрелки в новую стрелку, представляющую одинаковые подстановки переменных

Итак, стрелка:

{a=false} : (not a) and b -> b

функтор Negate сопоставляется с:

{a=false} : not ((not a) and b) -> not b

или, проще говоря, используя правила булевой логики:

{a=false} : a or (not b) -> not b

которая является действительной стрелкой в ​​исходной категории.

Этот функтор отражает идею о том, что "отрицание логического выражения" эквивалентно "отрицанию его конечного результата" или, возможно, в более общем смысле, что процесс замены переменных в выражении с отрицанием имеет ту же структуру, что и исходное выражение. Может быть, это не слишком увлекательно, но это просто длинный ответ о переполнении стека, а не учебник на 500 страниц по теории категорий, верно?

Bool как часть Hask категория

Теперь давайте перейдем от разговора об абстрактных логических категориях к вашему конкретному вопросу: Bool Тип Haskell - это категория с объектами True а также False,

Ответы, приведенные выше, по-прежнему применимы в той степени, в которой этот тип Хаскеля можно использовать в качестве модели логической логики.

Тем не менее, когда люди говорят о категориях в Haskell, они обычно говорят о конкретной категории Hask где:

• объекты являются типами (например, Bool, Int, так далее.)
• стрелки являются функциями Haskell (например, f :: Int -> Double). Наконец, синтаксис Haskell и наш синтаксис абстрактной категории совпадают - функция Haskell f можно рассматривать как стрелку от объекта Int к объекту Double).
• композиция является регулярной функцией композиции

Если мы говорим об этой категории, то ответ на ваш вопрос: нет, в Hask категория, Bool является одним из объектов, а стрелки являются функциями Haskell, такими как:

id :: Bool -> Bool
not :: Bool -> Bool
(==0) :: Int -> Bool

foo :: Bool -> Int
foo b = if b then 10 else 15

Чтобы сделать вещи более сложными, объекты также включают в себя типы функций, поэтому Bool -> Bool является одним из объектов. Один пример стрелки, которая использует этот объект:

and :: Bool -> (Bool -> Bool)

которая является стрелкой от объекта Bool к объекту Bool -> Bool,

В этом сценарии True а также False не являются частью категории. Значения Haskell для типов функций, таких как sqrt или же length являются частью категории, потому что они стрелки, но True а также False являются нефункциональными типами, поэтому мы просто оставляем их вне определения.

Теория категорий

Обратите внимание, что эта последняя категория, как и первые категории, на которые мы смотрели, не имеет абсолютно никакого отношения к булевой логике, хотя Bool является одним из объектов. На самом деле, в этой категории, Bool а также Int выглядят примерно одинаково - это просто два типа, которые могут иметь стрелки, выходящие или входящие в них, и вы никогда не узнаете этого Bool был о правде и ложь или что Int представлены целые числа, если вы просто смотрели на Hask категория.

Это фундаментальный аспект теории категорий. Вы используете определенную категорию для изучения определенного аспекта какой-либо системы. Так или иначе Bool категория или часть категории - это своего рода неопределенный вопрос. Лучший вопрос был бы, "это конкретный аспект Bool что меня интересует то, что можно представить как полезную категорию? "

Категории, которые я дал выше, примерно соответствуют этим потенциально интересным аспектам Bool:

• Категория "Дискретный логический тип" представляет Bool как простой математический набор из двух объектов, "истина" и "ложь", без дополнительных интересных функций.
• Категория "ложь -> истина" представляет порядок логических значений, false < true где каждая стрелка представляет оператор '<='.
• Категория логических выражений представляет модель оценки для простых логических выражений.
• Hask представляет собой набор функций, чьи типы ввода и вывода могут быть логическим типом или функциональным типом, включающим логический и другие типы.

Answer 2

Если вы говорите о Hask категория, то нет. Hask это категория, а объекты являются типами Haskell. То есть, Bool это объект, и True/False здесь даже не говорили Описание Hask можно найти на вики Haskell. Есть также разговоры, что Hask даже не правильная категория, прочитайте это.