Какова связь между функторами в SML и теории категорий?

24

Вдоль той же мысли, что и это высказывание Андрея Бауэра в этом ответе

Сообщество Haskell разработало ряд методов, основанных на теории категорий, из которых монады наиболее известны, но их не следует путать с монадами .

Какова связь между функторами в SML и функторами в теории категорий?

Поскольку я не знаю подробностей о функторах на других языках, таких как Haskell или OCaml, если есть полезная информация, добавьте также разделы для других языков.

Гай Кодер
источник
1
Я полагаю, вы могли бы попробовать написать Дейву МакКуину электронное письмо для окончательного ответа.
Жиль "ТАК - перестань быть злым"

Ответы:

14

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

Функторы ML не являются функторами в категориальном смысле этого слова. Но они являются «функциями большего размера» в теоретико-типовом смысле.

Думайте о конкретных типах данных в типичном языке программирования как о «маленьких». Таким образом int, bool, int -> intи т.д. маленькие классы в Java являются небольшими, а также в С. Структура Мы можем собирать все типы данных в большую коллекцию под названием Type. Конструктор типа, такой как listили arrayявляется функцией от Typeдо Type. Так что это «большая» функция. Функтор ML - это чуть более сложная большая функция: она принимает в качестве аргумента несколько мелких вещей и возвращает несколько мелких вещей. «Несколько мелких вещей вместе взятых» называется структурой в ОД. С точки зрения теории типов Мартина-Лёфа мы имеем вселенную Type малых типов. Большие типы обычно называют видами . Итак, мы имеем:

  1. значения типов элементов (пример: 42 : int)
  2. типы элементов Type(например: int : Type)
  3. Подписи ML являются виды (пример: OrderedType)
  4. конструкторы типов являются элементами видов (пример: list : Type -> Type)
  5. ML СТРУКТУР являются элементами видов (пример: String : OrderedType)
  6. ML функторы функции между видами (например Map.Make : Map.OrderedType -> Make.S)

Теперь мы можем провести аналогию между ML и категориями, при которых функторы соответствуют функторам. Но мы также замечаем, что типы данных в ML похожи на «маленькие категории без морфизмов», другими словами, они больше похожи на наборы, чем на категории. Мы могли бы использовать аналогию между ML и теорией множеств:

  1. типы данных как наборы
  2. виды похожи на теоретико-множественные классы
  3. функторы похожи на функции класса
Андрей Бауэр
источник
15

Стандартная структура ML сродни алгебре . Его подпись описывает целый класс алгебр схожей формы.

F:MоNгрпF:AбрNг который добавляет мультипликативный моноид к абелевым группам для образования колец.

Большинство из этих идей были разработаны в серии статей Burstall и Goguen по разработке языка спецификаций, называемого CLEAR (ссылки c5 и c6 на странице DBLP .). В то время Дэвид Маккуин работал вместе с Burstall и Sannella и был глубоко знаком с ним. с вопросами. Стандартная модульная система ML основана на этих идеях.

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

  • Часть ответа ДА применяется, если структуры первого порядка. Тогда существуют гомоморфизмы между различными структурами одной и той же сигнатуры, и стандартные функторы ML автоматически сопоставляют их с гомоморфизмами сигнатуры результата.
  • НЕТ часть ответа применяется, когда структуры имеют операции более высокого порядка.

Означает ли это, что стандарт ML отклоняется от теории категорий? Я так не думаю. Я скорее думаю, что Standard ML делает правильные вещи, а теория категорий еще не наверстала упущенное. Теория категорий еще не знает, как обращаться с функциями более высокого порядка. Когда-нибудь, это будет.

Удай Редди
источник
«Теория категорий еще не знает, как обращаться с функциями более высокого порядка». Это звучит как еще один вопрос, потому что я думал, что теория категорий может сделать все это в качестве основы.
Гай Кодер
2
T(Икс)знак равно[ИксИкс]TвесясеИксзнак равноT(Икс)T(Икс)
Uday Reddy
Я действительно сделал это реальным вопросом .
Guy Coder
«Стандартная структура ML сродни алгебре ». Разве функторы не являются более общими, чем это? Ничто не мешает структуре содержать несвязанные объекты (типы, значения и функции), т.е. не образуя алгебру.
Didierc
2
@didierc Сигнатура для алгебр состоит из одного или нескольких видов (например, наших типов) и одной или нескольких операций (например, наших функций) и, возможно, некоторых аксиом (например, наших спецификаций). Алгебра для подписи выбирает конкретные наборы для этих видов, а также особые функции для этих операций, например , что аксиомы удовлетворены. Сигнатуры и структуры SML являются именно такими вещами, за исключением того, что SML допускает операции более высокого порядка, а алгебра - нет.
Uday Reddy
3

Насколько мне известно, нет формальной связи между функторами в теории категорий и функторами в ML (SML или OCaml, они достаточно близки для нашей цели здесь).

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

Функторы ML были крещены Дейвом МакКуином в его ревизии Модули для стандарта ML (citeseerx) 1985 года, которая появилась в Бюллетене полиморфизма (в оригинальной статье использовалось выражение «параметрический модуль» - в более поздних публикациях обычно используется прилагательное «параметризованный»). К сожалению, я не могу найти копию этого документа. В своей статье 1986 года « Использование зависимых типов для выражения модульной структуры» (citeseerx) он называет имя «как установлено».

Жиль "ТАК - перестань быть злым"
источник
2
Функторы - это не просто функции на объектах, они также отображают морфизмы. Функторы - это «морфизмы между категориями».
Андрей Бауэр
@AndrejBauer Да, функторы являются функциями на объектах. Не каждая функция на объектах является функтором, но это второстепенное соображение.
Жиль "ТАК - перестань быть злым"