§ Введение в зависимо-типизированные алгебры
§§ Обыкновенные и матричные алгебры
Алгебры описываются в терминах грамматики и отношений взаимозаменяемости. В обыкновенных алгебрах (таких как моноид, группа, решётка, кольцо, поле) мы выделяем ровно один тип грамматических сущностей, но вообще говоря типов может быть много (напр. Существительное, Прилагательное, Глагол).
Чтобы ознакомиться с обозначениями, рассмотрим к примеру определение моноида:
a : M b : M
–———– ——————— ————————————————
M e : M a · b : M
x : M
——————————————————————————
x · e = x e · x = x
a : M b : M c : M
———————————————————————————
(a·b)·c = a·(b·c)
Тут встречаем все три типа суждений, которые понадобятся нам и в дальнейшем: “M” вводит нам тип M; “term : M” вводит нам представителей типа M; “α = β” задаёт аксиому, что α и β синтаксически взаимозаменимы.
Тем, кто изучал линейную алгебру, известен как минимум один пример алгебры, где типа уже два: линейные пространства. Там фигурируют два типа полукольцо скаляров K и линейное пространство V над ним.
a : T b : T c : K x : T
———————— ———————————————— ———————————————— —————————————————
K V 0 : T 1 : K a + b : T с · x
(в обоих типах есть (для обоих типов (любой x можно слева
нули, в K единица) имеется сложение) домножать на скаляр)
x : T x : T y : T с : K
——————————————————————— ————————————————— —————————
1·x = x 0 + x = x x + y = y + x c·1 = c
c : K a : T b : T a : K b : K x : T
————————————————————————— —————————————————————————
c·(a + b) = c·a + c·b (a + b)·x = a·x + b·x
a : T b : T c : T a : K b : K x : T
———————————————————————————— —————————————————————————
(a + b) + c = a + (b + c) (a·b)·x = a·(b·x)
Несложно развить эту идею и определить алгебру всевозможных конечномерных пространств над K, это уже будет алгебра с бесконечным количеством типов. Для этого просто уберём из системы выше тип V (он может обозначать бесконечномерное линейное пространство над K, в то время как мы хотим работать только с конечномерными), зато добавим новый конструктор типов, соответствующий конструктор элементов, и аксиому, говорящую нам как именно элементы складываются и домножаются на скаляр:
A B a : A b : B a : A x : A b : B y : B c : K
————————— ————————————————— ———————————————————————————————————————(покомпонентная линейная комбинация)
A ⊕ B (a, b) : A ⊕ B (a, b) + c·(x, y) = (a + c·x, b + c·y)
Теперь в нашей системе кроме типа K заведомо есть двумерный тип K ⊕ K, трёхмерные типы (K ⊕ K) ⊕ K и K ⊕ (K ⊕ K), и так далее.
Отметим, что добавить аксиому (A ⊕ B) ⊕ C = A ⊕ (B ⊕ C), чтобы схлопнуть эквивалентные типы каждой фиксированной размерности мы не можем, т.к. привело бы к синтаксической взаимозаменяемости (a, (b, c)) и ((a, b), c), в то время как правило покомпонентной линейной комбинации не сработает применительно к двум по-разному обёрнутым в скобки выраженям.
Несложно также развить систему, добавив в неё тип матриц, операцию их действия на векторы, аксиому, гарантирующую линейность этого действия, и аксиому, говорящую нам, как именно складываются и умножаются матрицы:
A B f : A -> B a : A f : A -> B a : A x : A c : K
———————— ————————————————————— ————————————————————————————————————
A -> B f(a) : B f(a + c·x) = f(a) + c·f(x)
a : A f : A -> B g : A -> B c : K
—————————————————————————————————————————
(f + c·g)(a) = f(a) + c·g(x)
Для типов вида K и A ⊕ B мы можем легко описать также и конструкторы матриц:
c : K f : A => X g : B => X u : A => Y w : B => Y
———————————— ————————————————————————————————————————————————————
c : K => K (f, g; u; w) : A ⊕ B => X ⊕ Y
f : A => X g : B => X u : A => Y w : B => Y a : A b : B
————————————————————————————————————————————————————————————————————
(f, g; u; w)(a, b) = (f(a) + g(b), u(a) + w(b))
Однако мы не можем описать конструктор типа A -> B в общем виде, без разбора того, как именно устроены A и B. Такая ситуация будет и в дальнейшем встречаться при определении конструкторов стрелочных типов (в частности, в типизированных лямбда-исчислениях). Семантически это связано в нашем случае с тем, что если в теорию добавить назад произвольный тип V (не обязательно конечномерное линейное пространство над K), то вообще говоря неверно, что все линейные отображения можно представить конечными термами (даже если K конечное поле, множество линейных отображений K^ω -> K^ω несчётно бесконечено).
§§ Правила вычисления и каноничность
В типизированной алгебре можно снабдить часть правил синтаксической взаимозаменяемости выделенным направлением, такие правила называют правилами вычисления. Для выделения правил вычисления среди правил взаимозаменяемости по историческим причинам приписывают к знаку равенства индекс бета, а равенство читают слева-направо, например: (f, g; u; w)(a, b) =ᵦ (f(a) + g(b), u(a) + w(b))
Вычислением называется последовательное применение к выражению всех применимых к нему правил вычисления. Если к выражению неприменимо ни одно правило вычисления, оно называется неприводимым. Наприводимые атомарные (т.е. введённые непосредственно в грамматике, а не составленные из таковых) конструкции называются каноническими конструкторами. Cистема называется вычислительно-полноценной (computationally sound), если вычислительных правил достаточно, чтобы неприводимыми могли быть только выражения, содержащие канонический конструктор в корневой позиции.
@Remark: Не обязательно (и, как правило, невозможно) превращать все правила синтаксической взаимозаменяемости системы в правила вычислительнения.
Теперь будем рассматривать направленный граф, получаемый из выражения t применением всевозможных правил редукции.
@Definition: Если любой путь исходящий из t приводит к (какому-нибудь) неприводимому выражению, система называется нормализующей в сильном смысле.
@Definition: Если существует путь, исходящий из t и приводящий к (какому-нибудь) неприводимому выражению, система называется нормализующей в слабом смысле.
@Remark: Отметим, что ни то, ни другое свойство не означает ни того, что этот граф имеет конечный размер (всегда может быть так, что у нас есть бесконечно много разных цепочек вычислений, каждая из которых конечной длины), ни того, что результат вычисления не зависит от того, какая цепь редукций выбрана.
@Definition: Если для любых двух путей t -...-> a и t-...-> b существует такой c, что есть пути a -...-> c и b -...-> с, система называется конфлуэтнтной. Это свойство также называют diamond property. Если система нормализует хотя бы в слабом смысле и конфлуэнтна, то она нормализует в сильном смысле и любой порядок применения вычислительных правил приводит к одному и тому же результату.
В дальнейшем мы сконцентрируемся на вычисляющих системах, т.е. вычислительно-полноценных конфлуэнтно-нормализующих системах.
@Remark: Немного более широкий класс вычисляющих систем получается, если допустить, что направление правил вычисления может выбираться по-разному в разных контекстах в зависимости от того, значение какого типа требуется получить в качестве результата. Используя такой приём возможно, например, сделать в матричных алгебрах типы K и K => K (матрицы 1х1 над кольцом K) взаимозаменяемыми синтаксически. Об этом мы ещё планируем написать в главе про выведение и двустороннюю проверку типов.
§§ Типы конечной информационной ёмкости и каноничность
Рассмотрим тип Bool с двумя конструкторами tt (true) и ff (false), снабженный оператором ветвления switch(a, b)(x), приводимым к a или b, если x имеет вид tt или ff соответствено:
x : Bool a : Z b : Z
—————— ———————————————————————— —————————————————————————————
Bool tt : Bool ff : Bool switch(a, b)(x) : Z
a : Z b : Z
————————————————————————————————————————————————
switch(a, b)(tt) =ᵦ a switch(a, b)(ff) =ᵦ b
Чтобы гарантировать, что после такого определения в системе случайно не образуется какого-нибудь zz : Bool, не приводимого к tt или ff, нам понадобится ещё одно правило:
x : Bool
——————————————————————
x = switch(tt, ff)(x)
(такие правила называются правилами уникальности или, по историческим причинам, η-правила). В любой системе, содержащей все 5 приведенных выше правил, вычислительность гарантирует, что не существует x : Bool, не заменимого синтаксически на tt или ff.
В самом деле: любой x : Bool может быть приведён к виду switch(tt, ff)(x), наличие вычислительных правил для switch гарантирует, что оператор switch не является каноническим конструктором таким образом в вычислительно-полноценной системе выражение switch(a, b)(x) : Bool не может являться неприводимым, а определение оператора switch гарантирует, что для неё нельзя записать вычислительных правил, редуцирующих её к чему-либо кроме первого или второго аргумента, стало быть switch(tt, ff)(x) в конечном итоге редуцируется либо к tt, либо к ff. Таким образом всякий x : Bool синтаксически взаимозаменяем либо с tt, либо с ff.
Типы, устроенные как Bool (т.е. по-существу, типы-перечисления, имеющие конечное число элементов с точностью до синтаксической взаимозаменимости) называются типами конечной информационной ёмкости.
Вычислительные системы называются каноническими в слабом смысле, если для каждого такого типа T верно, что замкнутое выражение t : T вычисляется до канонического конструктора типа T. Если это утверждение верно хотя бы для одного такого типа T с не менее чем двумя конструкторами, например, Bool, то оно верно и для всех остальных. Как мы видим, это свойство выполнено вообще говоря для любой вычислительно-полноценной конфлуэнтно-нормализующей системы.
Каноничность в сильном смысле — это утверждение о том, что всякое замкнутое выражение n : Nat (определение типа натуральных чисел см. ниже) вычисляется до нумерала. (Вместо Nat в определении можно взять любой бесконечный индуктивный тип.)
Пример матричной алгебры мотивирует понятие “типа T с конечной информационной ёмкостью относительно типа K”, т.е. “если тип K имеет конечную информационную ёмкость, то T тоже”. Это верно для всех типов, которые можно определить внутри матричной алгебры: конечномерные линейные пространства над конечными полями и кольцами сами по себе конечны. Наиболее естественным примером такого типа является тип пары:
A B a : A b : B x : A × B
——————— ———————————————— ———————————————————————————————————————————————————
A × B (a, b) : A x B fst(x) : A snd(x) : B x = (fst(x), snd(x))
a : A b : B
————————————————————————————————
fst(a, b) =ᵦ a snd(a, b) =ᵦ b
§§ Суждения с “дырками” и лямбда-термы
Пусть у нас есть некая типизированная алгебра, мы хотим добавить в неё типы вида A -> B, содержащие всевозможные выражения типа B с “дыркой”, куда можно подставлять любые выражения типа A. Для этого добавим новый формат суждений: (x : X) ⊢ y : Y
Оно означает, “y представляет собой терм типа Y, содержащий свободную переменную (“дырку”) x типа Y.
Теперь мы можем определить тип A -> B:
X Y (x : X) ⊢ y : Y f : X -> Y x : X
———————— ———————————————————————— —————————————————————
X -> Y (λx : X, y) : X -> Y f(x) : X
f : X -> Y (x : X) ⊢ y : Y x' : X
———————————————————— ——————————————————————————————
f = (λx : X, f(x)) (λx : X, y)(x) =ᵦ y[x: x']
Тут term[name: value] обозначает подстановку value вместо name в выражении term.
TODO: Сказать, что для всякой замкнутой теории (т.е. фиксированного набора правил) мы можем определить лямбда-выражения и индуктивно, говоря что он сделаны из имеющихся в теории конструкторов и экстракторов, например для матричной алгебры из первой главы тип A => B, определённый через лямба-выражения, совпадёт с уже определённым там типом матриц A => B. Однако, если расширить теорию например типом V потенциально бесконечномерных линейных пространств, типы начнут расходиться, ведь в определении матриц задано лишь, как они работают с определёнными прежде типами, в то время как A -> B расширяется “автоматически” при добавлении новых типов.
§§ STLC(+×→): Просто-типизированное лямбда-исчисление.
§§ Индуктивные типы
§§ Вселенные и сабтайпинг
TODO: Делаем вселенную U и иерархию вселенных U'. Говорим, что можно нафигачить в системе типов сахарок: хак, что все элементы u : U автоматически “живут и в U'”, т.е. u : U'.
§§ Зависимо-типизированные пары и типы-ограничения
Пример: натуральные не меньше n.
Определим f : Nat -> Nat -> U, которая для всех m <= n выдаёт '0 : U, если оно меньше и '1 : U, если меньше.
Потом делаем Nat × f(5) и получаем тип, у которого fst это всегда натуральное число не меньше 5, а snd всегда из типа 1 и потому его можно игнорить.
Говорим, что можно нафигачить в системе типов сахарок: вселенную Prop, в которой живут только коды 0, 1 и |any-type-code|, и конструктор T ⋉ (f : T -> Prop), такой что все эти типы автоматически надтипы T, т.е. если t : T ⋉ f, то t : T, т.е. можно не писать fst каждый раз. А второй элемент пары добывается через #TYPE(t). Потом этот сахарог ещё можно будет применять для пар, где второй элемент блесснутый, там тоже можно по умолчанию дефлотиться в fst, а разные snd добывать по их типу.
§§ Зависимо-типизированные отображения
TODO: Пример функции, отображающей Nat -> Nat^arg. Пример функции Nat -> Nat, у которой результат всегда не меньше аргумента.