Почему бесконечная иерархия типов?

18

Coq, Agda и Idris имеют бесконечную иерархию типов (Тип 1: Тип 2: Тип 3: ...). Но почему бы не сделать это, как λC, систему в лямбда-кубе, которая ближе всего к исчислению конструкций и имеет только два , * и , и эти правила?

:

ΓT1:s1Γ,x:T1t:T2Γ(λx:T1,t):(Πx:T1,T2)

ΓT1:s1Γ,Икс:T1T2:s2Γ(ΠИкс:T1,T2):s2

Это кажется проще. Есть ли у этой системы важные ограничения?

Руи Баптиста
источник

Ответы:

19

На самом деле, подход CoC более выразителен - он допускает произвольную непредсказуемую количественную оценку. Например, тип a,aaМожно создать экземпляр a \ to a для себя (a,aa)(a,aa) , что невозможно при иерархии юниверсов.

Причина, по которой он не используется широко, заключается в том, что непредсказуемое количественное определение несовместимо с классической логикой. Если у вас это есть, вы не можете дать модель теории типов, в которой типы интерпретируются как множества наивным способом - см. Знаменитую статью Джона Рейнольдса « Неимметричный по множеству» .

Поскольку многие люди хотят использовать теорию типов как способ проверки обычных математических доказательств, они, как правило, не испытывают энтузиазма по поводу теоретико-типичных особенностей, которые несовместимы с обычными основами. На самом деле, Coq изначально поддерживала непредсказуемость, но они неуклонно отказывались от нее.

Нил Кришнасвами
источник
9

Я дополню ответ Нила (как обычно, отлично) более подробным изложением того, почему уровни используются на практике.

Первое важное ограничение CoC состоит в том, что это тривиально! Удивительное наблюдение состоит в том, что нет типа, для которого вы можете доказать, что он имеет более одного элемента, а тем более бесконечное их число. Добавление всего 2 вселенных дает вам натуральные числа с доказуемо бесконечным количеством элементов и всеми «простыми» типами данных.

Второе ограничение - это правила вычислений: CoC поддерживает только итерацию , т. Е. Рекурсивные функции не имеют доступа к подусловиям своих аргументов. По этой причине удобнее добавлять индуктивные типы в качестве примитивной конструкции, порождая CIC. Но теперь возникает другая проблема: наиболее естественное правило индукции ( в данном контексте называемое исключением ) несовместимо с Исключенным Средним! Эти проблемы не появляются, если вы ограничиваете правило индукции предикативными типами с юниверсами.

В заключение представляется, что CoC не обладает ни выразительностью, ни надежностью по сравнению с последовательностью, которую вы хотели бы видеть в основополагающей системе. Добавление вселенных решает многие из этих проблем.

Коди
источник
У вас есть ссылки на первое ограничение? Если нет, не могли бы вы дать подсказки о том, как вторая вселенная помогает доказать (пропозициональное? Мета?) Неравенство?
Лукаш Лью
@ ŁukaszLew Это на самом деле простое следствие «не относящейся к доказательству» модели, которую можно легко найти. В этой модели ни один тип не имеет более 1 элемента. Наличие 2 вселенных предотвращает существование этой модели. Тезис Александра Микеля дает ссылку на тип с бесконечным числом элементов с двумя вселенными.
Коди