Полезна ли теория категорий для обучения функциональному программированию?

Я изучаю Haskell, и я очарован языком. Однако у меня нет серьезных знаний по математике или CS. Но я опытный программист.

Я хочу изучить теорию категорий, чтобы стать лучше на Хаскеле.

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

В предыдущем ответе на сайте «Теоретическая информатика» я сказал, что теория категорий является «фундаментом» для теории типов. Здесь я хотел бы сказать что-то покрепче. Теория категорий - это теория типов . И наоборот, теория типов - это теория категорий . Позвольте мне подробнее остановиться на этих моментах.

Теория категорий - это теория типов

В любом типизированных формальном языке, и даже в обычных математике с использованием неформальной нотации, мы в конце концов объявления функций с типами . В письменной форме подразумевается, что и - это некоторые вещи, называемые «типами», а - это «функция» от одного типа к другому. Теория категорий - это алгебраическая теория таких «типов» и «функций». (Официально теория категорий называет их «объектами» и «морфизмами», чтобы не наступать на теоретико-множественные пальцы традиционалистов, но все чаще я вижу, как теоретики категорий бросают такую ​​осторожность и используют более интуитивные термины: «тип»). "и" функция ". Но,A B $f : A \to B$$A$$B$$f$

Мы все воспитывались на теории множеств начиная со средней школы. Итак, мы привыкли думать о таких типах, как и как о множествах, а функции, такие как как о теоретико-множественных отображениях. Если вы никогда не думали о них таким образом, вы в хорошей форме. Вы избежали теоретико-множественного промывания мозгов. Теория категорий гласит, что существует много типов типов и функций. Таким образом, идея типов как множеств является ограничивающей. Вместо этого теория категорий аксиоматизирует типы и функции алгебраическим способом. По сути, это и есть теория категорий. Теория типов и функций. Это становится довольно сложным, включая высокие уровни абстракции. Но если вы научитесь этому, вы приобретете глубокое понимание типов и функций.B $A$$B$$f$

Теория типов - это теория категорий

Под «теорией типов» я подразумеваю любой типизированный формальный язык, основанный на жестких правилах формирования терминов, которые гарантируют, что все типы проверяются. Оказывается, всякий раз, когда мы работаем на таком языке, мы работаем в теоретико-категоричной структуре. Даже если мы используем теоретико-множественные нотации и мыслим теоретико-множественными, все же мы заканчиваем тем, что пишем вещи, которые имеют смысл категорично. Это удивительный факт .

Исторически Дана Скотт, возможно, была первой, кто осознал это. Он работал над созданием семантических моделей языков программирования, основанных на типизированном (и нетипизированном) лямбда-исчислении. Традиционные теоретико-множественные модели были неадекватны для этой цели, потому что языки программирования включают в себя неограниченную рекурсию, которой не хватает теории множеств. Скотт изобрел серию семантических моделей, в которых запечатлены явления программирования, и пришел к выводу, что набранное лямбда-исчисление точно представляет класс категорий, называемых декартовыми замкнутыми категориями . Существует множество закрытых декартовых категорий, которые не являются «теоретико-множественными». Но напечатанное лямбда-исчисление относится ко всем из них одинаково. Скотт написал хорошее эссе под названием « Соотношение теорий лямбда-исчисления«Объясняя, что происходит, отдельные части которых, по-видимому, доступны в Интернете. Оригинальная статья была опубликована в томе« To HB Curry: Очерки по комбинаторной логике, лямбда-исчислению и формализму », Academic Press, 1980. Berry and Curien пришли к той же реализации, вероятно, независимо: они определили категориальную абстрактную машину (CAM), чтобы использовать эти идеи для реализации функциональных языков, а язык, который они реализовали, назывался «CAML», который лежит в основе F # от Microsoft .

Конструкторы стандартных типов, такие как , , и т. Д., Являются функторами . Это означает, что они не только отображают типы в типы, но также выполняют функции между типами в функции между типами. Полиморфные функции сохраняют все такие функции, являющиеся результатом действий функтора. Теория категорий была изобретена в 1950-х годах Эйленбергом и Маклейном→ L i s $\times$$\to$$List$точно формализовать понятие полиморфных функций. Они назвали их «естественными преобразованиями», «естественными», потому что они единственные, которые вы можете написать с корректным типом, используя переменные типа. Таким образом, можно сказать, что теория категорий была изобретена именно для формализации полиморфных языков программирования, еще до появления языков программирования!

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

Все сказанное и сделанное, теория категорий является наиболее существенной математической теорией типов и функций. Таким образом, все программисты могут извлечь пользу из изучения теории категорий, особенно функциональные программисты. К сожалению, нет никаких учебников по теории категорий, предназначенных специально для программистов. Книги «Теория категорий для информатики», как правило, предназначены для студентов / исследователей в области теоретической информатики. Книга Бенджамина Пирса « Базовая теория категорий для компьютерщиков», пожалуй, самая читаемая из них.

Тем не менее, в Интернете есть множество ресурсов, предназначенных для программистов. Страница Haskellwiki может быть хорошей отправной точкой. В аспирантуре Мидлендса мы читаем лекции по теории категорий (среди прочих). Курс Грэма Хаттона был оценен как курс для начинающих, а мой - как продвинутый. Но оба они охватывают по существу один и тот же контент, уходя в разные глубины. У университета Чалмерса есть хорошая страница ресурса с книгами и примечаниями лекции со всего мира. Восторженный сайт блог «SIGFPE» также предоставляет много хороших интуитивные С точки зрения программиста.

Основные темы, которые вы хотели бы изучить:

• определение категорий и некоторые примеры категорий
• функторы и их примеры
• природные преобразования и примеры из них
• определения продуктов, копроизведений и показателей (функциональных пространств), начальных и конечных объектов.
• примыкания
• монады, алгебры и категории Клейсли

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

Чем больше математики вы знаете, тем легче будет изучить теорию категорий. Поскольку теория категорий является общей теорией математических структур, полезно знать некоторые примеры, чтобы понять, что означают определения. (Когда я изучал теорию категорий, мне приходилось создавать свои собственные примеры, используя мои знания семантики языка программирования, потому что в стандартных учебниках были только математические примеры, о которых я ничего не знал.) Затем появилась блестящая книга Ламбека. а Скотт назвал « Введение в категориальную логику»«которая относила теорию категорий к системам типов (то, что они называют« логикой »). Теперь можно понять теорию категорий, просто связав ее с системами типов, даже не зная множества примеров. Многие ресурсы, которые я упомянул выше, используют это подход к объяснению теории категорий.

Я постараюсь сделать это коротким и сладким. Существует неформальное соответствие между программами на Haskell и определенными классами категорий, которые можно сделать более формальными с некоторой работой. Это соответствие известно как соответствие Карри-Говарда-Ламбека и касается:

1. Типы Haskell с объектами категории
2. Термины типа с морфизмами (обратите внимание на похожие обозначения)f : A → $A\rightarrow B$ $f\colon A\rightarrow B$
3. Алгебраические типы данных с начальными объектами
4. Тип конструкторы с функторами
5. и т.д

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

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

Повторяя совет @AJed, я рекомендую обратить ваше заявление

I want to learn category theory so I can become better at Haskell.

с ног на голову: изучите Haskell, опираясь на свою интуицию программирования. Как только вы станете гуру ФП, вам может быть легче подобрать теорию категорий (если вы все еще заботитесь).

Теория категорий проста для человека с широким математическим образованием (группы, кольца, модули, векторные пространства, топология и т. Д.). Без этого фона теория категорий почти непроницаема. Прелесть теории категорий в том, что она объединяет множество, казалось бы, не связанных между собой вещей (например, к левым примыканиям забывчивых функторов относятся свободные группы, универсальные обертывающие алгебры, компактификации Стоун-Чеха, абеленизации групп и т. Д.), Что снижает сложность. Но если вы не знакомы с многочисленными примерами, которые объединяет теория категорий, теория категорий - это просто дополнительный уровень сложности, который усложняет вашу жизнь.

По моему опыту, учиться легче, опираясь на вещи, которые каждый уже знает. Как разработчик программного обеспечения, вы много знаете о программировании, и программирование на Haskell ничем не отличается от других программ, поэтому я рекомендую подходить к Haskell с прагматической точки зрения, игнорируя теорию категорий. Немного теории категорий, которая есть в Haskell, например, некоторая поддержка монад, программисту гораздо легче понять, не обходя стороной теорию категорий. В конце концов, монады представляют собой просто обобщенную композицию (и вы уже использовали монады в своей практике программирования - хотя и не подозревая, что вы это сделали), и Haskell на самом деле не поддерживает монады по-настоящему, поскольку не обеспечивает соблюдения монадических законов.

Короткий ответ: нет [но это только мнение]

Не переходите к теории категорий или другим теоретическим областям, чтобы стать хорошими в Haskell. Изучите методы функционального программирования, такие как хвостовая рекурсия, отображение, уменьшение и другие. Прочитайте как можно больше кода. Реализуйте как можно больше идей. Если у вас есть проблемы, читайте и читайте.

Если вы хотите получить хороший теоретический справочник по изучению языка Haskell и других парадигм функционального программирования, взгляните на: Введение в функциональное программирование с помощью лямбда-исчисления, Грег Майклсон (доступно онлайн). ... Есть и другие похожие книги.

Вот (длинный) пост в блоге, который дает мотивацию о том, как идеи теории категорий актуальны для практического программирования: http://cdsmith.wordpress.com/2012/04/18/why-do-monads-matter/

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

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