Функциональное программирование

Бакалавриат 2019/2020

Лучший по критерию «Новизна полученных знаний»

Статус: Курс по выбору (Прикладная математика и информатика)

Направление: 01.03.02. Прикладная математика и информатика

Кто читает: Департамент анализа данных и искусственного интеллекта

Где читается: Факультет компьютерных наук

Когда читается: 4-й курс, 3 модуль

Формат изучения: без онлайн-курса

Преподаватели: Кузнецов Степан Львович, Рогозин Даниил Дмитриевич

Язык: русский

Кредиты: 4

Контактные часы: 46

Полная версия программы учебной дисциплины

Аннотация

Настоящая дисциплина относится к профессиональному циклу, дисциплинам базовой части профиля. Для специализации «Распределенные системы» настоящая дисциплина является базовой. Изучение данной дисциплины базируется на знании курса “Сложность вычислений и логика в теоретической информатике”.

Цель освоения дисциплины

Освоение теоретической базы функционального программирования (начала теории типов, лямбда-исчисление, начала теории категорий).
Овладение техникой программирования на языке Haskell.

Планируемые результаты обучения

Студент знает теоретические основы функционального программирования (лямбда-исчисление, начала теории категорий и проч.).
Студент владеет общей информацией об императивном и функциональном стилях программирования, их сильных и слабых сторонах, умеет выбирать правильный стиль в зависимости от задачи.
Студент решает задачи на программирование на языке Haskell.
Студент разрабатывает новые библиотеки на языке Haskell.
Студент создает код на функциональном языке, корректность которого формально доказана (верифицирована).

Содержание учебной дисциплины

Типизованное лямбда-исчисление
Это теоретический вводный раздел курса. В нём на лекции излагаются основные понятия лямбда-исчисления, понятия, теории типов и их применения в программировании. На семинаре обсуждаются задачи на типизацию и преобразования лямбда-термов.
Нормализуемость и конфлюэнтность
На лекции даются формулировки основных свойств лямбда-исчисления (точнее, отношений бета- и ита-редукций): свойства сильной и слабой нормализуемости и свойство Чёрча - Россера (конфлюэнтности). Доказательства этих свойств выходят за рамки курса. На семинаре обсуждаются примеры нормализации лямбда-термов, а также нарушения нормализуемости (как слабой, так и сильной, при сохранении слабой) в нетипизируемом случае.
Императивное и функциональное программирование. Элементы функционального программирования в императивных языках
На лекции даётся сравнение двух парадигм программирования - императивной и функциональной. Практическое занятие и домашняя работа посвящены реализации некоторых мотивов функциональной парадигмы во в целом императивном языке Python.
Язык и среда разработки Haskell: установка и настройка
Практическое занятие: демонстрация работы с интерпретатором Haskell (GHC или иным).
Основы программирования на языке Haskell
Практическое занятие: простейшие программы на Haskell.
Типы данных в Haskell
Даётся обзор стандартных типов данных в Haskell. Обсуждаются возможности индуктивного построения новых типов (на примере натуральных чисел по Пеано). Обсуждается алгоритм Хиндли-Дамаса-Милнера для выведения типов (type inference).
"Ленивые" и "ретивые" вычисления
На лекции обсуждается различие между "ленивыми" вычислениями (когда значение подтерма вычисляется только по необходимости) и "ретивыми" вычислениями (когда рекурсивно вычисляется всё). На практическом занятии даются примеры, когда "ленивые" вычисления справляются с ситуациями, где "ретивые" входят в бесконечный цикл.
Монады и их использование для ввода-вывода
На лекции рассказывается введение в теорию категорий и даётся понятие монады. На практическом занятии обсуждается применение монад для реализации функций с состояниями и побочных эффектов.
Соответствие Карри - Говарда. Верификация программ и математических утверждений. Система Coq
Необязательная часть курса. Рассказывается о соответствии Карри - Говарда между типами и высказываниями и термам и доказательствами высказываний. В практической части демонстируются возможности формального доказательства математических теорем, в том числе о правильности работы программ (верификация).

Элементы контроля

Домашние задания
Программистские домашние задания (4-6 заданий в течение модуля). Домашние задания могут раздаваться и приниматься по электронной почте, посредством системы Github или каким-либо иным удобным для преподавателя и студентов способом. В ходе текущего контроля (домашние задания) студент должен продемонстрировать владение техниками программирования, обсуждёнными к настоящему моменту.
Контрольная работа
Контрольная работа (60 мин) в середине курса.
Экзамен
Письменный экзамен (90 мин). На итоговом экзамене студент должен показать владение теоретическими основами функционального программирования, посредством решения задач. Экзамен уже состоялся в 3 модуле.

Промежуточная аттестация

Промежуточная аттестация (3 модуль)
Итоговая оценка формируется следующим образом: 0,7*(накоп.) + 0,3*(экзамен), где (экзамен) - оценка за итоговый экзамен, а (накоп.) - накопленная оценка за семестр, определяемая следующим образом: (накоп.) = 0,72*(прог.) + 0,28*(контр.), где (прог.) - суммарная оценка за программистские домашние задания, (сам.) - оценка за контрольную работу.

Программа дисциплины