Практика 3. Типы в λ-исчислении

Анализ типов

• Попытаемся приписать каждой ноде программы синтаксические метки по определённым правилам
• Если метки таким образом приписать можно — программа «хорошая»
• Вид таких меток и правил задаётся системой типов
• Анализ типов — разновидность статического анализа: программу проверяем, не запуская

Наш язык на сегодня: \lambda_\to и константы

Типизация интуитивно: конкретные типы

Типизация интуитивно: буквы

Типизация интуитивно: функции-аргументы

Типизация самоприменения

Население типов интуитивно

Буквы и константы

Контекст типизации

• В программах используются введённые ранее имена
• Для типизации нужно знать типы сущностей, связанных ранее с этими именами
• Будем поддерживать доп. структуру данных, которую будем заполнять именами с соответствующими им типами в процессе обхода дерева программы

Пример на Си

int dostrange(int a, char i) {
    // point 0
    int c = 5;
    for (int i = 0; i < 15; ++i) {
        i -= 1; // point 1
        long r = i;
        i *= r; // point 2
    }
    return a + (int)i * c; // point 3
}

Контекст типизации: пример на лямбда-исчислении

В чистом лямбда-исчислении имена вводятся с помощью абстракции: \lambda f^A\,g^B\,x^C.\,f\ (g\ x) по Чёрчу.

Правила типизации \lambda_\to

Правила для констант + наше расширение

Константы — тоже вершины дерева, и у каждого вида своё правило: литералы и \mathtt{true}/\mathtt{false} — листья, операторы и \mathtt{if} — вершины с поддеревьями.

• Правила для \mathtt{-}, \mathtt{*} — как (\mathtt{+}); для \mathtt{==} — как (\mathtt{<})

Дерево вывода с дырками

Дерево вывода с нуля

Верно ли утверждение?

Простые примеры задач населения

Сколько обитателей у типа?

Рекурсия возвращается: fix факультативно

• \mathbf{Y} := \lambda f.\,(\lambda x.\,f\ (x\ x))\ (\lambda x.\,f\ (x\ x)) содержит x\ x — в \lambda_\to у него нет типа, как и у любого другого комбинатора неподвижной точки: все программы \lambda_\to завершаются
• Значит, рекурсию встраиваем в язык так же, как числа и були: новая форма терма \mathtt{fix}\ M, от которой нужно ровно свойство \mathbf{Y} из П2 — \mathtt{fix}\ M =_\beta M\ (\mathtt{fix}\ M)

Факториал в расширенном языке факультативно

\mathbf{fac} := \mathtt{fix}\ F, \qquad F \equiv \lambda f\,n.\,\mathtt{if}\ (n \mathrel{\mathtt{==}} \mathtt{0})\ \mathtt{1}\ (n \mathrel{\mathtt{*}} f\ (n \mathrel{\mathtt{-}} \mathtt{1}))

• Как в П2: рекурсивный вызов абстрагирован по имени f — только вместо \mathbf{Y} стоит \mathtt{fix}, а вместо кодировок — константы

Дерево типизации факториала факультативно

F \equiv \lambda f\,n.\,\mathtt{if}\ (n \mathrel{\mathtt{==}} \mathtt{0})\ \mathtt{1}\ (n \mathrel{\mathtt{*}} f\ (n \mathrel{\mathtt{-}} \mathtt{1})), \quad \Gamma \equiv f^{\mathrm{Int}\to\mathrm{Int}},\ n^{\mathrm{Int}}

Сегодня мы многое поняли

• Анализ типов — по правилам расставляем метки — просто!
• Научили мозг проверке типов — отличать хорошие программы от плохих
• Объяснить по всей строгости, почему программа типизируется или нет

Таинственные связи ☁

Дерево вывода типа комбинатора \mathbf{B} для произвольных типов A, B, C — или вывод силлогизма в исчислении высказываний?

\dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{}{\Gamma \vdash {\color{blue}f :}\ B\to C}\ {\scriptstyle (\text{акс})} \qquad \dfrac{ \dfrac{}{\Gamma \vdash {\color{blue}g :}\ A\to B}\ {\scriptstyle (\text{акс})} \quad \dfrac{}{\Gamma \vdash {\color{blue}x :}\ A}\ {\scriptstyle (\text{акс})} }{\Gamma \vdash {\color{blue}g\ x :}\ B}\ {\scriptstyle (\to E)} }{{\color{blue}f}^{B\to C},\ {\color{blue}g}^{A\to B},\ {\color{blue}x}^{A} \vdash {\color{blue}f\ (g\ x) :}\ C}\ {\scriptstyle (\to E)} }{{\color{blue}f}^{B\to C},\ {\color{blue}g}^{A\to B} \vdash {\color{blue}\lambda x.\,f\ (g\ x) :}\ A\to C}\ {\scriptstyle (\to I)} }{{\color{blue}f}^{B\to C} \vdash {\color{blue}\lambda g\,x.\,f\ (g\ x) :}\ (A\to B)\to A\to C}\ {\scriptstyle (\to I)} }{\vdash {\color{blue}\lambda f\,g\,x.\,f\ (g\ x) :}\ (B\to C)\to(A\to B)\to A\to C}\ {\scriptstyle (\to I)}

Таинственные связи ☁

Дерево вывода типа комбинатора \mathbf{B} для произвольных типов A, B, C — или вывод силлогизма в исчислении высказываний?

\dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{}{\Gamma \vdash \phantom{f :}\ B\to C}\ {\scriptstyle (\text{акс})} \qquad \dfrac{ \dfrac{}{\Gamma \vdash \phantom{g :}\ A\to B}\ {\scriptstyle (\text{акс})} \quad \dfrac{}{\Gamma \vdash \phantom{x :}\ A}\ {\scriptstyle (\text{акс})} }{\Gamma \vdash \phantom{g\ x :}\ B}\ {\scriptstyle (\to E)} }{{\phantom{f}}^{B\to C},\ {\phantom{g}}^{A\to B},\ {\phantom{x}}^{A} \vdash \phantom{f\ (g\ x) :}\ C}\ {\scriptstyle (\to E)} }{{\phantom{f}}^{B\to C},\ {\phantom{g}}^{A\to B} \vdash \phantom{\lambda x.\,f\ (g\ x) :}\ A\to C}\ {\scriptstyle (\to I)} }{{\phantom{f}}^{B\to C} \vdash \phantom{\lambda g\,x.\,f\ (g\ x) :}\ (A\to B)\to A\to C}\ {\scriptstyle (\to I)} }{\vdash \phantom{\lambda f\,g\,x.\,f\ (g\ x) :}\ (B\to C)\to(A\to B)\to A\to C}\ {\scriptstyle (\to I)}

Типизация в стиле Карри и в стиле Чёрча

Мотивация статического анализа программ

• Программное обеспечение — это сложно
• В программах случаются ошибки (постоянно и неизбежно)
• Поиск ошибок может занимать годы, десятилетия, вечность
• Нужны методы для того, чтобы судить о программах и их свойствах автоматически
• Программы могут работать долго
• Хотим отвергать «плохие» программы до исполнения (статически)

Роль типов в языках

• Позволяют выявлять некоторые классы ошибок:

  GHCi> length 42         -- Ошибка: на вход не список, а число
  GHCi> foldr (+) "ABCDE" -- Ошибка: плюс работает на числах, но не символах

• Механизм абстракции: интерфейс, скрывающий детали реализации

• Средство документирования: как использовать сущность

• Частичная спецификация поведения

• Позволяют генерировать более эффективный низкоуровневый код

Ограниченность систем типов ☁

• Хотелось бы, чтобы все «хорошие» программы типизировались, а все «плохие» — нет
• Однако по теореме Успенского-Райса задача проверки любого нетривиального¹ свойства программы неразрешима

В чем подвох с системами типов?

• Всё, что типизируется, — «хорошее», но обратное не всегда верно
• ⇒ Всегда существуют «хорошие» программы, которые не типизируются²

Деревья вывода

• Теория доказательств математической логики — доказываем принадлежность утверждения типизации множеству истинных утверждений
• Истинное утверждение в теории доказательств — то, которое можно синтаксически вывести по правилам вывода из аксиом
• Деревья вывода — синтаксические, машинно-проверяемые конструкции
• Деревья сами по себе не несут смысла, наличие корректного дерева говорит только о возможности его построения
• Чтобы деревья имели смысл, для каждой теории доказываются утверждения вида:
  • Если существует дерево вывода с корнем X, то верно Y
  • e.g. Если существует \lambda_\to дерево с утверждением про терм M в корне (терм M в таком-то контексте имеет такой-то тип), то этот терм строго нормализуем
• Иногда по правилам вывода очевиден алгоритм построения дерева
  • В нашем случае (для \lambda_\to) это так
  • В общем случае — нет (математики оказались бы не нужны)

Не всё сильно-нормализуемое типизируется ✱

Вспомним: всё, что типизируется, «хорошее», но обратное не всегда верно. Будем «хорошим» считать сильную нормализуемость.

\mathbf{2}\ \mathbf{K} терм сильно нормализуем и редуцируется так:

\mathbf{2}\ \mathbf{K} = \lambda z.\,\mathbf{K}\ (\mathbf{K}\ z) = \lambda z\,a\,b.\,z

Однако протипизировать это не получится.

• Наиболее общий тип \mathbf{K} — это \gamma \to \tau \to \gamma
• \mathbf{2} := \lambda s\,z.\,s\ (s\ z), наиболее общий тип \mathbf{2} — это (\alpha \to \alpha) \to \alpha \to \alpha
• По правилу типизации аппликации, применение \mathbf{2} к \mathbf{K} накладывает на \gamma, \tau, \alpha ограничения \alpha = \gamma,\ \alpha = \tau \to \gamma

Противоречие.

Эквивалентности не сохраняют тип ✱

\beta-эквивалентность не сохраняет тип

Из лекции известно, что если M редуцируется к N и \Gamma \vdash M : \tau, то \Gamma \vdash N : \tau.

Неправда, что если M редуцируется к N и \Gamma \vdash N : \tau, то \Gamma \vdash M : \tau.

Пример: N = \lambda x.\,x, N : \alpha \to \alpha; M = \lambda x.\,(\lambda y.\,x)\ (x\ \mathbf{I}), и за одно редуцирование M переходит в N, но M : \alpha \to \alpha не выполняется: тогда бы подтерм x\ \mathbf{I} не типизировался, так как \alpha не является стрелочным типом.

\eta-эквивалентность не сохраняет тип

Если \lambda x.\,M\ x : \tau (где x не является свободным в M), то M : \tau.

Если M : \tau, то не обязательно \lambda x.\,M\ x : \tau.

Пример: \mathbf{I} : \alpha \to \alpha, но \lambda x\,y.\,x\ y : (\beta \to \gamma) \to (\beta \to \gamma) нельзя приписать тип \alpha \to \alpha: тогда бы подтерм x\ y не типизировался, так как \alpha не является стрелочным типом.

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

• Формальная верификация операционных систем

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

• Соответствие Карри–Говарда: от матлогики к программированию
• Вывод типов от Хиндли-Милнера до GHC 8.8
• Программирование с зависимыми типами на языке Idris
• Edwin Brady «Type-Driven Development with Idris»
• Pierce, Benjamin C. Types and programming languages. MIT press, 2002.
• Пирс Б. Типы в языках программирования. — Лямбда пресс, Добросвет, 2012. — 656 c.
• Sandy Maguire «Thinking with Types. Type-Level Programming in Haskell»
• Henk Barendregt, Wil Dekkers, and Richard Statman. «Lambda Calculus with Types». Cambridge University Press, New York, NY, USA, 2013.
• Dunfield, Jana, and Neel Krishnaswami. «Bidirectional typing.» ACM Computing Surveys (CSUR) 54.5 (2021): 1-38.