Идиомы функционального программирования

Санкт-Петербург, осень 2015

Описание

Данный курс правильно было бы назвать «некоторые приёмы функционального программирования на статически типизированных языках». Так или иначе эти приемы основаны на использовании полиморфизма и функций высшего порядка и часто позволяют выразить то, что в других языках реализовывается ad hoc.

В качестве основного языка будет использован Haskell, хотя в большинстве случаев рассматриваемые приёмы могут быть перенесены в другие строго типизированные языки (например, Objective Caml).

Примерный (и неполный) перечень тем, которые предполагается затронуть:

  • Функции с переменным числом аргументов («variadic functions»).
  • Однородная обработка кортежей.
  • Вычисления на уровне типов («type-level computations»).
  • Расширяемые типы данных («expression problem»).

Некоторая литература:

  1. Olivier Danvy. Functional Unparsing // J. Funct. Program., 1998, Vol. 8, №6, P. 621—625.
  2. Oleg Kiselyov. Polyvariadic functions and keyword arguments: pattern-matching on the type of the context.
  3. Daniel Fridlender, Mia Indrika. Do We Need Dependent Types? // J. Funct. Program., 2001, Vol. 10, P. 409—415.
  4. Oleg Kiselyov, Ralf Lammel, Keean Schupke. Strongly Typed Heterogeneous Collections // Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, 2004, P. 96—107.
  5. Arthur I.Baars, S.Doaitse Swierstra. Typing Dynamic Typing // Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming, 2002, P. 157--166.
  6. 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; Экзистенциальные типы.

Проблема overlapping instances. Причины возникновения, интерпретация. Обобщение головы, использование эквивалентности типов.

Экзистенциальные типы, абстракция относительно схемы свойств.

Эквивалентность типов

Эквивалентность по Лейбницу. Представление лейбницевской эквивалентности типов в терминах Haskell. Простейшие тактики для доказательства эквивалентности.

Динамическое представление типов

Динамическое представление типов на основе эквивалентности. Тестирование эквивалентности при работе программы, приведение эквивалентных типов.

Рекурсивные типы и обобщенные катаморфизмы.

Сумма и произведения типов. Конструктор неподвижной точки. Катаморфизмы, проблемы реализации.