Я не думаю, что понятие «бесплатно» определено так четко, как вам кажется. Хотя я думаю, что общее мнение состоит в том, что это действительно левый сопряженный функтор забывчивости, проблема заключается в том, что "забывчивый" означает. Существуют четкие определения в некоторых широких случаях, особенно для конкретных категорий.
Универсальная алгебра обеспечивает широкий подход, который охватывает почти все «алгебраические» структуры (над множествами). Результату дается «подпись», которая состоит из сортировок, операций и уравнений, вы строите алгебру терминов (т. Это свободная алгебра, созданная из этой подписи. Например, мы обычно говорим о моноидах как о множестве, снабженном ассоциативным умножением и единицей. В коде свободная алгебра до факторизации будет выглядеть так:
data PreFreeMonoid a
= Unit
| Var a
| Mul (PreFreeMonid a) (PreFreeMonoid a)
Затем мы будем частно использовать отношение эквивалентности, полученное из уравнений:
Mul Unit x = x
Mul x Unit = x
Mul (Mul x y) z = Mul x (Mul y z)
Но вы можете показать, что полученный частный тип изоморфен спискам. В многосортном случае у нас будет семейство алгебр терминов, по одной для каждого вида.
Один из способов переформулировать это категорически — использовать понятие (слегка обобщенное) теории Ловера. . Имея сигнатуру с набором сортировок, S, мы можем создать небольшую категорию, назовем ее T, объекты которой представляют собой списки элементов S. >. Эти небольшие категории будут называться теориями в целом. Операции сопоставляются со стрелками, источник и цель которых соответствуют соответствующим элементам. Мы свободно добавляем стрелки «tupling» и «projection», чтобы, например. [A,B,A] становится продуктом [A][B ][А]. Наконец, мы добавляем коммутативные диаграммы (то есть уравнения между стрелками), соответствующие каждому уравнению в подписи. На данный момент T по существу представляет собой термин алгебра(ы). На самом деле, фактическая интерпретация или модель этого термина алгебра — это просто сохраняющий конечный продукт функтор T Set, напишите Mod(T ) для категории функторов, сохраняющих конечное произведение, из T Set. В случае с одиночной сортировкой у нас был бы базовый функтор множеств, но в общем случае мы получаем семейство множеств с S-индексом, т. е. у нас есть функтор U : < strong>Mod(T) УстановитьS, где мы просматриваем S< /em> в качестве дискретной категории здесь. U — это просто U(m)(s) = m([s]). На самом деле мы можем вычислить левое сопряженное. Во-первых, у нас есть семейство наборов, индексированное элементами S, назовем его G. Затем нам нужно построить сохраняющий конечный продукт функтор T Set, но любой функтор в Set (т.е. copresheaf) копредел представимых объектов, что в данном случае означает частное следующего (зависимого) типа суммы:
Бесплатно(G)(s) = t:T.T(< em>t,s)Free(G)(t)
Если Free(G) сохраняет конечный продукт, то в t = [A,B< /em>], например, у нас было бы:
T([A,B],s)Free(G)( [A,B]) = T([A,B], s)Бесплатно(G)([A])Бесплатно(G)([B< /эм>])
и мы просто определяем Free(G)([A]) = G(A) для каждого A в S производит:
T([A,B],s)Free(G)( [A]) Бесплатно(G)([B]) = T([A< /em>,B],s)G(A)G( Б)
В целом это говорит о том, что элемент Free(G)([A]) состоит из стрелки T в [A ] и список элементов соответствующих множеств, соответствующих источнику этой стрелки, т. е. арности терма по модулю уравнений, которые заставляют его вести себя разумно и подчиняться уравнениям из подписи, но которые я не собираюсь уточнить. Для умножения моноида у нас была бы стрелка m : [A,A] [A], и это привело бы к кортежи (m, x, y), где x и y — элементы G(A), соответствующий такому термину, как m(x, y). Переделывая это определение как рекурсивное, нужно взглянуть на уравнения, по которым мы частно используем.
Есть и другие вещи, которые нужно проверить, чтобы показать, что Free U свободна, но это не так уж сложно. После этого UFree становится монадой на SetS.
Преимущество теории Лоувера в том, что ее легко обобщить несколькими способами. Один из простых способов — заменить Set другим топосом E. На самом деле категории ориентированных мультиграфов образуют топос, но я не верю, что вы можете (легко) рассматривать категории как теории над Графиком. Другим направлением расширения теорий Ловера является рассмотрение доктрин, отличных от функторов, сохраняющих конечное произведение, в частности limit сохраняющие функторы, также известные как левые точные или лексические функторы, представляют собой интересный точка. Как небольшие категории, так и ориентированные мультиграфы (которые классификаторы иногда называют колчанами) можно рассматривать как модели категории. с конечными пределами. Существует прямое включение теории ориентированных мультиграфов в теорию малых категорий. Это, наоборот, индуцирует функтор cat Graph просто путем предварительной композиции. слева от этого тогда (почти) левые расширения Kan вдоль этого включения. Эти левые расширения Кана будут встречаться в Set, поэтому в конечном итоге они являются просто копределами, которые являются просто частными (зависимыми) типами сумм. (Технически вам нужно проверить, что результирующие расширения Кана сохраняют конечный предел. Нам также помогает тот факт, что модели теории графов по существу являются произвольными функторами из теории графов. Это происходит потому, что теория графов состоит только из унарных операций.)
Однако ничто из этого не помогает для бесплатных монад. Однако оказывается, что одна конструкция объединяет все это, включая свободные монады. Возвращаясь к универсальной алгебре, это тот случай, когда каждая сигнатура без уравнений порождает (полиномиальный) функтор, чей rel="noreferrer">начальная алгебра — это алгебра свободных терминов. лемма Ламбека предполагает, и легко доказать, что исходная алгебра является просто копределом повторных применений функтора. Приведенный выше общий результат основан на аналогичном подходе, и соответствующий случай для свободных монад — это случай неуказанного эндофунктора, в котором вы начинаете видеть определение Free, которое вы дали, но на самом деле его полная разработка требует развертывания многих конструкций.
Откровенно говоря, я почти уверен, что на самом деле в мире FP произошло следующее. Если вы посмотрите на PreFreeMonoid, на самом деле это свободная монада. PreFreeMonoid Void - это начальная алгебра для функтора, к которому может привести сигнатура моноида (за вычетом уравнений). Если вы знакомы с использованием функторов для исходных алгебр и даже начинаете думать об универсальной алгебре, вы почти наверняка в конечном итоге определите такой тип, как data Term f a = Var a | Op (f (Term f a)). Легко убедиться, что это монада, как только вы решите задать вопрос. Если вы хотя бы смутно знакомы с отношением монад к алгебраическим структурам или к подстановке терминов, вы можете довольно быстро задать вопрос. На ту же конструкцию можно наткнуться с точки зрения реализации языка программирования. Если вы прямо поставили перед собой цель построить свободную монадную конструкцию в Haskell, есть несколько интуитивных способов прийти к правильному определению, особенно в сочетании с некоторыми рассуждениями, основанными на уравнениях/параметрах. На самом деле, «моноидный объект в категории эндофункторов» весьма наводит на размышления.
('Очень хотелось бы, чтобы этот StackExchange имел поддержку MathJax.)
person
Derek Elkins left SE
schedule
20.11.2016
