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

118

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

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

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

Рафаэль
источник
1
Я ценю, что вы различаете программирование и CS.
13
4
«Изучение теории категорий, чтобы стать лучше в Хаскеле» немного похоже на «Изучение физики, чтобы стать лучше в теннисе»
user26756

Ответы:

115

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

Удай Редди
источник
3
@UdayReddy Я категорически не согласен с вашей идентификацией теории категорий с теорией типов. Современная теория типов, в основном, относится к типам для процессов параллелизма, например, к теории сессионных типов. Насколько мне известно, нет категорического понимания таких систем ввода.
Мартин Бергер
6
@MartinBerger Я думаю, что ваша интерпретация «теории типов» немного узкая. Однако я согласен с тем, что правильное теоретико-типовое и теоретико-категоричное понимание типов сеансов в настоящее время является хорошей исследовательской задачей, на которую я намерен потратить время.
Uday Reddy
2
@MartinBerger. Чтобы увидеть, как теория категорий применяется к более богатым понятиям вычислений, я предлагаю вам взглянуть на то, как она применяется к теории императивного программирования и семантике игр (которая снова может довольно хорошо кодировать императивные вычисления). Поэтому я не верю, что функциональное программирование обладает монополией на теорию категорий.
Uday Reddy
1
@nicolas, расслоения - это способ создания индексированных категорий, которые моделируют зависимые типы. Фибрации также можно рассматривать как очень общую форму программной логики, где означает, что отображает удовлетворяющие значения в удовлетворяющие значения. f P Qf:PQfPQ
Uday Reddy
2
«К сожалению, нет никаких учебников по теории категорий, специально предназначенных для программистов». Такой «учебник» в настоящее время более или менее существует в «Теории категорий для программистов» Бартоша Милевского . Бартош также создал серию сопроводительных лекций .
alx9r
30

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

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

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

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

Коди
источник
1
«Придумайте понятия, которые полезны для математиков, но также распространены в практике программирования на Хаскелле», - можете ли вы привести пример, или для этого потребуется слишком много предварительных знаний?
Рафаэль
7
@ Рафаэль: Монады. Стрелки. Алгебры. Коалгебрах.
Дейв Кларк
6
Функторы, двойственность, категория Клейсли, лемма Йонеды ...
Коди
4
Картелирование закрытых категорий. Карринг.
Дейв Кларк,
2
«Введение в теорию категорий для разработчиков программного обеспечения», cs.toronto.edu/~sme/presentations/cat101.pdf
Владимир Алексиев
29

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

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

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

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

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

Мартин Бергер
источник
7
Нет, если честно Haskell на самом деле является , что отличается от большинства других языков программирования, к тому , что получение прошлых предвзятое часто является самой большой проблемой. Опытные разработчики программного обеспечения, кажется, имеют больше проблем, чем люди, которые никогда не программировали раньше.
CA Макканн
5
@CAMcCann Я согласен, что некоторым опытным программам, похоже, трудно перейти, например, с Java или C # на Haskell, но я не думаю, что это потому, что в Haskell есть что-то принципиально иное. Я думаю, что это отчасти потому, что кажется другим. Идея, что вам нужно изучить теорию категорий, чтобы оценить Haskell, вероятно, помешала многим опытным разработчикам программного обеспечения достичь мастерства в Haskell. (См. Почему F # не имеет монад.) Мне, конечно, трудно думать о многих особенностях Haskell, которые также не имеют сходства в других языках.
Мартин Бергер
5
Знание теории категорий может немного помочь, но не так уж много, и изучить ее , безусловно, гораздо сложнее, чем изучение Haskell. Существуют довольно фундаментальные различия по сравнению с большинством языков (чистота, нестрогая оценка, система типов), и удаление всех терминов CT не делает их более знакомыми. С другой стороны, изучение Haskell побуждает некоторых людей изучать компьютерную томографию, потому что заимствованные идеи полезны . Ограниченная система типов F # и исключение совершенно хорошего существующего термина - недостатки, а не особенности.
CA Макканн
1
Я не знаю ни одного языка, кроме Scala, с системой типов, действительно сопоставимой с языком Haskell. Из эмпирических наблюдений не сразу понимается чистота , а нестрогая оценка (которую вы пропустили) еще сложнее. Наконец, я являюсь рабочим программистом , и я спорю , что кто - нибудь в поле собирается быть запуганно именем . Индустрия разработки программного обеспечения уже полна непрозрачного жаргона. Кроме того, система типов F # не может выражать монады напрямую - вычислительные выражения не являются первым классом, что значительно ограничивает их использование.
CA Макканн
2
CBN также концептуально прост, например, по аналогии с thunking, концепцией, которую большинство работающих программистов использовали ранее. Чистота - это то, что понимает каждый работающий программист. Haskell используется в бакалавриате в Великобритании. Когда мои ученики спрашивают меня, как заняться функциональным программированием, я часто рекомендую сначала изучить Haskell, но ученики пугаются его репутацией, так как это было инициатором вопроса. Я считаю, что главной причиной этого является ассоциация Хаскелла с теорией категорий.
Мартин Бергер
13

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

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

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

AJed
источник
1
Я поднимаю бровь на это, потому что "хвостовая рекурсия" обычно не важна для программирования на Хаскеле из-за лени. Тем не менее, «учиться на практике» - это почти всегда хороший совет.
Дэн Бертон,
@DanBurton .. интересное наблюдение. Допустим, вместо Хаскелла изучите эрланг или схему :). [Я не эксперт в Haskell, я просто выбрал его, потому что это звучит круто]
AJed
0

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

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

shvahabi
источник
Это на самом деле не отвечает на вопрос: полезно ли это для изучения функционального программирования? Какие темы в теории категорий полезны для Haskell?
Дэвид Ричерби