Конструктивная математика . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216
Расширение лямбда исчисления . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216
14.2 Комбинаторная логика . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216
Связь с лямбда-исчислением . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217
Немного истории . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218
14.3 Лямбда-исчисление с типами . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219
14.4 Краткое содержание . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219
14.5 Упражнения . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219
15 Теория категорий
221
15.1 Категория . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
15.2 Функтор . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223
15.3 Естественное преобразование . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224
15.4 Монады . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226
Категория Клейсли . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226
15.5 Дуальность . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 227
15.6 Начальный и конечный объекты . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228
Начальный объект . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228
Конечный объект . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229
15.7 Сумма и произведение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229
15.8 Экспонента . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 232
15.9 Краткое содержание . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233
15.10Упражнения . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233
16 Категориальные типы
234
16.1 Программирование в стиле оригами . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234
16.2 Индуктивные и коиндуктивные типы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 238
Существование начальных и конечных объектов . . . . . . . . . . . . . . . . . . . . . . . . . . 239
16.3 Гиломорфизм . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 241
16.4 Краткое содержание . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 244
16.5 Упражнения . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 244
17 Дополнительные возможности
245
17.1 Пуд сахара . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 245
Сахар для списков . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 245
Сахар для монад, do-нотация . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 246
17.2 Расширения . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 248
Обобщённые алгебраические типы данных . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 249
Семейства типов . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 252
Классы с несколькими типами . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 254
Экземпляры классов для синонимов . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255
Функциональные зависимости . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255
Ограничение мономорфизма . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256
Полиморфизм высших порядков . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256
Лексически связанные типы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257
И другие удобства и украшения . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 258
17.3 Краткое содержание . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 258
17.4 Упражнения . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 258
8