Идиомы функционального программирования
Санкт-Петербург, осень 2015
Описание
Данный курс правильно было бы назвать «некоторые приёмы функционального программирования на статически типизированных языках». Так или иначе эти приемы основаны на использовании полиморфизма и функций высшего порядка и часто позволяют выразить то, что в других языках реализовывается ad hoc.
В качестве основного языка будет использован Haskell, хотя в большинстве случаев рассматриваемые приёмы могут быть перенесены в другие строго типизированные языки (например, Objective Caml).
Примерный (и неполный) перечень тем, которые предполагается затронуть:
- Функции с переменным числом аргументов («variadic functions»).
- Однородная обработка кортежей.
- Вычисления на уровне типов («type-level computations»).
- Расширяемые типы данных («expression problem»).
Некоторая литература:
- Olivier Danvy. Functional Unparsing // J. Funct. Program., 1998, Vol. 8, №6, P. 621—625.
- Oleg Kiselyov. Polyvariadic functions and keyword arguments: pattern-matching on the type of the context.
- Daniel Fridlender, Mia Indrika. Do We Need Dependent Types? // J. Funct. Program., 2001, Vol. 10, P. 409—415.
- Oleg Kiselyov, Ralf Lammel, Keean Schupke. Strongly Typed Heterogeneous Collections // Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, 2004, P. 96—107.
- Arthur I.Baars, S.Doaitse Swierstra. Typing Dynamic Typing // Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming, 2002, P. 157--166.
- Wouter Swierstra. Data Types a la Carte // J. Funct. Program., 2008, Vol. 18, № 4, P. 423—436.
Преподаватели
Список лекций
Функции с переменным числом аргументов (variadic functions) представляют собой удобное средство программирования. В большинстве ситуаций поддержка функций с переменным числом агрументов специально встроена в язык (например, С/C++, Java). Кроме того, далеко не всегда такая поддержка реализована в безопасном стиле (type-safe). На данном занятии мы убедимся, что при наличии определенных средств в языке безопасные функции с переменным числом аргументов могут быть выражены естественным образом.
Представление натуральных чисел в форме Пеано, трансляция чисел в нумералы Чёрча в задаче об однородной обработке кортежей.
Проблема overlapping instances. Причины возникновения, интерпретация. Обобщение головы
, использование эквивалентности типов.
Экзистенциальные типы, абстракция относительно схемы свойств.
Эквивалентность по Лейбницу. Представление лейбницевской эквивалентности типов в терминах Haskell. Простейшие тактики
для доказательства эквивалентности.
Динамическое представление типов на основе эквивалентности. Тестирование эквивалентности при работе программы, приведение эквивалентных типов.
Сумма и произведения типов. Конструктор неподвижной точки. Катаморфизмы, проблемы реализации.