Istnieje niedawna praca Paula-André Mellièsa i Noama Zeilbergera, która bada to. W szczególności artykuły Functors to Type Refinement Systems i An Isbell Duality Theorem for Type Refinement Systems . Jest też wideo z rozmowy na temat pierwszego.
Myślę, że istnieje wiele nieporozumień wokół typów udoskonalania, ponieważ ludzie myślą o konkretnych systemach jako reprezentatywnych, co powoduje, że cele i szczegóły tych konkretnych systemów przypisuje się ogólnej idei. Krótko mówiąc, systemy doprecyzowujące typy klasyfikują terminy, które istnieją niezależnie, podczas gdy typy (niedokładne), zależne lub inne, są częścią terminów. Może to zabrzmieć znajomo, a może nawet trochę sprzecznie.
Potencjalnie znajoma i prawdopodobnie sprzeczna z pozoru część powstaje, jeśli spojrzysz na typy à la Curry (zewnętrznie) i typy à la Church (wewnętrznie). Kiedy myślimy o typach à la Curry, myślimy o typach jako o klasyfikacjach nietypowych terminów, które już mają znaczenie. W typach à la Church jedynymi istniejącymi terminami są dobrze napisane, tzn. Ograniczenia typowe są częścią naszej składni. Mówię więc, że system typu Curry jest w rzeczywistości systemem dopracowywania typów, dopracowującym nietypowe terminy, podczas gdy system typu kościelnego nie jest systemem dopracowywania typów. Oznacza to, że na przykład możemy myśleć o prostym typie rachunku lambda jako o systemie doprecyzowania typu lub o systemie niedokładania typu.
Oczywiście nikt nie mówi, że nasze warunki muszą być terminami bez typu. Równie dobrze moglibyśmy zastosować system dopracowywania typów do wpisywanych terminów, i historycznie jest to kontekst, w którym powstały typy doprecyzowania (o tej nazwie). Jednak aplikacje do pisania miękkiego ilustrują coś bliższego opisanej powyżej sytuacji.
Jak dotąd nie mówiłem nic o typach zależnych. Powodem jest to, że jest to kwestia całkowicie ortogonalna. Powiedziałbym, że archetypowe systemy typów zależnych są zwykle przedstawiane w stylu kościelnym, a zatem nie są to systemy doprecyzowania typów, ale NuPRL (oparty na obliczeniowej teorii typów , wariant najbardziej archetypowej teorii typów zależnych, teoria typów Martina-Löfa) jest rażąco typem systemu dopracowania typu, jak opisałem. Warunki w NuPRL mogą nawet nie mieć typów! Trzeba przyznać, że fakt, że „PRL” oznacza „logikę udoskonalania programu”, może być również wskazówką. Z drugiej strony, typy uściślenia dla ML opisują system typów uściślenia, być może pochodzenie terminu, który w żaden sposób nie jest systemem typów zależnych.
Jeśli chodzi o tróje Hoare, są to systemy dopracowania typu. Są one faktycznie używane jako przykład systemu doprecyzowania typu w pierwszym artykule. Jednak Hoare Rodzaj Teoria daje coś, co może być postrzegane jako system typu non-wyrafinowanie dla języka mającego trójek Hoare.
Aby uzyskać odpowiedź na temat „mocy” różnych systemów, musisz określić konkretny (typ) zależny (-e) system (-y) typowy (-ych) i szczególny (rodzina) system (-y) typu uściślenia. Termin „system typów zależnych” obejmuje bardzo szeroką klasę systemów typów, a „systemy udoskonalania typów” są jeszcze szersze. Nawet wtedy terminy nie wykluczają się wzajemnie, więc nie byłoby porównania między „systemami typów zależnych” i „systemami typów doprecyzowania”. Jeśli jednak przez „system typów zależnych” myślisz o czymś takim jak Coq , a o „systemie typów wyrafinowanych” coś takiego jak typy płynneto jest dość jednostronne. Coq jest ogólnie postrzegany jako wystarczająco silny, aby poradzić sobie praktycznie z całą matematyką w praktyce; możesz dosłownie zaimplementować i udowodnić poprawność solvera SMT w Coq, a następnie użyć go; i można sformułować bardzo podobny analog do typu podzbioru. (NuPRL ma dosłownie typy podzbiorów.) Z drugiej strony solwery SMT są zwykle ograniczone do rozstrzygalnych teorii, w których Coq nie ma takich ograniczeń; a wiele systemów, takich jak typy płynów, ma ograniczony i nierozszerzalny język do określania predykatów. (Oczywiście przez „zależny system typów” można rozumieć zależny ML , a przez „system udoskonalania typu” NuPRL [który jest także zależnym systemem typów], który byłby jednostronny w inny sposób.)