Определение функционального программирования. Связь с императивным программированием. Связь с другими моделями вычислений, тезис Черча-Тюринга.
Строгие нестрогие и спекулятивные вычисления. Динамическая и статическая типизация. Практическое применение функционального программирования.
Нетипизированное лямбда-исчисление.
Примитивно типизированное лямбда-исчисление. Рекурсивные типы. Интуиционисская логика. Проверка типов.
Изоморфизм Карри-Говарда.
Параметрический полиморфизм. Вывод типов.
Категории. Категория множеств, Порядок. Свободный моноид. Связь категорий и графов. Изоморфизм категорий. Коммутативные диаграммы.
Произведения и суммы объектов категорий.
Категория Circ.
Категория Flow.
Дистрибутивные категории. Связь с императивным программированием.
Типы данных как категории. Доказательство свойств.
Система автоматизации доказательств Coq. Функциональное программирование в Coq. Использование вывода типов для доказательства теорем в интуиционисской логике.
Использование ssreflect. Эквивалентность и переисывание. Булева рефлексия.
Использование ssreflect. Индуктивные доказательства. Кодирование структур.
Сравнение синтаксиса Java и Scala
Представление структур данных в Scala
Функциональный подход к обработке ошибок
Ленивые вычисления в Scala
Функциональный параллелизм
Тестирование свойств
Парсер как композиция частичных парсеров
Моноиды и монады
Аппликативные функторы
Локальные эффекты и изменяемое состояние.
Ввод/вывод. Потоковый ввод/вывод.
Обработка больших данных. Преимущества функционального программирования для масштабирования.
Использование Scala для обработки больших данных. Платформа SMACK (Spark, Mesos, Akka, Kasandra, Kafka).
Apache Spark
Akka
Apache Kafka
Интеграция компонент SMACK и связь с функциональным программированием.