Вдоль той же мысли, что и это высказывание Андрея Бауэра в этом ответе
Сообщество Haskell разработало ряд методов, основанных на теории категорий, из которых монады наиболее известны, но их не следует путать с монадами .
Какова связь между функторами в SML и функторами в теории категорий?
Поскольку я не знаю подробностей о функторах на других языках, таких как Haskell или OCaml, если есть полезная информация, добавьте также разделы для других языков.
Ответы:
Категории образуют (большую) категорию, чьи объекты являются (небольшими) категориями и морфизмы которых являются функторами между малыми категориями. В этом смысле функторы в теории категорий являются «морфизмами больших размеров».
Функторы ML не являются функторами в категориальном смысле этого слова. Но они являются «функциями большего размера» в теоретико-типовом смысле.
Думайте о конкретных типах данных в типичном языке программирования как о «маленьких». Таким образом
int
,bool
,int -> int
и т.д. маленькие классы в Java являются небольшими, а также в С. Структура Мы можем собирать все типы данных в большую коллекцию под названиемType
. Конструктор типа, такой какlist
илиarray
является функцией отType
доType
. Так что это «большая» функция. Функтор ML - это чуть более сложная большая функция: она принимает в качестве аргумента несколько мелких вещей и возвращает несколько мелких вещей. «Несколько мелких вещей вместе взятых» называется структурой в ОД. С точки зрения теории типов Мартина-Лёфа мы имеем вселеннуюType
малых типов. Большие типы обычно называют видами . Итак, мы имеем:42 : int
)Type
(например:int : Type
)OrderedType
)list : Type -> Type
)String : OrderedType
)Map.Make : Map.OrderedType -> Make.S
)Теперь мы можем провести аналогию между ML и категориями, при которых функторы соответствуют функторам. Но мы также замечаем, что типы данных в ML похожи на «маленькие категории без морфизмов», другими словами, они больше похожи на наборы, чем на категории. Мы могли бы использовать аналогию между ML и теорией множеств:
источник
Стандартная структура ML сродни алгебре . Его подпись описывает целый класс алгебр схожей формы.
Большинство из этих идей были разработаны в серии статей Burstall и Goguen по разработке языка спецификаций, называемого CLEAR (ссылки c5 и c6 на странице DBLP .). В то время Дэвид Маккуин работал вместе с Burstall и Sannella и был глубоко знаком с ним. с вопросами. Стандартная модульная система ML основана на этих идеях.
Большинство людей задаются вопросом, а как насчет морфизмов? Теоретические категории функторы имеют часть объекта и часть морфизма. Стандартные функторы ML имеют то же самое? Ответ да, и нет.
Означает ли это, что стандарт ML отклоняется от теории категорий? Я так не думаю. Я скорее думаю, что Standard ML делает правильные вещи, а теория категорий еще не наверстала упущенное. Теория категорий еще не знает, как обращаться с функциями более высокого порядка. Когда-нибудь, это будет.
источник
Насколько мне известно, нет формальной связи между функторами в теории категорий и функторами в ML (SML или OCaml, они достаточно близки для нашей цели здесь).
В теории категорий функторы - это функции, которые оперируют объектами. Они на один уровень выше морфизмов, которые часто являются функциями, которые работают с элементами (многие категории имеют объекты, которые являются множествами с некоторой алгебраической структурой, и стрелки, которые являются гомоморфизмами между этими структурами). Функтор ML - это функция, которая работает с модулями, на один уровень выше функций, работающих с базовыми значениями языка. Я думаю, что сходство заканчивается здесь.
Функторы ML были крещены Дейвом МакКуином в его ревизии Модули для стандарта ML (citeseerx) 1985 года, которая появилась в Бюллетене полиморфизма (в оригинальной статье использовалось выражение «параметрический модуль» - в более поздних публикациях обычно используется прилагательное «параметризованный»). К сожалению, я не могу найти копию этого документа. В своей статье 1986 года « Использование зависимых типов для выражения модульной структуры» (citeseerx) он называет имя «как установлено».
источник