В теории типов тип тождества представляет собой концепцию равенства . Он также известен как пропозициональное равенство , чтобы отличать его от «судебного равенства». Равенство в теории типов является сложной темой и было предметом исследований, таких как область теории гомотопических типов . [1]
Тип идентичности — одно из двух различных понятий равенства в теории типов. [2] Более фундаментальным понятием является «равенство суждений», которое представляет собой суждение .
Тип тождества может делать больше, чем то, что может делать оценочное равенство. Его можно использовать для демонстрации "для всех ", что невозможно показать с оценочным равенством. Это достигается с помощью элиминатора (или "рекурсора") натуральных чисел, известного как "R".
Функция "R" позволяет нам определить новую функцию для натуральных чисел. Эта новая функция "P" определяется как "(λ x:nat . x+1 = 1+x)". Другие аргументы действуют как части доказательства индукции. Аргумент "PZ : P 0" становится базовым случаем "0+1 = 1+0", который является термином "refl nat 1". Аргумент "PS : P n → P (S n)" становится индуктивным случаем. По сути, это говорит о том, что когда "x+1 = 1+x" заменяет "x" каноническим значением, выражение будет таким же, как "refl nat (x+1)".
Тип идентичности сложен и является предметом исследования в теории типов. Хотя каждая версия соглашается с конструктором, "refl". Их свойства и функции элиминатора существенно различаются.
Для "экстенсиональных" версий любой тип идентичности может быть преобразован в оценочное равенство. Вычислительная версия известна как "Аксиома K" благодаря Томасу Штрайхеру. [3] Они не очень популярны в последнее время.
Мартин Хоффман и Томас Штрайхер опровергли утверждение, что теория типа идеи требует, чтобы все термины типа идентичности были одинаковыми. [4]
Популярными направлениями исследований типа тождества являются теория гомотопических типов [5] и ее теория кубического типа.
