свобода, равенство, унивалентность!
(Disclaimer: не то чтобы я в этом что-то понимал, будьте готовы к куче неточностей и ошибок)
Итак, допустим, ваш ребенок приходит из школы в слезах и говорит, что учитель зачеркнул 9*2 и вписал 2*9, "но ведь это одно и то же!"
А вы, будучи подкованы в современных веяниях науки, отвечаете так. Математика - это лишь прикладная теория типов, поэтому данный вопрос стоит рассмотреть с точки зрения этой теории. В теории типов у нас есть базовые суждения вроде "нечто является типом", "нечто является термом (выражением)" и "такой-то терм имеет такой-то тип" ("a : A"). Потом возникают индуктивные определения, состоящие из посылок и заключений. Например, "если A тип и В тип, то A -> B тоже тип". Еще: "если терм f имеет тип A -> B и терм x имеет тип A, то f x - это валидный терм, и он имеет тип В". Вводятся разные способы построения типов и термов: функция, произведение, сумма... Вводятся базовые типы. И вот тут первый ключевой момент. Если у нас есть терм
mul : Nat -> Nat -> Nat
то
mul 9 2 : Nat
Т.е. терм mul 9 2 - полноправный элемент типа Nat. Не число в привычной нам форме, не результат вычисления функции mul, а само выражение. Кажется, в этом одно из отличий типов от множеств. Никто не скажет, что выражение 9*2 входит в множество натуральных чисел, а вот в тип натуральных оно входит. И терм mul 2 9 тоже имеет тип Nat, и всякому очевидно, что mul 9 2 и mul 2 9 - это разные термы. А еще есть терм 18 того же типа, он на них совсем не похож, но все трое как-то связаны, они "равны". Что это значит? Если бы мы в нашей теории только вводили способы конструирования термов и типов, толку от нее было бы немного. Но у нее есть и вычислительное содержание. Подобно тому, как просветленный ум имеет два аспекта: это союз блаженства и пустоты, т.е. сострадания и мудрости, т.е. ясности и осознавания, т.е. конструирования ментальных образов и их познания, синтеза и анализа, в логике и теории типов всякое конструирование сопровождается способом разбора: если есть создание пары, есть и разбирающие ее на части fst и snd, если есть конструирование списка, есть и его разбор на части, head и tail, если есть конструирование натуральных чисел, есть и их элиминатор, рекурсор - математическая индукция. И вот эти элиминаторы обычно сопровождаются суждениями о равенстве термов. Мы не только говорим, что ежели р : (А,В) то fst p : A, но сопровождаем правилом:
fst (a,b) = a
Именно тут появляется равенство по определению, definitional equality. Именно оно позволяет утверждать, что fst (18, 3) = 18, именно благодаря ему и именно в этом смысле мы говорим, что термы fst (18, 3) и 18 равны. Аналогичное правило есть для рекурсора натуральных чисел, и через него мы определяем функциии на них, вроде той же mul.
Получается такая картина, что в том же типе Nat у нас куча разнообразных термов, и некоторые из них связаны между собой равенствами.
Связанные термы образуют направленные графы (с т.з. вычислений definitional equality связывает термы в определенном направлении - что во что вычисляется). Если мы не успели наделать в теории глупостей (вроде некоторых вредных аксиом), то каждый такой граф будет сходиться в одной точке, канонической форме. Это хорошее свойство, оно позволяет компилятору без труда убедиться, что термы mul 2 9, mul 9 2 и fst (18, 'x') равны по определению, достаточно каждый из них вычислить, пробежавшись по графу до канонической формы, и убедиться, что получился тот же терм (с точностью до переименования переменных, если они в нем есть). Более того, компилятор даже понимает, что 0 + x = x. Но вот что x + 0 = x он уже не понимает, термы x + 0 и x не definitionally equal, не равны в этом смысле, их не связывает путь в том графе. Потому что сложение у нас определено матчингом по первому аргументу; когда первый аргумент Z или S n, у нас есть какие-то равенства на этот счет, но когда первый аргумент - переменная, все, приехали. Тем более выражения x * y и y * x не равны definitionally. "Но ведь это одно и то же!"
Чтобы выразить эту однуитужесть, придумали propositional equality. В теории типов мы в типах можем выражать утверждения конструктивной математики, теоремы, а в термах их доказательства. Получилось построить терм нужного типа, населить тип - доказали теорему. Не получилось, тип остался пустым - теорема не доказана. Так вот, мы можем выразить утверждение "x = y" в виде типа, так называемого identity type. Терм такого типа будет доказательством, конструктивным обоснованием почему x = y. Подобно спискам и натуральным числам, опишем его в виде индуктивного типа (это должен быть инициальный объект в определенной категории), выражающего определенный принцип минимальности, в данном случае это "least reflexive relation", минимальное рефлексивное отношение. Задать его можно так:
если А - некоторый тип, то для него опишем семейство типов, индексированное двумя термами этого типа:
Id_A : A -> A -> Type
id_a : (a : A) -> Id_A a a
т.е. если мы возьмем два объекта x и y типа А, то Id_A x y будет типом, выражающим утверждение x = y. В Агде и Идрисе такой тип так и записывается, "x = y". У этого индуктивного типа один конструктор id_a, который для всякого значения a из A дает терм id_a(a) типа Id_A a a, т.е. служит доказательством того, что а=а. В Агде и Идрисе такой терм известен как refl. Все, что мы пока умеем им доказывать, что это отношение рефлексивно, а=а. Теперь, чтобы этот тип был минимальным рефлексивным отношением, он должен служить инициальным объектом в категории себе подобных, и выражается это так. Для любого типа А и любых его значений x и y, для любого утверждения D, опирающегося на равенство x=y, и его доказательства d(a) должна существовать стрелка J из нашего identity type в D, дающая это самое доказательство D. При этом D получается зависимым от Id_A x y типом, а стрелка J - его сечением (пи-типом). Т.е. если
D : {x,y : A} -> Id_A x y -> Type
d : (a : A) -> D a a id_a
то существует
J(D,d) : {x,y :A} -> (p : Id_A x y) -> D x y p
с таким свойством, что
J(D, d, id_a) = d(a)
Выглядит с непривычки сложно, но это просто один из стандартных способов описания произвольных индуктивных типов в теории с зависимыми типами - через dependent elimination. В результате у нас появляется способ конструировать какие-то следствия. Например, если положить
D(x, y, p) = Id_A y x и
d = \x -> id_x : (x : A) -> D(x, x, id_x)
то J дает нам
J(D,d,x,y,p) : Id_A y x для каждого p : Id_A x y. Тогда inv = J(D,d,x,y) это функция из Id_A x y в Id_A y x. А вычислительное правило для J дает inv(id_x) = id_x. Мы получили симметричность отношения.
Аналогично можно получить функцию композиции
(о) : Id_A y z -> Id_A x y -> Id_A x z
дающую транзитивность. Мы получили тройку рефлексивность-симметричность-транзитивность, т.е. отношение эквивалентности. Причем симметричность и транзитивность оказались выведены как свойства, следствия из минимальной рефлексивности.
Пользуясь таким понятием равенства, мы можем показать, что x*y равно y*x, т.е. тип Id_Nat (x*y) (y*x) населен. Это то, что делается в библиотеках Агды, Идриса и других языков этого уровня. Леммы про коммутативность умножения там имеют такой тип. Однако если мы возьмем две функции f,g : Nat -> Nat
f x = 2 * x
g x = x * 2
то доказать их равенство, не только definitional, но даже propositional, мы не сможем! "Но это же одно и то же!"
Для этого нам требуется function extensionality - принцип, гласящий, что если для всякого аргумента две функции дают одинаковые результаты, то сами эти функции равны. В интенсиональной теории типов, что тут пока излагалась, этот принцип невыводим. И это разумно: мы вовсе не обязательно хотим считать равными функциями те, что дают одинаковые результаты, нам ведь может быть небезразлично их внутреннее устройство. Если одна вычисляет результат за константное время, а вторая за экспоненциальное, мы можем захотеть не считать их равными и взаимозаменяемыми. Если же допустить function extensionality, то они становятся равны, неразличимы. Поскольку этот принцип сам собой не выводится, его, если он нужен, можно ввести через дополнительные аксиомы. И тут возможны варианты. Можно его просто в явном виде ввести как аксиому. Можно пойти чуть в обход и, аксиоматизировав uniqueness of identity proofs (UIP), сделать теорию типов экстенсиональной, там function extensionality уже выводится. Но оба подхода имеют проблемы. Перестает работать теорема о канонических формах. Что означает, например, что у нас может возникнуть терм типа Bool, вычисление которого застревает, и в результате не получается ни True, ни False. Кроме того, в экстенсиональной теории из пропозиционального равенства следует вычислительное, из-за чего проверка типов становится неразрешимой. Ну и UIP делает теорию одномерной (об этом позже), неинтересной. Однако есть и другой способ получить function extensionality, не постулируя ее и сохраняя теорию интенсиональной. Для этого нам пригодится топология.
В топологии мы рассматриваем пространства, где у точек бывают соседи, что связывает разные области пространства и позволяет по ним мысленно перемещаться. Две точки в одной связной области мы можем соединить путем, определяемым как непрерывное отображение интервала [0,1] на это пространство. Если один путь заканчивается в некоторой точке, а другой в ней начинается, мы можем из них составить композицию путей. Кроме того, всякий путь мы можем развернуть, пройти его в обратном направлении, оказавшись в исходной точке. Имея два пути p и q из точки х в точку y, мы можем рассмотреть непрерывное отображение одного пути в другой.
Это уже будет непрерывное отображение интервала [0,1] на пространство путей, или, что то же самое, отображение квадрата [0,1]х[0,1] на исходное пространство, двумерная такая поверхность. Такое отображение называется гомотопией. И если рассматривать не исходное пространство Х, а уже пространство путей в нем, то гомотопии в Х будут служить путями в этом пространстве путей. Их тоже можно отображать друг в друга, получая уже трехмерные штуковины, их - дальше, в четырехмерные и т.д. до бесконечности. При этом когда мы гомотопией непрерывно превращаем один путь в другой, нам важно, чтобы его начальная и конечная точки оставались на месте, а все другие мы можем шевелить свободно, лишь бы это делалось плавно, непрерывно. Если возьмем некоторый путь p из х в y, возьмем обратный к нему p-1, полученный просто сменой направления, и возмьмем их композицию p-1 . р, получим путь из х в х. Он будет отличен от тривиального пути из х в х - стояния на месте. Однако теперь, когда точка y перестала быть концом, мы можем наш составной путь начать шевелить, и плавно и непрерывно можем его стянуть до стояния на месте, тривиального пути из х в х, построить гомотопию из p-1 . р в id_x. Говорят, что такие пути равны с точностью до гомотопии.
Теперь вернемся к теории типов. Если мы посмотрим на описанные выше identity types, то увидим, что они ведут себя в точности как пути в топологии! Тип IdA x y "соединяет" точки x и y в пространстве (типе) А. У него всегда есть обратный путь IdA y x, мы можем строить композиции. Более того, тип IdA x y мы можем рассматривать как пространство и задуматься о пропозициональном равенстве элементов этого пространства, т.е. путей в нем. Если p и q - доказательства того, что x=y, они оба имеют тип IdA x y. Утверждение о том, что они сами равны, будет типом
IdIdA x y p q
Если a и b - доказательства того, что p = q, то утверждение, что a = b будет типом
IdIdIdA x y p q a b
и т.д. до бесконечности.
Итак, допустим у нас есть путь p из x в y и тривиальные пути id_x из х в х и id_y из y в y. Как связаны p и p . id_x? Оказывается, они не равны definitionally, но равны propositionally, т.е. из p в p . id_x есть путь, мы его можем построить конструктивно, пользуясь индуктивным определением IdA y x и его элиминатором J. Так мы можем доказать следующие утверждения, т.е. представить конкретные функции этих типов:
1) reflRight: p ~~> (p o id_x)
2) invLeft : p-1 o p ~~> id_x и invRight : p o p-1 ~~> id_y
3) invTwice : (p-1)-1 ~~> p (исправлено, тут была ошибка)
4) assoc : r o (q o p) ~~> (r o q) o p
Тут (q o p) - композиция путей, как описана ранее, а "x ~~> y" - синоним для IdA x y, такое обозначение проще и лучше отражает идею пути из х в y.
Подобно тому, как в топологии композиция пути с обратным ему не тождественна тривиальному пути, но равна с точностью до гомотопии, пути более высокого измерения, так и композиция idenity type с обратным не равна-по-определению тривиальному (id_x a.k.a. refl), но равна с точностью до idenity type более высокого порядка, пути более высокого измерения. Заметим, что перечисленные свойства очень похожи на определение группы, где есть пространство некоторых элементов (здесь это пути), есть ассоциативная бинарная операция "умножения" (в данном случае это композиция), есть нейтральный элемент, который при участии в умножении не меняет результата (тут тривиальный путь), у каждого элемента есть обратный (тут обратный путь), умножение на который дает нейтральный элемент. Только в группе это все должны быть прямые равенства, не "с точностью до". Есть еще понятие группоида - это категория, где все стрелки - изоморфизмы, тогда если там взять стрелки как элементы группы, а их композицию как умножение, все законы группы выполняются, но опять же там равенства более строгие. Когда же равенства в группоиде выполняются с точностью до путей более высокого измерения, которые сами опять образуют такую псевдогруппу, где законы выполняются с точностью до путей еще более высокого измерения и т.д. до бесконечности, такая конструкция называется ∞-группоид. Так вот, выходит, что и типы в интенсиональной теории типов, и топологические пространства имеют одну и ту же алгебраическую структуру ∞-группоида. Вот мы и приехали к гомотопической теории типов (HoTT), теперь название такое должно быть понятно откуда берется.
Гомотопия в HoTT определяется чуть иначе, чем в топологии, она как бы повернута на 90 градусов. Если у нас есть две функции f и g типа A -> B, то гомотопия между ними определяется как
H = (x : A) -> f x ~~> g x
Это функция, которая для каждого х из А производит доказательство того, что f x = g x. Тип такой функции, пространство всех гомотопий между f и g обозначается f ~ g.
Имея арсенал зависимых типов и путей, можно рассуждать о таких топологических вещах, как стягиваемость пространств и их эквивалентность. Пространство А стягиваемо, если в нем существует такой элемент а, что любой элемент х из А ему равен:
isContr(A) := Exists (a:A), (x:A) -> x ~~> a
т.е. для доказательства стягиваемости пространства А мы должны предъявить зависимую пару, где первый элемент - значение а из А, а второй - функция, которая для каждого х производит доказательство того, что х = а, конкретный путь из х в а. В частности, несложно показать, что тип unit стягиваемый. Стягиваемый тип обязан быть непустым, иначе мы не сможем предъявить а.
Эквивалентность пространств можно определять немного по-разному, есть альтернативные подходы. Например, если у нас есть функция f : A -> B и точка b в B, можно сначала определить homotopy fiber
hFiber(f,b) := Exists (a:A), f a ~~> b
Это тип пар, где первый элемент - значение из А, а второй - доказательство того, что f его отображает в значение, равное b. Фактически, это обратный образ для f в точке b. Утверждение, что функция f - это эквивалентность, это такой тип:
isEquiv(f) := (b : B) -> isContr( hFiber(f,b) )
Т.е. если для каждой точки b из B существует ее праобраз в А (относительно f). Очень похоже на биекцию, только равенства везде пропозициональные. Отдельно доказывается, что всякая функция-эквивалентность это изоморфизм и наоборот.
Ну а дальше мы говорим, что пространства (типы) А и В эквивалентны, если существует такая функция f для которой населен isEquiv(f). Эквивалентность пространств А и В будем обозначать А ~= B.
Теперь, мы можем рассмотреть пространство всех типов Type (не включая его самого, делаем стандартную иерархию вселенных а-ля Агда и подкапотный Идрис). Обычные типы, вроде Nat и (Int -> Int), будут его элементами. Тогда для двух элементов типа Type, для двух типов А и В, мы можем задуматься: а когда они равны? Утверждение о равенстве двух типов А и В будет типом
IdTypeA B
или в нашем новом обозначении A ~~> B. Это тип, т.е. тоже пространство, точки в котором - это доказательства равности А и В, пути в Type. Утверждение об эквивалентности простанств А и В, А ~= B, это тоже тип, тоже пространство. Мы можем построить конструктивно функцию
v(A,B) : (A ~~> B) -> (A ~= B)
которая логически означает, что из пропозиционального равенства двух типов следует их эквивалентность. При этом сама v - это функция из пространства (A ~~> B) в пространство (A ~= B). Что можно сказать об этих двух пространствах? Тут приходит Воеводский и говорит: давайте добавим одну аксиому, аксиому унивалентности:
univalence : {A, B : Type} -> isEquiv( v(A,B) )
т.е. постулируем, что такая v - это эквивалентность. Другими словами,
(A ~~> B) ~= (A ~= B)
пространство путей между двумя типами эквивалентно пространству эквивалентностей (и изоморфизмов) между этими типами. Бах!
Внезапно, наличие такой аксиомы сразу дает очень много плюшек и многое упрощает. В том числе из нее автоматом получается следствие
ndfe : {f,g : A -> B} -> (f ~ g) -> (f ~~> g)
- это наивная независимотиповая function extensionality; из гомотопии между f и g можно получить доказательство равности f и g. Возвращаясь ближе к началу поста, у нас были
f x = 2 * x
g x = x * 2
доказать равенство которых мы не могли. Мы можем построить гомотопию
H : (x : A) -> f x ~~> g x
которая для каждого x произведет доказательство того, что 2 * x = x * 2 (это банальное упражнение для агда-программистов), и теперь ndfe H нам даст значение типа f ~~> g, т.е. доказателство равности этих двух функций. В случае зависимых типов, доказывается, что из унивалентности также следует weak function extensionality:
wfe : ((x:A) -> isContr(P x)) -> isContr( (x:A) -> P x )
а еще ранее, безо всякой унивалентности, можно было показать, что из нее следует strong function extensionality:
sfe : (f,g : (x:A) -> P x) -> isEquiv( hApply(f,g) )
где
hApply : (f, g : (x:A) -> P x) -> (f ~~> g) -> (f ~ g)
т.е. для всяких зависимых функций из (х:А) в (Р х) пространство гомотопий между ними эквивалентно пространству путей между ними.
Вот так, добавив одну аксиому, можно сохранить интенсиональность теории типов, ее многомерную структуру и получить доказательство равности f x = 2 * x и g x = x * 2.
К слову о многомерности. В этой теории типы можно классифицировать по уровням. Чтобы было интересней, в классической гомотопической теории они нумеруются начиная с -2. Тип уровня -2 - это любой стягиваемый тип, например unit, он же () в хаскеле.
Тип уровня -1 - это h-prop, он характеризуется формулой A -> isContr(A): он стягиваем если населен. Его еще называют proof-irrelevant, любые два значения его пропозиционально равны, но в отличие от уровня -2 они могут и не существовать вовсе. Такой тип используется для записи многих логических утверждений.
Тип уровня 0 - это h-set, тип множеств. В таком типе может быть много разных значений, но любые доказательства равности его элементов сами между собой равны, т.е. справедлив принцип uniqueness of identity proofs. В ETT, экстенсиональной теории типов, все типы - это такие одномерные множества.
Тип уровня 1 - это группоид, в нем могут быть нетривиальные морфизмы, но все 2-морфизмы тривиальны. И т.д. Категорно, n-типы соответствуют n-группоидам.
Получаются такие типы обрезанием ∞-группоида, когда мы выбираем некоторый уровень n и объявляем все пути более высокого порядка равными.
Вот, как-то так обстоят дела с 2*9=9*2.
Итак, допустим, ваш ребенок приходит из школы в слезах и говорит, что учитель зачеркнул 9*2 и вписал 2*9, "но ведь это одно и то же!"
А вы, будучи подкованы в современных веяниях науки, отвечаете так. Математика - это лишь прикладная теория типов, поэтому данный вопрос стоит рассмотреть с точки зрения этой теории. В теории типов у нас есть базовые суждения вроде "нечто является типом", "нечто является термом (выражением)" и "такой-то терм имеет такой-то тип" ("a : A"). Потом возникают индуктивные определения, состоящие из посылок и заключений. Например, "если A тип и В тип, то A -> B тоже тип". Еще: "если терм f имеет тип A -> B и терм x имеет тип A, то f x - это валидный терм, и он имеет тип В". Вводятся разные способы построения типов и термов: функция, произведение, сумма... Вводятся базовые типы. И вот тут первый ключевой момент. Если у нас есть терм
mul : Nat -> Nat -> Nat
то
mul 9 2 : Nat
Т.е. терм mul 9 2 - полноправный элемент типа Nat. Не число в привычной нам форме, не результат вычисления функции mul, а само выражение. Кажется, в этом одно из отличий типов от множеств. Никто не скажет, что выражение 9*2 входит в множество натуральных чисел, а вот в тип натуральных оно входит. И терм mul 2 9 тоже имеет тип Nat, и всякому очевидно, что mul 9 2 и mul 2 9 - это разные термы. А еще есть терм 18 того же типа, он на них совсем не похож, но все трое как-то связаны, они "равны". Что это значит? Если бы мы в нашей теории только вводили способы конструирования термов и типов, толку от нее было бы немного. Но у нее есть и вычислительное содержание. Подобно тому, как просветленный ум имеет два аспекта: это союз блаженства и пустоты, т.е. сострадания и мудрости, т.е. ясности и осознавания, т.е. конструирования ментальных образов и их познания, синтеза и анализа, в логике и теории типов всякое конструирование сопровождается способом разбора: если есть создание пары, есть и разбирающие ее на части fst и snd, если есть конструирование списка, есть и его разбор на части, head и tail, если есть конструирование натуральных чисел, есть и их элиминатор, рекурсор - математическая индукция. И вот эти элиминаторы обычно сопровождаются суждениями о равенстве термов. Мы не только говорим, что ежели р : (А,В) то fst p : A, но сопровождаем правилом:
fst (a,b) = a
Именно тут появляется равенство по определению, definitional equality. Именно оно позволяет утверждать, что fst (18, 3) = 18, именно благодаря ему и именно в этом смысле мы говорим, что термы fst (18, 3) и 18 равны. Аналогичное правило есть для рекурсора натуральных чисел, и через него мы определяем функциии на них, вроде той же mul.
Получается такая картина, что в том же типе Nat у нас куча разнообразных термов, и некоторые из них связаны между собой равенствами.
Связанные термы образуют направленные графы (с т.з. вычислений definitional equality связывает термы в определенном направлении - что во что вычисляется). Если мы не успели наделать в теории глупостей (вроде некоторых вредных аксиом), то каждый такой граф будет сходиться в одной точке, канонической форме. Это хорошее свойство, оно позволяет компилятору без труда убедиться, что термы mul 2 9, mul 9 2 и fst (18, 'x') равны по определению, достаточно каждый из них вычислить, пробежавшись по графу до канонической формы, и убедиться, что получился тот же терм (с точностью до переименования переменных, если они в нем есть). Более того, компилятор даже понимает, что 0 + x = x. Но вот что x + 0 = x он уже не понимает, термы x + 0 и x не definitionally equal, не равны в этом смысле, их не связывает путь в том графе. Потому что сложение у нас определено матчингом по первому аргументу; когда первый аргумент Z или S n, у нас есть какие-то равенства на этот счет, но когда первый аргумент - переменная, все, приехали. Тем более выражения x * y и y * x не равны definitionally. "Но ведь это одно и то же!"
Чтобы выразить эту однуитужесть, придумали propositional equality. В теории типов мы в типах можем выражать утверждения конструктивной математики, теоремы, а в термах их доказательства. Получилось построить терм нужного типа, населить тип - доказали теорему. Не получилось, тип остался пустым - теорема не доказана. Так вот, мы можем выразить утверждение "x = y" в виде типа, так называемого identity type. Терм такого типа будет доказательством, конструктивным обоснованием почему x = y. Подобно спискам и натуральным числам, опишем его в виде индуктивного типа (это должен быть инициальный объект в определенной категории), выражающего определенный принцип минимальности, в данном случае это "least reflexive relation", минимальное рефлексивное отношение. Задать его можно так:
если А - некоторый тип, то для него опишем семейство типов, индексированное двумя термами этого типа:
Id_A : A -> A -> Type
id_a : (a : A) -> Id_A a a
т.е. если мы возьмем два объекта x и y типа А, то Id_A x y будет типом, выражающим утверждение x = y. В Агде и Идрисе такой тип так и записывается, "x = y". У этого индуктивного типа один конструктор id_a, который для всякого значения a из A дает терм id_a(a) типа Id_A a a, т.е. служит доказательством того, что а=а. В Агде и Идрисе такой терм известен как refl. Все, что мы пока умеем им доказывать, что это отношение рефлексивно, а=а. Теперь, чтобы этот тип был минимальным рефлексивным отношением, он должен служить инициальным объектом в категории себе подобных, и выражается это так. Для любого типа А и любых его значений x и y, для любого утверждения D, опирающегося на равенство x=y, и его доказательства d(a) должна существовать стрелка J из нашего identity type в D, дающая это самое доказательство D. При этом D получается зависимым от Id_A x y типом, а стрелка J - его сечением (пи-типом). Т.е. если
D : {x,y : A} -> Id_A x y -> Type
d : (a : A) -> D a a id_a
то существует
J(D,d) : {x,y :A} -> (p : Id_A x y) -> D x y p
с таким свойством, что
J(D, d, id_a) = d(a)
Выглядит с непривычки сложно, но это просто один из стандартных способов описания произвольных индуктивных типов в теории с зависимыми типами - через dependent elimination. В результате у нас появляется способ конструировать какие-то следствия. Например, если положить
D(x, y, p) = Id_A y x и
d = \x -> id_x : (x : A) -> D(x, x, id_x)
то J дает нам
J(D,d,x,y,p) : Id_A y x для каждого p : Id_A x y. Тогда inv = J(D,d,x,y) это функция из Id_A x y в Id_A y x. А вычислительное правило для J дает inv(id_x) = id_x. Мы получили симметричность отношения.
Аналогично можно получить функцию композиции
(о) : Id_A y z -> Id_A x y -> Id_A x z
дающую транзитивность. Мы получили тройку рефлексивность-симметричность-транзитивность, т.е. отношение эквивалентности. Причем симметричность и транзитивность оказались выведены как свойства, следствия из минимальной рефлексивности.
Пользуясь таким понятием равенства, мы можем показать, что x*y равно y*x, т.е. тип Id_Nat (x*y) (y*x) населен. Это то, что делается в библиотеках Агды, Идриса и других языков этого уровня. Леммы про коммутативность умножения там имеют такой тип. Однако если мы возьмем две функции f,g : Nat -> Nat
f x = 2 * x
g x = x * 2
то доказать их равенство, не только definitional, но даже propositional, мы не сможем! "Но это же одно и то же!"
Для этого нам требуется function extensionality - принцип, гласящий, что если для всякого аргумента две функции дают одинаковые результаты, то сами эти функции равны. В интенсиональной теории типов, что тут пока излагалась, этот принцип невыводим. И это разумно: мы вовсе не обязательно хотим считать равными функциями те, что дают одинаковые результаты, нам ведь может быть небезразлично их внутреннее устройство. Если одна вычисляет результат за константное время, а вторая за экспоненциальное, мы можем захотеть не считать их равными и взаимозаменяемыми. Если же допустить function extensionality, то они становятся равны, неразличимы. Поскольку этот принцип сам собой не выводится, его, если он нужен, можно ввести через дополнительные аксиомы. И тут возможны варианты. Можно его просто в явном виде ввести как аксиому. Можно пойти чуть в обход и, аксиоматизировав uniqueness of identity proofs (UIP), сделать теорию типов экстенсиональной, там function extensionality уже выводится. Но оба подхода имеют проблемы. Перестает работать теорема о канонических формах. Что означает, например, что у нас может возникнуть терм типа Bool, вычисление которого застревает, и в результате не получается ни True, ни False. Кроме того, в экстенсиональной теории из пропозиционального равенства следует вычислительное, из-за чего проверка типов становится неразрешимой. Ну и UIP делает теорию одномерной (об этом позже), неинтересной. Однако есть и другой способ получить function extensionality, не постулируя ее и сохраняя теорию интенсиональной. Для этого нам пригодится топология.
В топологии мы рассматриваем пространства, где у точек бывают соседи, что связывает разные области пространства и позволяет по ним мысленно перемещаться. Две точки в одной связной области мы можем соединить путем, определяемым как непрерывное отображение интервала [0,1] на это пространство. Если один путь заканчивается в некоторой точке, а другой в ней начинается, мы можем из них составить композицию путей. Кроме того, всякий путь мы можем развернуть, пройти его в обратном направлении, оказавшись в исходной точке. Имея два пути p и q из точки х в точку y, мы можем рассмотреть непрерывное отображение одного пути в другой.
Это уже будет непрерывное отображение интервала [0,1] на пространство путей, или, что то же самое, отображение квадрата [0,1]х[0,1] на исходное пространство, двумерная такая поверхность. Такое отображение называется гомотопией. И если рассматривать не исходное пространство Х, а уже пространство путей в нем, то гомотопии в Х будут служить путями в этом пространстве путей. Их тоже можно отображать друг в друга, получая уже трехмерные штуковины, их - дальше, в четырехмерные и т.д. до бесконечности. При этом когда мы гомотопией непрерывно превращаем один путь в другой, нам важно, чтобы его начальная и конечная точки оставались на месте, а все другие мы можем шевелить свободно, лишь бы это делалось плавно, непрерывно. Если возьмем некоторый путь p из х в y, возьмем обратный к нему p-1, полученный просто сменой направления, и возмьмем их композицию p-1 . р, получим путь из х в х. Он будет отличен от тривиального пути из х в х - стояния на месте. Однако теперь, когда точка y перестала быть концом, мы можем наш составной путь начать шевелить, и плавно и непрерывно можем его стянуть до стояния на месте, тривиального пути из х в х, построить гомотопию из p-1 . р в id_x. Говорят, что такие пути равны с точностью до гомотопии.
Теперь вернемся к теории типов. Если мы посмотрим на описанные выше identity types, то увидим, что они ведут себя в точности как пути в топологии! Тип IdA x y "соединяет" точки x и y в пространстве (типе) А. У него всегда есть обратный путь IdA y x, мы можем строить композиции. Более того, тип IdA x y мы можем рассматривать как пространство и задуматься о пропозициональном равенстве элементов этого пространства, т.е. путей в нем. Если p и q - доказательства того, что x=y, они оба имеют тип IdA x y. Утверждение о том, что они сами равны, будет типом
IdIdA x y p q
Если a и b - доказательства того, что p = q, то утверждение, что a = b будет типом
IdIdIdA x y p q a b
и т.д. до бесконечности.
Итак, допустим у нас есть путь p из x в y и тривиальные пути id_x из х в х и id_y из y в y. Как связаны p и p . id_x? Оказывается, они не равны definitionally, но равны propositionally, т.е. из p в p . id_x есть путь, мы его можем построить конструктивно, пользуясь индуктивным определением IdA y x и его элиминатором J. Так мы можем доказать следующие утверждения, т.е. представить конкретные функции этих типов:
1) reflRight: p ~~> (p o id_x)
2) invLeft : p-1 o p ~~> id_x и invRight : p o p-1 ~~> id_y
3) invTwice : (p-1)-1 ~~> p (исправлено, тут была ошибка)
4) assoc : r o (q o p) ~~> (r o q) o p
Тут (q o p) - композиция путей, как описана ранее, а "x ~~> y" - синоним для IdA x y, такое обозначение проще и лучше отражает идею пути из х в y.
Подобно тому, как в топологии композиция пути с обратным ему не тождественна тривиальному пути, но равна с точностью до гомотопии, пути более высокого измерения, так и композиция idenity type с обратным не равна-по-определению тривиальному (id_x a.k.a. refl), но равна с точностью до idenity type более высокого порядка, пути более высокого измерения. Заметим, что перечисленные свойства очень похожи на определение группы, где есть пространство некоторых элементов (здесь это пути), есть ассоциативная бинарная операция "умножения" (в данном случае это композиция), есть нейтральный элемент, который при участии в умножении не меняет результата (тут тривиальный путь), у каждого элемента есть обратный (тут обратный путь), умножение на который дает нейтральный элемент. Только в группе это все должны быть прямые равенства, не "с точностью до". Есть еще понятие группоида - это категория, где все стрелки - изоморфизмы, тогда если там взять стрелки как элементы группы, а их композицию как умножение, все законы группы выполняются, но опять же там равенства более строгие. Когда же равенства в группоиде выполняются с точностью до путей более высокого измерения, которые сами опять образуют такую псевдогруппу, где законы выполняются с точностью до путей еще более высокого измерения и т.д. до бесконечности, такая конструкция называется ∞-группоид. Так вот, выходит, что и типы в интенсиональной теории типов, и топологические пространства имеют одну и ту же алгебраическую структуру ∞-группоида. Вот мы и приехали к гомотопической теории типов (HoTT), теперь название такое должно быть понятно откуда берется.
Гомотопия в HoTT определяется чуть иначе, чем в топологии, она как бы повернута на 90 градусов. Если у нас есть две функции f и g типа A -> B, то гомотопия между ними определяется как
H = (x : A) -> f x ~~> g x
Это функция, которая для каждого х из А производит доказательство того, что f x = g x. Тип такой функции, пространство всех гомотопий между f и g обозначается f ~ g.
Имея арсенал зависимых типов и путей, можно рассуждать о таких топологических вещах, как стягиваемость пространств и их эквивалентность. Пространство А стягиваемо, если в нем существует такой элемент а, что любой элемент х из А ему равен:
isContr(A) := Exists (a:A), (x:A) -> x ~~> a
т.е. для доказательства стягиваемости пространства А мы должны предъявить зависимую пару, где первый элемент - значение а из А, а второй - функция, которая для каждого х производит доказательство того, что х = а, конкретный путь из х в а. В частности, несложно показать, что тип unit стягиваемый. Стягиваемый тип обязан быть непустым, иначе мы не сможем предъявить а.
Эквивалентность пространств можно определять немного по-разному, есть альтернативные подходы. Например, если у нас есть функция f : A -> B и точка b в B, можно сначала определить homotopy fiber
hFiber(f,b) := Exists (a:A), f a ~~> b
Это тип пар, где первый элемент - значение из А, а второй - доказательство того, что f его отображает в значение, равное b. Фактически, это обратный образ для f в точке b. Утверждение, что функция f - это эквивалентность, это такой тип:
isEquiv(f) := (b : B) -> isContr( hFiber(f,b) )
Т.е. если для каждой точки b из B существует ее праобраз в А (относительно f). Очень похоже на биекцию, только равенства везде пропозициональные. Отдельно доказывается, что всякая функция-эквивалентность это изоморфизм и наоборот.
Ну а дальше мы говорим, что пространства (типы) А и В эквивалентны, если существует такая функция f для которой населен isEquiv(f). Эквивалентность пространств А и В будем обозначать А ~= B.
Теперь, мы можем рассмотреть пространство всех типов Type (не включая его самого, делаем стандартную иерархию вселенных а-ля Агда и подкапотный Идрис). Обычные типы, вроде Nat и (Int -> Int), будут его элементами. Тогда для двух элементов типа Type, для двух типов А и В, мы можем задуматься: а когда они равны? Утверждение о равенстве двух типов А и В будет типом
IdTypeA B
или в нашем новом обозначении A ~~> B. Это тип, т.е. тоже пространство, точки в котором - это доказательства равности А и В, пути в Type. Утверждение об эквивалентности простанств А и В, А ~= B, это тоже тип, тоже пространство. Мы можем построить конструктивно функцию
v(A,B) : (A ~~> B) -> (A ~= B)
которая логически означает, что из пропозиционального равенства двух типов следует их эквивалентность. При этом сама v - это функция из пространства (A ~~> B) в пространство (A ~= B). Что можно сказать об этих двух пространствах? Тут приходит Воеводский и говорит: давайте добавим одну аксиому, аксиому унивалентности:
univalence : {A, B : Type} -> isEquiv( v(A,B) )
т.е. постулируем, что такая v - это эквивалентность. Другими словами,
(A ~~> B) ~= (A ~= B)
пространство путей между двумя типами эквивалентно пространству эквивалентностей (и изоморфизмов) между этими типами. Бах!
Внезапно, наличие такой аксиомы сразу дает очень много плюшек и многое упрощает. В том числе из нее автоматом получается следствие
ndfe : {f,g : A -> B} -> (f ~ g) -> (f ~~> g)
- это наивная независимотиповая function extensionality; из гомотопии между f и g можно получить доказательство равности f и g. Возвращаясь ближе к началу поста, у нас были
f x = 2 * x
g x = x * 2
доказать равенство которых мы не могли. Мы можем построить гомотопию
H : (x : A) -> f x ~~> g x
которая для каждого x произведет доказательство того, что 2 * x = x * 2 (это банальное упражнение для агда-программистов), и теперь ndfe H нам даст значение типа f ~~> g, т.е. доказателство равности этих двух функций. В случае зависимых типов, доказывается, что из унивалентности также следует weak function extensionality:
wfe : ((x:A) -> isContr(P x)) -> isContr( (x:A) -> P x )
а еще ранее, безо всякой унивалентности, можно было показать, что из нее следует strong function extensionality:
sfe : (f,g : (x:A) -> P x) -> isEquiv( hApply(f,g) )
где
hApply : (f, g : (x:A) -> P x) -> (f ~~> g) -> (f ~ g)
т.е. для всяких зависимых функций из (х:А) в (Р х) пространство гомотопий между ними эквивалентно пространству путей между ними.
Вот так, добавив одну аксиому, можно сохранить интенсиональность теории типов, ее многомерную структуру и получить доказательство равности f x = 2 * x и g x = x * 2.
К слову о многомерности. В этой теории типы можно классифицировать по уровням. Чтобы было интересней, в классической гомотопической теории они нумеруются начиная с -2. Тип уровня -2 - это любой стягиваемый тип, например unit, он же () в хаскеле.
Тип уровня -1 - это h-prop, он характеризуется формулой A -> isContr(A): он стягиваем если населен. Его еще называют proof-irrelevant, любые два значения его пропозиционально равны, но в отличие от уровня -2 они могут и не существовать вовсе. Такой тип используется для записи многих логических утверждений.
Тип уровня 0 - это h-set, тип множеств. В таком типе может быть много разных значений, но любые доказательства равности его элементов сами между собой равны, т.е. справедлив принцип uniqueness of identity proofs. В ETT, экстенсиональной теории типов, все типы - это такие одномерные множества.
Тип уровня 1 - это группоид, в нем могут быть нетривиальные морфизмы, но все 2-морфизмы тривиальны. И т.д. Категорно, n-типы соответствуют n-группоидам.
Получаются такие типы обрезанием ∞-группоида, когда мы выбираем некоторый уровень n и объявляем все пути более высокого порядка равными.
Вот, как-то так обстоят дела с 2*9=9*2.