Практика 1. Программирование в λ-исчислении

Зачем этот курс

• Мы возьмём простейший язык — \lambda-исчисление — и построим программирование заново
• ⇒ Вы научитесь описывать намерение так, чтобы его проверяла машина
• ⇒ Научитесь смотреть на каждый новый язык как на набор знакомых концепций
• ⇒ И перестанете считать языковые инструменты магией — потому что соберёте их сами
• NB Сегодня за час мы соберём из одних только функций: пары, логические значения и числа

Как устроена неделя

• Δ Лекция — новая тема
• Δ Практика
  • пишем летучку, она отрывается и сдаётся
  • мы разговариваем и решаем задачки, как и на зачётных сессиях
  • присутствуйте, используйте это время максимально, не откладывая на потом
  • ноутбуками не пользуемся
  • слайды и материалы будут — имеет смысл конспектировать только свои мысли
• Δ Домашка
  • выдаётся каждую неделю на неделю
  • базовое закрепление и подготовка к зачётным сессиям
  • рассчитана на решения “вручную”
  • если вы всё поняли, решается очень быстро, в действительности медленнее — это нормально
• Δ Ревью
  • после дедлайна бот рассылает решение случайно между одногруппниками
  • помощь другому — хороший способ научиться самому

Зачёт по практике

• Летучки - нужно сдать 12 из 14, правильность не учитывается
• Домашки - нужно сдать 12 из 14 на минимальный порог
• Очные сессии
  • нужно сдать 3
  • 20 минут решаем задачку маркером на доске и обсуждаем
• Старайтесь не терять темп, но будет достаточно возможностей дозакрыть долги
• Зачёт по практике необходим, чтобы получить допуск на экзамен
• Оценка за курс формируется на экзамене

Обозначения на слайдах

Что значит «задать язык»

• Δ Синтаксис — как записывать программы на этом языке
• Δ Семантика — как исполнять программы на этом языке

Формальный синтаксис термов

Дерево абстрактного синтаксиса (AST)

Запишем ту же редукцию строками

Подстановка

\begin{alignedat}{3} &[x \mapsto N]\ x &&\equiv N \\ &[x \mapsto N]\ y &&\equiv y \\ &[x \mapsto N]\ (P\ Q) &&\equiv ([x \mapsto N]\ P)\ ([x \mapsto N]\ Q) \\ &[x \mapsto N]\ \lambda x.\,P &&\equiv \lambda x.\,P \\ &[x \mapsto N]\ \lambda y.\,P &&\equiv \lambda y.\,[x \mapsto N]\ P &&\quad y \notin FV(N) \\ &[x \mapsto N]\ \lambda y.\,P &&\equiv \lambda y'.\,[x \mapsto N]\ ([y \mapsto y']\ P) &&\quad y \in FV(N) \end{alignedat}

Когда два терма — одно и то же

Записи, кортежи, пары

Одна сущность часто описывается несколькими свойствами: котик — это имя и мурлычность.

class Cat:
   def __init__(self, name, murlycity):
      self.name = name
      self.murlycity = murlycity

Чего мы хотим от такой структуры данных:

• Δ Конструктор создаёт новое значение: barsik = Cat("barsik", 4)
• Δ Элиминаторы достают информацию из значения: barsik.murlycity
• NB Мутаторы (barsik.murlycity += 3) не используем: вместо изменения — новое значение Cat(barsik.name, barsik.murlycity + 3)

Спецификация пары

Пары в \lambda-исчислении

• В \lambda-исчислении нет ничего, кроме функций. Где хранить два значения?

Проверка законов пар

\mathbf{pair} := \lambda x\,y.\,\lambda f.\,f\ x\ y \qquad \mathbf{fst} := \lambda p.\,p\ \mathbf{K} \qquad \mathbf{snd} := \lambda p.\,p\ \mathbf{K}_*

Спецификация логических величин

API логических величин — конструкторы-константы \mathbf{true} и \mathbf{false}, элиминатор \mathbf{if}

Логические величины в \lambda-исчислении

Операции над логическими величинами: отрицание

Натуральные числа \mathbb{N} := \{0, 1, 2, 3, \cdots\}

API натуральных чисел

• Первая аксиома Пеано: ноль является натуральным числом (\mathbf{0})
• Вторая аксиома Пеано: число, следующее за натуральным, тоже натуральное (\mathbf{suc}\ n)
• Элиминатор: воспользоваться натуральным числом — что-то сделать n раз, \mathbf{natElim}

Операции над числами Чёрча: чётность

Что вы теперь умеете

• Мы задали простейший язык программирования — описали синтаксис и семантику \lambda-исчисления
  • программы (термы) — деревья правильного вида
  • вычисление — переписывание деревьев
• Мы спроектировали первые структуры данных в \lambda-исчислении
  • начинали с API — набор конструкторов и элиминаторов
  • записывали законы, определяющие поведение конструкторов и элиминаторов
  • конструировали термы, удовлетворяющие законам

Каррирование

Эквивалентен ли код?

def k_star(x, y):
    return y

def k_star(x):
    def helper(y):
        return y
    return helper

• Δ Каррирование превращает функцию многих аргументов в набор вложенных функций, каждая из которых берёт часть аргументов. В ООП методы каррированы: часть «аргументов» приходит через конструктор

Замыкания и функции высших порядков

def k(x):
    def helper(y):
        return x      # x — из окружения
    return helper

auto screen = Screen::create(...);
clearButton.onClick([screen]() {
    screen.textField = "";
});

def compose(f, g):
    def helper(x):
        return f(g(x))
    return helper

Законы и algebra driven design

Закодировав пару, мы получили абстракцию по данным:

• Это уже не два значения, а доменная сущность
• Реализацию можно выбрать любую, лишь бы выполнялись законы, — и дальше забыть, как она устроена
• Её можно в любой момент подменить, например на более эффективную, и пользовательский код не сломается
• Соответствие законам можно проверять автоматически

Прочитать: Sandy Maguire, Algebra-Driven Design; посмотреть: John Hughes — How to specify it! (Lambda Days 2020).

Идея кодирования по Чёрчу

• Пусть функция не возвращает результат, а принимает способ его сразу обработать: «штуку я не дам, скажи, зачем она тебе, — я всё сделаю»
• Вместо того чтобы нести объект туда, где его разберут, мы приносим разбор туда, где объект создаётся: вместо (X) -> R получается (X, (R) -> a) -> a
• Так избавляются от аллокаций и промежуточных структур: десериализатор вместо std::variant<Msg1, Msg2> сразу вызывает Impl::processMsg1(...) или Impl::processMsg2(...)

Это известно как tagless final, кодирование Чёрча — Бёма — Берардуччи и CPS-преобразование; всё это ещё встретится в курсе.

Объектно-ориентированная запись пар по Чёрчу

На самом деле, приоритезировать элиминаторы - более характерно для ОО стиля.

interface Pair<A, B> {
    fun <R> fold(f: (A, B) -> R): R
}

fun <A, B> pair(x: A, y: B): Pair<A, B> = object : Pair<A, B> {
    override fun <R> fold(f: (A, B) -> R): R = f(x, y)
}

fun <A, B> fst(p: Pair<A, B>): A = p.fold { x, _ -> x }

fun <A, B> snd(p: Pair<A, B>): B = p.fold { _, y -> y }

object : Interface — это конструкция для определения анонимного класса-наследника. Аналогичным образом можно сделать через именованные классы.

Объектно-ориентированная запись логических величин

interface Bool {
    fun <R> myif(t: R, e: R): R
}

val tru = object : Bool {
    override fun <R> myif(t: R, e: R): R = t
}

val fls = object : Bool {
    override fun <R> myif(t: R, e: R): R = e
}

fun not(b: Bool): Bool = b.myif(fls, tru)

Объектно-ориентированная запись натуральных чисел

interface Nat {
    fun <T> elim(z: T, s: (T) -> T): T
}

val zero = object : Nat {
    override fun <T> elim(z: T, s: (T) -> T): T = z
}

fun suc(n: Nat): Nat = object : Nat {
    override fun <T> elim(z: T, s: (T) -> T): T =
        s(n.elim(z, s))
}

fun plus(n: Nat, m: Nat): Nat = n.elim(m, ::suc)

Что посмотреть в транспорте

• Функциональное программирование как предмет и метод теоретической информатики
• Podlodka #279 — Тьюринг-полнота | Виталий Брагилевский
• Roman Elizarov: Immutability we can afford
• Памятка с полезностями от Computer Science Center

Серьёзные материалы

• Записи лекций Дениса Николаевича на МКН
• Книга: Х. Барендрегт, «Ламбда-исчисление. Его синтаксис и семантика»
• Beyond Church encoding: Böhm–Berarducci isomorphism of algebraic data types and polymorphic lambda-terms