Фон . Я студент бакалавриата, который интересуется исследованиями, связанными с теорией категорий, монадами и Хаскеллом, и я хочу найти тему для своей диссертации бакалавра в этой области.
Я посмотрел на бумагу
- Эудженио Могги , « Понятия вычислений и монад », 1991,
и я пока не очень разбираюсь в этом. Возможно, мне понадобится некоторое время, чтобы полностью понять это. Но прежде чем тратить больше времени на его изучение, я хочу лучше понять сферу и ее исследовательский потенциал. Я недавно говорил с моим профессором об этом, и он сказал мне, что монады были в моде в исследовательском сообществе еще в 90-х годах, но в настоящее время они вышли из моды.
Поэтому я сейчас ищу недавнюю работу, связанную с монадами, и мне интересно:
- В каких областях теоретической информатики в настоящее время проводятся исследования, связанные с теорией категорий и монад?
- Какое исследование было построено или предложено в работе Э. Могги по монадам в теории программирования? Были ли какие-либо последующие или продолжающиеся исследования, связанные с его бумагой?
Ответы:
Со времени работы Эухенио Могги произошел ряд разработок, касающихся использования монад в теории вычислений. Я не могу дать исчерпывающий отчет, но вот некоторые моменты, с которыми я знаком, другие могут ответить своими ответами.
Конкретные примеры монад
Вам не нужно постоянно изучать супер-общую теорию. Есть примеры монад, которые очень интересны и достаточно сложны, чтобы заполнить весь диплом бакалавра.
Мне очень нравится блог Дэна Пипони, где он приводит удивительные примеры того, как монады можно использовать для смешивания функционального программирования и математики. Ищите его работы на узлах и заплетайте монады, например.
Другой конкретный пример того, что стоит изучить, был приведен Мартином Эскардо и Пауло Оливой в контексте функционалов выбора, их функций выбора, рекурсии и обратной индукции или, возможно, чтобы заинтересоваться, сначала прочитайте « Что такое последовательные игры», «Теорема Тихонова» и Сдвиг двойного отрицания имеет в общем (связанные файлы Haskell и Agda здесь ).
Математическое обоснование
Монады происходят из теории категорий и намного старше, чем Эудженио Могги. Вы можете изучить фоновую теорию, если вы склонны к математике. Например, вы можете атаковать теорему Бека о монадичности . Теоретик-компьютерщик никогда не знает слишком много математики.
Вариации на тему
Вы можете посмотреть на то, что не строго монады.
Например, « Идиомы» Коннора Макбрайда и Росса Патерсона : аппликативное программирование с эффектами показывает, как можно обобщить монады к чему-то, что практически уместно и проницательно.
Или вы можете посмотреть, как комонады используются для моделирования вычислительных эффектов. Кто-то должен предложить некоторые ссылки на эту тему, но хорошим началом могут быть слайды Дэвида Обертоне .
Теория модальных типов
В теории гомотопических типов, а также в теории типов в целом монады появляются в форме теории модальных типов . Недавно теория модального типа была рассмотрена в теории гомотопического типа, потому что операторы усечения являются примерами модальных операторов. Кроме того, существует связная теория гомотопического типа, в которой модальные операторы (которые являются монадами) играют существенную роль.
Алгебраические эффекты и обработчики
[Отказ от ответственности: частично дует мой собственный рог здесь.]
Некоторое время назад Гордон Плоткин и Джон Пауэр наблюдали, что многие вычислительные эффекты - это не просто какие-либо монады, а специальные монады, возникающие из алгебраических теорий. Это привело к совершенно новой обработке вычислительных эффектов, известных как алгебраические эффекты . Позже Гордон Плоткин и Матия Претнар представили обработчики, и вместе с алгебраическими эффектами они образуют очень хорошую теорию вычислительных эффектов. Одним из преимуществ этого подхода является то, что алгебраические теории могут быть легко объединены, а монады - нет.
Вы могли бы изучить, как именно алгебраические эффекты относятся к монадам. Вы можете посмотреть, как люди реализуют алгебраические эффекты и обработчики, скажем, на языке Eff или в Haskell в виде библиотеки . Это более или менее актуальное исследование.
источник
eff-lang.org/handlers-tutorial.pdfотсутствует.Эта статья дает некоторые важные недавние работы с использованием монад.
источник