Начальная страница

Все переводы разделены на 2 группы: «Книги» и «Статьи». Каждая из групп содержит список названий-ссылок (с указанием авторов) на соответствующие записи (если название не превращено в ссылку, запись только запланирована).

Все записи структурированы единообразно, в соответствии со следующим шаблоном:

Это перевод … (предыдущий раздел — <URL-ссылка>, оглавление — <URL-ссылка>)

<URL-ссылка содержимого> [включает подразделы: …]

Следующий раздел — <URL-ссылка>

где, <URL-ссылка> — название-ссылка; квадратные скобки указывают на необязательность соответствующего текста; <URL-ссылка содержимого> — название-ссылка, начинающаяся с «Содержимое …» и указывающая на текст данного раздела в pdf-формате.

Текст в pdf-формате не содержит непосредственно возможности его комментирования. Комментарии можно размещать в записи, откуда исходит <URL-ссылка содержимого>. Сделано это для того, чтобы формирование комментариев и просмотр содержимого можно было осуществлять параллельно, поскольку содержимое всегда открывается в новом окне.

Просьба в комментарии указывать номер страницы комментируемого текста.

…

Книги

• Гомотопическая теория типов (Международный коллектив авторов)
• Лекции по теории категорий (Turi)
• Теория категорий для программистов (Milewski)

Статьи

• Бесплатные теоремы (Wadler)
• Универсальная коалгебра (Rutten)

Реклама

Теория категорий для программистов (перевод глав книги Б. Милевски)

Предисловие редактора перевода

Исходный авторский текст расположен по адресу:

https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

В основу перевода первых глав включены варианты, подготовленные М.Страховым (Monnoroch на Хабрахабр: предисловие и гл.1-4), А.Бирюковым совместно с Bodigrim (leshabirukov, Bodigrim на Хабрахабр: гл.5-7). Комплектность перевода соответствует текущему состоянию книги у автора. Активное участие в вычитке переводов принимает А.Бирюков.

Основная особенность переводов, отличающая текст от авторского, заключается в цветовом выделении формальных фрагментов. Синим цветом выделены математические формулы и символы, а также программные фрагменты, набранные моноширинным шрифтом, на псевдо Haskell. Пурпурный цвет выделяет программные фрагменты на C++ и Haskell. Помимо этого везде черным полужирным начертанием выделены обозначения категорий. (Цель этой самодеятельности — улучшить восприятие текста; убрать это, при необходимости, будет нетрудно).

С благодарностью принимаются любые замечания по переводу и офрмлению текста. (Согласование текста из разных глав, например, существуют повторы при введении новых терминов, будет произведено после авторского завершения работы; возможно Милевски внесет некоторые изменения после завершения).

---

Предисловие

Часть I

1. Категория: суть композиции
2. Типы и функции
3. Большие и малые категории
4. Категории Клейсли
5. Произведения и копроизведения
6. Простые алгебраические типы данных
7. Функторы
8. Функториальность
9. Функциональные типы
10. Естественные преобразования

Часть II

1. Теория категорий и декларативное программирование
2. Пределы и копределы
3. Свободные моноиды
4. Представимые функторы
5. Лемма Йонеды
6. Вложение Йонеды

Часть III

1. Все о морфизмах
2. Сопряжения
3. Свободные / забывающие сопряжения
4. Монады: определение программиста
5. Монады и эффекты
6. Монады с категорной точки зрения
7. Комонады
8. F-алгебры
9. Алгебры для монад
10. Концы и коконцы
11. Расширения Кана
12. Обогащенные категории
13. Топосы
14. Теории Ловера
15. Монады, моноиды и категории

 

(HoTT) Гомотопические n-типы

Это перевод 7 главы книги (предыдущий раздел — (HoTT) Высшие индуктивные типы, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

• Определение n-типов
• Доказательства единственности тождественности
• Усечения
• Копределы n-типов
• Связность
• Ортогональная факторизация
• Модальности

(HoTT) Высшие индуктивные типы

Это перевод 6 главы книги (предыдущий раздел — (HoTT) Индукция, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

• Введение
• Принципы индукции и зависимые пути
• Интервал
• Окружности и сферы
• Надстройки
• Клеточные комплексы
• Концентраторы и спицы
• Амальгамы
• Усечения
• Частные
• Алгебра
• Лемма сглаживания
• Общий синтаксис высших индуктивных определений

Следующий раздел — (HoTT) Гомотопические n-типы

(HoTT) Индукция

Это перевод 5 главы книги (предыдущий раздел — (HoTT) Эквивалентность, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

• Введение в индуктивные типы
• Единственность индуктивных типов
• W-типы
• Индуктивные типы являются инициальные алгебры
• Гомотопически-индуктивные типы
• Общий синтаксис индуктивных определений
• Обобщения индуктивных типов
• Типы тождественности и системы тождественности

Следующий раздел — (HoTT) Высшие индуктивные типы

(Rutten) Универсальная коалгебра

Это перевод статьи Раттена (J.J.M.M. Rutten, Universal coalgebra: a theory of systems, 1996) об универсальных коалгебрах, рассматриваемых в контексте описания систем (исходный текст расположен по адресу — Текст оригинальной статьи).

Содержимое перевода статьи включает:

1. Введение
2. Коалгебры, гомоморфизмы и взаимоподобие
3. Системы
4. Пределы и копределы систем
5. Основные сведения о взаимоподобиях
6. Подсистемы
7. Три теоремы об изоморфизмах
8. Простые системы и коиндукция
9. Терминальные системы
10. Существование терминальных систем
11. Примеры коиндуктивных определений
12. Примеры доказательств по коиндукции
13. Индукция и коиндукция
14. Сравнение систем
15. Косвободность и комногообразие систем
16. Динамические системы и символическая динамика
17. Замечания и связанные с этим работы
18. Дополнения о множествах и категориях

(HoTT) Эквивалентность

Это перевод 4 главы книги (предыдущий раздел — (HoTT) Множества и логика, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

• Квазиобратные
• Полусопряженные эквивалентности
• Би-обратимые отображения
• Стягиваемые слои
• Об определении эквивалентностей
• Сюръекции и вложения
• Свойства замкнутости эквивалентностей
• Классификатор объектов
• Унивалентность означает функциональную экстенсиональность
• Примечания
• Упражнения

Следующий раздел — (HoTT) Индукция

(HoTT) Множества и логика

Это перевод 3 главы книги (предыдущий раздел — (HoTT) Гомотопическая теория типов, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

• Множества и n-типы
• Высказывания как типы?
• Простые высказывания
• Классическая и интуиционистская логики
• Подмножества и пропозициональное изменение размера
• Логика простых высказываний
• Пропозициональное усечение
• Аксиома выбора
• Принцип единственности выбора
• Когда высказывания усекаются?
• Стягиваемость
• Примечания
• Упражнения

Следующий раздел — (HoTT) Эквивалентность

(FreeTrm) «Бесплатные» теоремы

Это перевод пересмотренного варианта статьи Уодлера (Philip Wadler), представленной на 4 Международном симпозиуме по языкам функционального программирования и компьютерной архитектуре в Лондоне, сентябрь 1989 года (исходный текст расположен по адресу — https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf).

Содержимое перевода статьи включает:

1. Введение
2. Объяснение параметричности
3. Применение параметричности
4. Полиморфное λ-исчисление
5. Семантика полиморфного λ-исчисления
6. Теорема о параметричности
7. Неподвижные точки