Статус-кво теории категорий и монад в теоретической информатике?

17

Фон . Я студент бакалавриата, который интересуется исследованиями, связанными с теорией категорий, монадами и Хаскеллом, и я хочу найти тему для своей диссертации бакалавра в этой области.

Я посмотрел на бумагу

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

Поэтому я сейчас ищу недавнюю работу, связанную с монадами, и мне интересно:

  • В каких областях теоретической информатики в настоящее время проводятся исследования, связанные с теорией категорий и монад?
  • Какое исследование было построено или предложено в работе Э. Могги по монадам в теории программирования? Были ли какие-либо последующие или продолжающиеся исследования, связанные с его бумагой?
k.stm
источник
Прежде чем мы ответим на этот вопрос: это не исследовательский уровень, не так ли? Это может быть лучше подходит для cs.stackexchange.com.
Андрей Бауэр
3
@AndrejBauer Мой диплом бакалавра не будет исследовательским, но мой вопрос касается текущих исследований или, по крайней мере, исследований, выполненных в последнее десятилетие.
kstm
9
@ AndrejBauer Я не согласен. Сестринский сайт в основном предназначен для домашних заданий, тогда как здесь требуется экспертное мнение.
Юваль Фильмус
@Kaveh Это было довольно радикальное изменение, которое вы только что сделали. Вы улучшили некоторые моменты, но теперь это уже не тот вопрос, который я задавал. Когда у меня будет время завтра, я отменю некоторые твои изменения. Например, для меня важно иметь фон там. Пожалуйста, скажите мне, какие изменения вы считаете необходимыми и почему, чтобы я знал, что не нужно откатывать.
k.stm
1
@Yuval, я думаю, что многие люди в области компьютерных наук будут категорически не согласны с вашим комментарием о том, что это в основном домашние задания и что эксперты по компьютерным наукам отсутствуют . В этом случае Андрей ответил более чем на 100 вопросов по информатике .
Каве

Ответы:

15

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

Конкретные примеры монад

Вам не нужно постоянно изучать супер-общую теорию. Есть примеры монад, которые очень интересны и достаточно сложны, чтобы заполнить весь диплом бакалавра.

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

Другой конкретный пример того, что стоит изучить, был приведен Мартином Эскардо и Пауло Оливой в контексте функционалов выбора, их функций выбора, рекурсии и обратной индукции или, возможно, чтобы заинтересоваться, сначала прочитайте « Что такое последовательные игры», «Теорема Тихонова» и Сдвиг двойного отрицания имеет в общем (связанные файлы Haskell и Agda здесь ).

Математическое обоснование

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

Вариации на тему

Вы можете посмотреть на то, что не строго монады.

Например, « Идиомы» Коннора Макбрайда и Росса Патерсона : аппликативное программирование с эффектами показывает, как можно обобщить монады к чему-то, что практически уместно и проницательно.

Или вы можете посмотреть, как комонады используются для моделирования вычислительных эффектов. Кто-то должен предложить некоторые ссылки на эту тему, но хорошим началом могут быть слайды Дэвида Обертоне .

Теория модальных типов

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

Алгебраические эффекты и обработчики

[Отказ от ответственности: частично дует мой собственный рог здесь.]

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

Вы могли бы изучить, как именно алгебраические эффекты относятся к монадам. Вы можете посмотреть, как люди реализуют алгебраические эффекты и обработчики, скажем, на языке Eff или в Haskell в виде библиотеки . Это более или менее актуальное исследование.

Андрей Бауэр
источник
Привет, спасибо за этот ответ! Я нажал на вашем сайте об Eff, и похоже, что ссылка на Введение в алгебраические эффекты и обработчики устарела, то есть файл eff-lang.org/handlers-tutorial.pdfотсутствует.
k.stm
1
Я попросил Матюю исправить ссылку, пока вы можете посмотреть на arxiv.org/abs/1203.1539 .
Андрей Бауэр
Я уже. Кстати, можете ли вы дать краткий обзор базовой теории, которую мне нужно изучить, чтобы понять вашу статью? Я знаю некоторую теорию категорий, нетипизированное лямбда-исчисление и некоторую элементарную теорию вычислений и элементарную теорию программирования (я знаю, что такое денотационная семантика), но пока не намного. Я, например, уже могу сказать из раздела 3 вашей статьи, что мне нужно изучить правила типизации (возможно, типизированное лямбда-исчисление). Извините, если я настаиваю здесь.
k.stm
3
Вам следует немного узнать об универсальной алгебре и / или теории алгебраических теорий Лаввера. Если вы не знакомы с правилами набора текста, вы можете изучить общий учебник по языкам программирования, такой как TAPL Бенджамина Пирса или Практические основы языков программирования Боба Харпера .
Андрей Бауэр
1

Эта статья дает некоторые важные недавние работы с использованием монад.

NietzscheanAI
источник
1
Привет спасибо за ответ Буду признателен за небольшой контекст, то есть, если вы сможете сэкономить время, чтобы рассказать некоторые детали. (На самом деле статья содержит хорошее введение в ее содержание, но я все же хотел бы увидеть некоторый контекст для его окружения, например, если есть связанные работы и тому подобное.)
k.stm