Тип фактора
В области теории типов в информатике — факторный тип это тип данных , который учитывает определяемое пользователем отношение равенства . Фактортип определяет отношение эквивалентности на элементах типа — например, можно сказать, что два значения типа Person эквивалентны, если имеют одинаковое имя; формально p1 == p2 если p1.name == p2.name. В теориях типов, которые допускают фактортипы, выдвигается дополнительное требование, согласно которому все операции должны соблюдать эквивалентность между элементами. Например, если f — это функция значений типа Person, должно быть так, что для двоих Personс p1 и p2, если p1 == p2 затем f(p1) == f(p2).
Факторные типы являются частью общего класса типов, известного как алгебраические типы данных . В начале 1980-х годов фактор-типы были определены и реализованы как часть Nuprl помощника по доказательству в работе под руководством Роберта Л. Констебла и других. [1] [2] Фактортипы изучались в контексте теории типов Мартина-Лёфа . [3] теория зависимых типов , [4] логика высшего порядка , [5] и теория гомотопических типов . [6]
Определение
[ редактировать ]Чтобы определить факторный тип, обычно предоставляют тип данных вместе с отношением эквивалентности для этого типа, например: Person // ==, где == это определяемое пользователем отношение равенства. Элементы фактор-типа являются классами эквивалентности элементов исходного типа. [3]
Типы частных можно использовать для определения модульной арифметики . Например, если Integer это тип данных целых чисел, можно определить, сказав, что если разница четный. Затем мы формируем тип целых чисел по модулю 2: [1]
Integer //
Действия над целыми числами, +, - можно доказать, что они корректно определены для нового фактор-типа.
Вариации
[ редактировать ]В теориях типов, в которых отсутствуют фактортипы, сетоиды вместо фактортипов часто используются (множества, явно снабженные отношением эквивалентности). Однако, в отличие от сетоидов, многие теории типов могут требовать формального доказательства того, что любые функции, определенные для фактортипов, корректно определены . [7]
Характеристики
[ редактировать ]Факторные типы являются частью общего класса типов, известного как алгебраические типы данных . Подобно тому, как типы продукта и типы суммы аналогичны декартову произведению и несвязному объединению абстрактных алгебраических структур, фактор-типы отражают концепцию теоретико- множественных факторов , множеств, элементы которых разделены на классы эквивалентности заданным отношением эквивалентности на множестве. Алгебраические структуры, базовым набором которых является частное, также называются факторами. Примеры таких факторструктур включают фактормножества , группы , кольца , категории и , в топологии, факторпространства . [3]
Ссылки
[ редактировать ]- ^ Jump up to: Перейти обратно: а б Констебль, Роберт Л. (1986). Реализация математики с помощью системы разработки доказательств Nuprl . Прентис-Холл. ISBN 978-0-13-451832-9 .
- ^ Констебль, РЛ (1984). «Математика как программирование» . В Кларке, Эдмунд; Козен, Декстер (ред.). Логика программ . Конспекты лекций по информатике. Том. 164. Берлин, Гейдельберг: Шпрингер. стр. 116–128. дои : 10.1007/3-540-12896-4_359 . hdl : 1813/6405 . ISBN 978-3-540-38775-6 .
- ^ Jump up to: Перейти обратно: а б с Ли, Нуо (15 июля 2015 г.). «Фактортипы в теории типов» . eprints.nottingham.ac.uk . Проверено 13 сентября 2023 г.
- ^ Хофманн, Мартин (1995). «Простая модель для фактортипов» . Типизированные лямбда-исчисления и приложения . Конспекты лекций по информатике. Том. 902. Берлин, Гейдельберг: Springer. стр. 216–234. дои : 10.1007/BFb0014055 . ISBN 978-3-540-49178-1 .
- ^ Хомейер, Питер В. (2005). «Структура расчета для коэффициентов высшего порядка» . В Херде, Джо; Мелхэм, Том (ред.). Доказательство теорем в логике высшего порядка . Конспекты лекций по информатике. Том. 3603. Берлин, Гейдельберг: Springer. стр. 130–146. дои : 10.1007/11541868_9 . ISBN 978-3-540-31820-0 .
- ^ «Книга ХоТТ» . Гомотопическая теория типов . 12 марта 2013 г. Проверено 13 сентября 2023 г.
- ^ Хофманн, Мартин (1997). «Расширенные конструкции в теории интенсиональных типов» . СпрингерЛинк . дои : 10.1007/978-1-4471-0963-1 . ISBN 978-1-4471-1243-3 .