Пример, когда нарушение условия строгой положительности в индуктивных типах приводит к несогласованности

Большинство зависимых типизированных систем имеют строгие условия положительности для индуктивных типов. Кто-нибудь знает пример, когда нарушение условия приводит к несогласованности в системе?

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

$$T \triangleq \mu\alpha. (\alpha \to 2) \to 2$$

где переменные рекурсивного типа встречаются слева от четного числа стрелок и сохраняют согласованность.

Однако теории, допускающие такого рода индуктивный тип, не имеют теоретико-множественных моделей - вы не можете интерпретировать типы как множества, а термины как элементы множеств. В этом случае мы говорим, что изоморфно своему двойному множеству (т. Е. ), и это нарушает теорему Кантора .$T$$T \simeq \mathcal{P}(\mathcal{P}(T))$

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

РЕДАКТИРОВАТЬ: я добавляю это изменение в ответ на вопрос Андрея. Тип непротиворечив, если вы добавите его в (скажем) Agda; проблем с этим нет вообще. У нас проблема только в том случае, если мы объединяем нестрогую положительность с исключенным средним.$T$

Интуиция о том, почему это безопасно, (ИМО) лучше всего видна сквозь призму параметричности. В Системе F мы можем показать с помощью параметричности, что для любого определяемого функтора тип действительно индуктивный тип.$F$$\mu F \triangleq \forall \alpha.\; (F\alpha \to \alpha) \to \alpha$

Теперь напомним, что определяемый функтор является оператором типа вместе с оператором удовлетворяющие условиям функториальности (т. е. и ).$F$$F : \ast \to \ast$

$$\mathrm{map} : \forall \alpha,\beta.\;(\alpha \to \beta) \to F\;\alpha \to F\;\beta$$ $\mathrm{map}\;id = id$$\mathrm{map}\;f\;\circ \mathrm{map}\;g = \mathrm{map}\;(f \circ g$

Теперь мы можем определить оператор типа для двойного powerset

$$C = \lambda \alpha.\; (\alpha \to 2) \to 2$$

и поскольку встречается только положительно, мы также можем определить для нее оператор карты:$\alpha$

$$map_C = \lambda f : \alpha \to \beta, a' : (\alpha \to 2) \to 2, k : \beta \to 2.\; a' \;(\lambda a:\alpha.\; k\;(f\;a))$$

Итак, мы знаем, что является законным индуктивным типом.$T = \mu C$