Co sprawia, że ​​wnioskowanie o typach dla typów zależnych jest nierozstrzygalne?

Widziałem już wspomniane, że systemy typów zależnych nie są wnioskami, ale można je sprawdzić. Zastanawiałem się, czy istnieje proste wyjaśnienie, dlaczego tak jest, i czy istnieje granica „zależności”, w której typy mogą być indeksowane według wartości, poniżej której możliwe jest wnioskowanie typu, a powyżej której nie jest?

W przypadku dość prostej wersji teorii typów zależnych Gilles Dowek przedstawił dowód nierozstrzygalności typowania w niepustym kontekście:

Gilles Dowek, Nierozstrzygalność typowania w -calculus$\lambda\Pi$

Które można znaleźć tutaj .

Najpierw wyjaśnię, co zostało udowodnione w tym artykule: pokazuje on, że w rachunku zależnym bez adnotacji o abstrakcjach nierozstrzygalne jest wykazanie typowalności terminu w niepustym kontekście . Obie te hipotezy są konieczne: w pustym kontekście maszynowość ogranicza się do zwykłego -calculus (rozstrzyganego przez Hindleya-Milnera), a przy adnotacjach na abstrakcjach stosuje się zwykły algorytm ukierunkowany na typ.$\lambda$

Chodzi o to, aby zakodować problem korespondencji jako problem konwersji typu, a następnie ostrożnie skonstruować termin, który można wpisać, jeśli dwa konkretne typy są konwertowalne. Wykorzystuje to wiedzę o kształcie normalnych form, które zawsze istnieją w tym rachunku różniczkowym. Artykuł jest krótki i dobrze napisany, więc nie będę się tutaj zagłębiał w szczegóły.

Teraz w obliczeniach polimorficznych, takich jak system-F, byłoby fajnie móc wnioskować o abstrakcjach typów i aplikacjach oraz pomijać adnotacje na jak wyżej. Jest to również nierozstrzygalne, ale dowód jest znacznie trudniejszy, a pytanie było otwarte od dłuższego czasu. Sprawa została rozwiązana przez Wellsa:$\lambda$

JB Wells, typowość i kontrola typu w systemie F są równoważne i nierozstrzygalne .

Można to znaleźć tutaj . Wiem tylko, że redukuje problem półjednolitości (czyli instancji modulo unifikacji uniwersalnych kwantyfikatorów i jest nierozstrzygalny) do sprawdzania typu w Systemie F.

Wreszcie dość łatwo jest wykazać, że zamieszkanie zależnych rodzin jest nierozstrzygalne: wystarczy zakodować problem Post w indeksach konstruktora. Oto kilka slajdów Nicolasa Oury'ego, które szkicują argument.

Jeśli chodzi o to, czy istnieje „limit”, wiele zależy od tego, co próbujesz zrobić ze swoimi typami zależnymi, i istnieje wiele przybliżeń, które próbują być rozstrzygalne lub przynajmniej na tyle bliskie, aby były użyteczne. Te pytania są jednak nadal częścią aktywnych badań.

Jedną z możliwych możliwości jest pole „typów doprecyzowania”, w którym język wyrażania zależności między typami jest ograniczony, aby umożliwić decydujące sprawdzenie, patrz np . Typy płynów . Rzadko zdarza się jednak, że wnioskowanie o pełnym typie jest rozstrzygalne nawet w tych systemach.