Przykład, w którym naruszenie ścisłego warunku dodatniego w typach indukcyjnych prowadzi do niespójności

Większość systemów typowanych zależnie ma ścisłe warunki dodatnie dla typów indukcyjnych. Czy ktoś zna przykład, w którym naruszenie warunku prowadzi do niespójności w systemie?

W rzeczywistości można rozluźnić ścisłą pozytywność i zachować spójność. Na przykład wystarczy mieć warunek dodatni. Oznacza to, że możemy zaakceptować takie definicje typów

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

gdzie zmienne typu rekurencyjnego występują po lewej stronie parzystej liczby strzałek i zachowują spójność.

Jednak teorie pozwalające na tego rodzaju indukcyjny typ nie mają modeli teoretycznych - nie można interpretować typów jako zbiorów, a terminów jako elementów zbiorów. W tym przypadku mówimy, że $T$ jest izomorficzny w stosunku do swojego podwójnego zestawu sił (tj. $T \simeq \mathcal{P}(\mathcal{P}(T))$ ), a to narusza twierdzenie Cantora .

Ponieważ teorie typów zależnych są często używane do sformalizowania matematyki, ich projektanci zwykle wahają się dodawać zasady, które nie są zgodne z semantyką teoretyczną, nawet jeśli są spójne.

EDYCJA: Dodam tę zmianę w odpowiedzi na pytanie Andreja. Typ jest spójny, jeśli dodasz go do (powiedzmy) Agdy; nie ma z tym żadnych problemów. Mamy problem tylko wtedy, gdy połączymy nie ścisłą pozytywność z wykluczonym środkiem.$T$

Intuicja, dlaczego jest bezpieczny, jest najlepiej widoczna przez soczewkę parametryczną (IMO). W Systemie F możemy pokazać za pomocą parametryczności, że dla dowolnego definiowalnego funktora , typ jest rzeczywiście typem indukcyjnym.$F$$\mu F \triangleq \forall \alpha.\; (F\alpha \to \alpha) \to \alpha$

Przypomnijmy teraz, że definiowalnym funktorem jest operator typu , wraz z operatorem spełniających warunki funkcjonalności (tj. i ).$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$

Teraz możemy zdefiniować operator typu dla podwójnego zestawu zasilającego

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

a ponieważ występuje tylko pozytywnie, możemy również zdefiniować dla niego operatora mapy:$\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))$$

Wiemy więc, że jest uzasadnionym typem indukcyjnym.$T = \mu C$