Лекция 4.
Типы
Введение в Функциональное программирование
Джон Харрисон
Университет Кембриджа
10 сентября 2008 г.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Темы
Зачем нужны типы? Ответы из программирования и логики
Простое типизированное λ-исчисление
Полиморфизм
Let-полиморфизм
Наиболее общие типы и алгоритм Милнера
Сильная нормализация; рекурсия.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Логическое обоснование типов
Так что же всё-таки «термы» означают в λ-исчислении? Какой
смысл в применении функции к самой себе, как в f f ?
Некоторый смысл есть для таких функций, как тождество λx. x или
константная функция λx. y . Но, в основном, это выглядит
подозрительно.
Возможно, именно поэтому попытка расширить систему, чтобы
включить теорию множеств, натыкается на парадокс Рассела.
Вот поэтому Чёрч и разработал типизированное λ-исчисление,
которое и по сей день успешно используется в роли основания для
математики.
В настоящее время теория типов рассматривается как альтернатива
теории множеств в роли основания математики. Есть интересные
связи между теорией типов и программированием (Мартин-Лёф и
другие).
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Обоснование типов в программировании
Типы были введены в программирование по ряду причин. Мы
можем (по крайней мере ретроспективно) выделить следующие
преимущества:
Они помогают компьютеру генерировать более эффективный
код и рациональнее использовать память.
Они служат в роли некоторого «общего контроля» программ,
обнаруживая множество программистских ошибок ещё до
исполнения программы.
Они служат как документация для людей.
Они могут помочь в сокрытии данных и в улучшении
модульности программ.
В то же время некоторые программисты считают их раздражающим
ограничением. Как нам достичь оптимального баланса?
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Различные способы типизации
Мы можем различать:
Сильную типизацию, как в Modula-3, где типы должны
полностью совпадать.
Слабую типизацию, как в C, где допускается бо́льшая свобода
(например, аргумент типа int в функции ожидающей тип
float).
а также
Статическую типизацию, как в FORTRAN, которая
осуществляется в момент компиляции.
Динамическую типизацию, как в LISP, которая осуществляется
в момент исполнения.
ML статически и сильно типизирован. В то же время возможность
полиморфизма даёт много преимуществ слабой и динамической
типизации.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Совокупность типов
Допустим, что у нас есть некий набор Ptys константных типов,
например int и bool, и мы можем создавать из них новые типы,
используя конструктор функциональных типов, например
int → int
и
(int → bool) → int → bool
Оговорим, что функциональная стрелка обычно ассоциативна
справа.
Формально это ещё одно индуктивное определение.
В дальнейшем мы введём другие конструкторы типов, такие как
конструктор декартова произведения типов α × β, а также типовые
переменные, участвующие в полиморфизме. Обычно мы используем
α и β для типовых переменных.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Идея типизированного λ-исчисления
Тут мы просто каждому λ-терму задаём тип и осуществляем
сильную типизацию.
Мы можем составить применение s t только, если типы совпадают,
то есть s имеет функциональный тип σ → τ , а t имеет тип σ. В этом
случае комбинация s t имеет тип τ .
Мы используем запись t : σ, которая означает «t имеет тип σ».
Мы думаем о типах, как о множествах, в которых объекты
обозначаются термами, и t : σ читается как t ∈ σ. Такая
математическая запись обычно используется в случае
функциональных пространств.
Однако, как обычно, это только эвристическое руководство, и мы
ещё разработаем простое типизированное λ-исчисление как
формальную систему.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Типизация по Чёрчу
Это способ создания типов как структурной части термов. Это
система явных типов.
Каждая константа c : σc связана с определённым типом.
Переменная может иметь любой тип; переменные с
одинаковыми именами, но разными типами являются
различными термами.
Если s : σ → τ и t : σ – термы, то s t : τ тоже терм.
Если v : σ – переменная, а t : τ – терм, то λx. t : σ → τ – терм.
Однако предпочительнее использовать неявную типизацию. По сути,
в ML никогда не надо указывать тип!
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Типизация по Карри
Здесь термы такие же, как и были раньше; кроме того, есть
отдельное понятие типизации. Всё типизируется неявно, и у терма
может быть много типов. Мы используем контекст Γ, который задаёт
назначение типов для переменных и констант:
Γ`t:σ
это означает, что «при условии назначения типов из набора Γ, t
имеет тип σ».
В случае, когда контекст пустой, мы будем писать t : σ.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Формальные правила типизации
Отношение к типам задаётся следующим образом:
v :σ∈Γ
Γ`v :σ
c :σ∈Γ
Γ`c :σ
Γ`s:σ→τ Γ`t:σ
Γ`st:τ
Γ ∪ {v : σ} ` t : τ
Γ ` λv . t : σ → τ
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Пример
Посмотрим, как присвоить тип функции тождества λx. x. Согласно
первому правилу имеем:
{x : σ} ` x : σ
поэтому, согласно последнему правилу, мы получим, как и ожидали:
∅ ` λx. x : σ → σ
По соглашению, мы пишем просто λx. x : σ → σ.
Заметим, что контекст сыграл ключевую роль для «связи» разных
вхождений одной и той же переменной. В типизации по Чёрчу это
бы не понадобилось, ибо каждая переменная несёт в себе тип.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Сохранение типа
Правила преобразования ровно такие же, какие были в
нетипизируемом случае.
Очень важное свойство – это сохранение типа. Оно означает, что
преобразования из нетипизируемого λ-исчисления сохраняют
свойства типизируемости.
Например, если Γ ` t : σ и t −→ t 0 , то также Γ ` t 0 : σ.
β
Похожие свойства поддерживаются и другими преобразованиями, и
согласно структурной индукции мы видим, что если Γ ` t : σ и
t −→ t 0 , то также Γ ` t 0 : σ.
Это означает, что статическая типизация и динамическое
исполнение не мешают друг другу.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Добавление новых типов
Описанная выше система продолжает работать, если мы добавим
примитивных типов и конструкторов типов.
Например, введём новый бинарный конструктор типов × для
произведения типов.
Мы также введём инфиксный оператор составления пары «,»,
который имеет тип σ → τ → σ × τ . Таким образом:
(x : σ), (y : τ ) : σ × τ
Мы также можем ввести константы: fst : σ × τ → σ и snd : σ × τ → τ .
В общем случае у нас может быть сколь угодно много конструкторов
типов и любое количество констант, типы которых содержат эти
конструкторы. Как мы увидим, ML позволяет нам создавать свои
собственные конструкторы типов.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Полиморфизм
Типизация по Карри уже даёт нам форму полиморфизма. В том
смысле, что данный терм может иметь разные типы. Мы различаем:
Истинный («параметрический») полиморфизм, в котором все
типы несут в себе структурную взаимосвязь.
Специальный полиморфизм или перегрузка операций, в котором
различные типы, которые может иметь терм, различны.
Например, использование + для различных систем счисления.
У нас истинный, параметрический полиморфизм. Например,
функция тождества может иметь типы: σ → σ, τ → τ , или
(σ → τ ) → (σ → τ ).
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Let-полиморфизм (1)
У нашей системы есть печальное ограничение. В одном и том же
терме мы можем использовать одинаковые выражения разных
типов, например:
if (λx. x) true then (λx. x) 1 else 0
Однако, если мы применим локальную привязку при помощи let,
проблема исчезнет. Рассмотрим:
let I = λx. x in if I true then I 1 else 0
Согласно нашему определению, это всего лишь синтаксическая
обёртка для:
(λI . if I true then I 1 else 0) (λx. x)
Это выражение не может быть типизировано согласно нашим
правилам, ибо функция тождества тут одна, и ей должен быть задан
один тип.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Let-полиморфизм (2)
С таким ограничением практическое использование
функционального программирования невозможно. Чтобы избежать
его нам понадобится выполнить два действия.
Во-первых, мы сделаем конструкцию let примитивной, вместо того,
чтобы отнести её к синтаксической обёртке, как мы делали раньше.
Во-вторых, мы добавим новое правило типизации:
Γ ` s : σ Γ ` t[s/x] : τ
Γ ` let x = s in t : τ
Теперь мы можем записывать выражения, такие как в предыдущем
слайде, в том виде, как мы и ожидали.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Наиболее общие типы (1)
Как мы уже сказали, различные типы терма структурно схожи.
Собственно говоря, существует наиболее общий тип, а все остальные
типы всего лишь отдельные случаи такого типа.
Мы говорим, что тип σ более общий, нежели σ 0 , и записываем
σ ≤ σ 0 , если мы можем подставить типы вместо типовых
переменных в σ и получить σ 0 .
Формально определение подстановки в отношении типов достаточно
просто, потому что тут нет понятия связанности. Мы будем
использовать ту же запись, что и для λ-выражений. Например:
α → bool ≤ (τ → τ ) → bool
потому что
(α → bool )[(τ → τ )/α] = (τ → τ ) → bool
Но не наоборот.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Наиболее общие типы (2)
У любого выражения в ML, которое имеет тип, есть наиболее общий
тип. Первым в похожей ситуации это доказал Хиндли, а для нашего
случая – Милнер.
Более того, существует алгоритм нахождения наиболее общего типа
для любого выражения, даже если оно вообще не содержит
информации о типах.
В ML используется этот алгоритм. Поэтому в ML никогда не надо
прописывать типы. Назначение типов происходит неяно.
Таким образом, система типов в ML менее утомительна, чем во
многих других языках, таких как Modula-3. Нам никогда не надо
задавать типы явно, и мы можем использовать один и тот же код с
разными типами, так как компилятор всё сделает за нас.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Сильная нормализация
Вспомним наш пример терма, у которого нет нормальной формы.
Например, такой как:
((λx. x x x) (λx. x x x))
−→ ((λx. x x x) (λx. x x x) (λx. x x x))
−→ (· · · )
В типизированном λ-исчислении такого не может произойти — у
любого типизируемого терма есть нормальная форма, и все
последовательности редукций завершаются на нормальной форме.
Это свойство называется сильной нормализацией.
Это замечательно — любая программа завершается. Однако, это
означает, что мы не можем написать все вычислимые, или даже все
интересные, функции. Нам надо что-то добавить.
Джон Харрисон Введение в Функциональное программирование
Лекция 4. Типы
Рекурсия
Мы не можем определять произвольные рекурсивные функции,
иначе мы смогли бы определить функцию, которая никогда не
завершается.
Очевидно, что функция Y = λf . (λx. f (x x))(λx. f (x x)) не
полностью типизирована, так как она применяет x к самой себе.
Таким образом, нам надо найти способ определения произвольных
рекурсивных функций, которые полностью типизированы.
Введём семейство полиморфных операторов рекурсии в виде:
Rec : ((α → β) → (α → β)) → α → β
и дополнительное правило редукции, такое, что для любой функции
F : (σ → τ ) → (σ → τ ). В итоге мы имеем:
Rec F −→ F (Rec F )
Джон Харрисон Введение в Функциональное программирование
