Лекция 1. Введение и воспоминания о ФП

• О курсе: зачем он, как устроен и что в нём будет, глава за главой
• Вспоминаем ФП: глава 1 конспекта по разделам, с задачами
  • термы и редукция · типы · функции, данные, классы типов и монады в Haskell

• Многие сложные вещи в дизайне языков и программ — частные случаи нескольких простых принципов
• Эти принципы считаются «общеизвестным фольклором», поэтому их не объясняют

• − Знание рассеяно по книгам, статьям и культовым блог-постам; собрать картину самому — долго

• ⇒ Цель курса — собрать фольклор в одном месте и организовать в систему
• ⇒ Курс явно опирается на классические работы; чтение статей — часть работы в курсе

• Δ ФП — трепетное отношение к понятию эффекта
  • в других школах мысли эффект — аксиоматическая данность
  • в ФП — предмет изучения, сознательного конструирования и аккуратного обращения

• ⇒ Это полезно для изучения языков и построения выразительных конструкций
• ⇒ И это основа продуктивного стиля программирования

• i Функциональные языки сравнительно просты, поэтому новые идеи часто рождаются в них и расходятся дальше
• Haskell как язык курса: воплощает многие концепции, доведённые до логического завершения, достаточно выразителен, чтобы кодировать остальные, и при этом промышленный

• NB Пререквизиты: АТД, паттерн-матчинг, свёртки, параметрический полиморфизм, классы типов, базовые монады
• + Полезно: читать типовые дроби, полиморфное \lambda-исчисление, кодирование Чёрча

• Занятие раз в неделю: два часа с перерывом, лекция и практика вперемешку
• Конспект — источник истины; слайды и записи — производные. Главу читать до или сразу после занятия

• Домашка каждую неделю
  • маленький обязательный минимум — допуск к экзамену (все минимумы сданы, не больше двух пропусков)
  • остальные задачи — уровень «к экзамену» и «челлендж», по желанию
  • проверка автоматическая: тесты и линтер в CI, ревью от LLM — совещательное

• Оценка за курс = экзамен: вопрос по конспекту и must-read главы плюс задача из домашек уровня «к экзамену»
• Банк вопросов по главам публикуется с первой недели — это и программа экзамена, и вопросы для повторения

• Какие формы принимает полиморфизм в языках и как он реализуется: мономорфизация, словари, боксинг
• System F, ранги, кодирование данных полиморфными функциями
• Тизер: структуры данных на уровне типов и «полиморфизм по полиморфизму» — по конвенции вызова

• ⇒ Полиморфизм — код, который ничего не знает о типе; на этом стоит модульность интерпретаторов

• Как устроены классы типов: словари, резолв инстансов как логическое программирование
• Семейства типов — функции на типах
• Тизер: 100500 применений классов типов, и многое окажется их частным случаем: рефлексия, Typeable, Generic, зависимость от значения через тип

• ⇒ Классы типов — механизм расширяемости; выстрелит в tagless final и в системах эффектов

• Алгебра типов и изоморфизмы: ищем дизайн данных алгебраически
• Вариантность и при чём тут функторы
• Рекурсивные типы через неподвижную точку; свёртки и развёртки как универсальные схемы
• Тизер: всё через свёртки? всё через развёртки? как ФП связано с ООП?

• ⇒ Здесь впервые появляется expression problem — главная проблема курса

• Научимся видеть интерпретаторы повсюду: башня интерпретаторов, встроенные языки
• Типы во встроенных языках, связывания и функции: интерпретируем самих себя самими собой
• Tagless final — интерпретатор без синтаксического дерева
• Тизер: почему написание функции — это расширение языка? монада — это интерпретатор чего, простите?

• ⇒ Expression problem формулируется точно: добавить и конструкцию, и интерпретацию, не трогая старое

• Как понять продолжения: «остаток вычисления» как значение
• CPS и стейт-машины; Cont — one monad to rule them all
• Дефункционализация продолжений — и мы получаем абстрактную машину
• Ограниченные продолжения, генераторы, корутины
• Тизер: callCC, shift/reset, и почему исключения, async и yield — одно и то же

• ⇒ Продолжения — материал, из которого сделаны хендлеры эффектов

• Алгебраические эффекты: операция отдельно, интерпретация отдельно
• Free-монады, data types à la carte, трансформеры монад — три способа собрать интерпретатор из кусков
• Тизер: любой язык программирования выражается через одну конструкцию?

• ⇒ Это ответ на expression problem: модульные интерпретаторы

• Как типизировать эффекты: строки эффектов, хендлеры в типах
• Koka и Effekt как языки; effectful, polysemy, bluefin как библиотеки
• Тизер: типизированные ошибки без боли — это возможно? Наверное

fun divide(a : int, b : int) : exn int

• ⇒ То, чем сегодня живёт промышленный Haskell, и куда движутся другие языки

• В ФП программа — выражение; выполнение — редукция выражения к более простому
• Выражение можно записать строкой, а можно деревом: дереву не нужны скобки и приоритеты

• Δ Простейший функциональный язык — \lambda-исчисление; его выражения — \lambda-термы из вершин трёх видов

\Lambda ::= V \ \mid\ (\lambda V.\,\Lambda) \ \mid\ (\Lambda\ \Lambda)

• Δ β-редукция — единственное правило переписывания: найти применение \lambda-функции к аргументу и подставить аргумент вместо связанной переменной

(\lambda x.\,M)\ N \ \rightsquigarrow_\beta\ [x \mapsto N]\ M

• Программное обеспечение — это сложно, поэтому ошибки в программах неизбежны
• Их можно искать статически, не запуская программу; анализ типов — один из видов статического анализа

• Δ Идея: каждой вершине дерева программы приписываем синтаксическую метку по правилам
• Если удалось приписать метку каждой вершине — программа проходит проверку типов и считается «хорошей»

• Δ Система типов задаёт синтаксис меток и правила, по которым их можно приписывать
• Синтаксис — в нотации вроде BNF; правила — типовые дроби: над чертой посылки, под чертой вывод
• Просто типизированное \lambda-исчисление \lambda_\to:

\dfrac{(x : \sigma) \in \Gamma}{\Gamma \vdash x : \sigma}\ {\scriptstyle ctx} \qquad \dfrac{\{x : \sigma\} \cup \Gamma \vdash M : \tau}{\Gamma \vdash \lambda x^{\color{red}\sigma}.\,M : \sigma \to \tau}\ {\scriptstyle intro\!\to} \qquad \dfrac{\Gamma \vdash M : \sigma \to \tau \quad \Gamma \vdash N : \sigma}{\Gamma \vdash M\ N : \tau}\ {\scriptstyle elim\!\to}

• i Метки чисто синтаксические, но их можно интерпретировать: самая популярная интерпретация — тип как множество, int \to int как множество функций \mathbb{Z} \to \mathbb{Z}

Дерево вывода — перевёрнутое дерево терма: каждой вершине по одному правилу.

• Плюс примитивные типы, объявления имён, структуры данных и классы типов

ghci> (\x -> x + 1) 4
5
ghci> :t \x -> x + 1

• Функциям дают имена; сигнатуры на верхнем уровне пишут явно

f :: Int -> Int
f x = x + 1

• Δ Имя типа с маленькой буквы — типовая переменная: параметрический полиморфизм. id ничего не знает про аргумент, но результат обязан быть того же типа

id :: a -> a
id x = x

• Δ Функции принимают функции — функции высших порядков
• Имя из специальных символов — оператор, применяется инфиксно

($) :: (a -> b) -> a -> b
f $ x = f x

• Рекурсия с охранными выражениями для базового случая

factorial :: Int -> Int
factorial n
  | n < 1 = 1
  | otherwise = n * factorial (n - 1)

• Δ Cat и Dog — конструкторы данных: функции, реализованные языком; выделяют память и позиционно размещают компоненты

Cat :: String -> Int -> Animal
Dog :: String -> Animal

• Чтобы воспользоваться данными, значение деконструируют паттерн-матчингом: образец выбирается, если похож на то, как значение сконструировано, и его переменные начинают ссылаться на компоненты

describeAnimal :: Animal -> String
describeAnimal animal = case animal of
  Cat name nLifes -> "This is cat " ++ name ++ " " ++ show nLifes
  Dog name -> "This is dog " ++ name

• Записи с именованными полями порождают функции-аксессоры: getName :: Penguin -> String

data Penguin = Penguin { getName :: String, getAge :: Int }

• Функции часто частичны: не для всех аргументов есть результат. Смоделируем это типом данных

data MaybeD = NothingD | JustD Double
safeSqrtD :: Double -> MaybeD
safeSqrtD x = if x < 0 then NothingD else JustD (sqrt x)

• − Так придётся объявлять свой MaybeT для каждого T
• ⇒ Haskell позволяет абстрагироваться в типе, как \lambda абстрагируется по значению в терме

data Maybe a = Nothing | Just a
safeSqrt :: Double -> Maybe Double
safeSqrt x = if x < 0 then Nothing else Just (sqrt x)

• Δ Maybe — не тип, а типовый конструктор: ему нужно передать типовой параметр, чтобы получить тип

• А что если дать типовому конструктору меньше параметров, чем он ждёт? Или больше?
• Δ Система кайндов контролирует корректность типовых аппликаций: простейшие «типы для типов»
• Обычные типы имеют кайнд *, типовые конструкторы — стрелочные кайнды; аппликация убирает одну стрелку

• Синонимы типов — просто другое имя для типа, если запись оригинала слишком длинная

type T a = VeryLongType Int (a -> AnotherLongType a)

• newtype — тип с одним конструктором и одним полем: не нужно выделять память под тег и ссылки на поля, значение обёртки — значение оборачиваемого типа, а сама обёртка существует только во время компиляции

newtype CourseId = CourseId Int64
newtype ModuleId = ModuleId Int64

• Δ Параметрический полиморфизм — один код для разных типов; классы типов — один идентификатор для разных реализаций, как перегрузка: механизм специального (ad-hoc) полиморфизма

class Eq a where
  (==) :: a -> a -> Bool

• Реализация выбирается по типу аргументов в месте вызова

ghci> CourseId 1 == CourseId 2
False
ghci> [CourseId 1, CourseId 2] == [CourseId 1, CourseId 2]
True

• Параметрически-полиморфная функция ничего не может делать с аргументом, кроме как вернуть его или передать дальше
• Чтобы делать что-то ещё, нужна дополнительная информация о типе: suc n = n + 1 не работает для строк, поэтому тип suc :: a -> a некорректен

• ⇒ Классы типов — способ ограничить полиморфизм: не любой тип, а любой, для которого есть нужные операции

suc :: Num a => a -> a
suc n = n + 1

• Δ Functor объявляется для конструкторов типов и заменяет все элементы контейнера, не меняя его структуру

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b

• В Haskell функция просто вычисляет результат. Но часто нужно и «что-то ещё»: изменить состояние, написать в консоль — побочные эффекты
• Вернуть можно только результат, поэтому эффекты кодируем как дополнительную структуру, оборачивающую чистый результат: вместо a функция возвращает тип вычислений f a

• Стандартная библиотека даёт классы типов для значений вида f a: они позволяют работать с a внутри, как будто структуры f нет

• Applicative позволяет писать выражения над вычислениями f a

class Functor f => Applicative (f :: * -> *) where
  pure :: a -> f a
  liftA2 :: (a -> b -> c) -> f a -> f b -> f c
instance Applicative Maybe where
  pure = Just
  liftA2 _ Nothing _ = Nothing
  liftA2 _ _ Nothing = Nothing
  liftA2 f (Just x) (Just y) = Just (f x y)

• Monad позволяет последовательно компоновать вычисления в императивном стиле

class Applicative m => Monad (m :: * -> *) where
  (>>=) :: m a -> (a -> m b) -> m b
newtype State s a = State { runState :: s -> (s, a) }

• Для таких цепочек есть do-нотация: тот же example строчка в строчку

example = do
  x <- get
  put 42
  y <- get
  pure (x + y)

• Домашка fp2-01: интерпретатор Lalalang — изучить выданный код, добавить операции, S-выражения, паттерн-матчинг. Минимум — задачи 1.1–1.2
• На следующем занятии: параметрический полиморфизм — глава 2