Które języki badawcze mają silniejszy system typów niż Haskell i dlaczego?

Tutaj czytam:

Haskell zdecydowanie nie ma najbardziej zaawansowanego systemu czcionek (nawet bliskiego, jeśli liczyć języki badawcze), ale spośród wszystkich języków faktycznie używanych w produkcji Haskell jest prawdopodobnie na szczycie.

Pytam więc o dwie rzeczy:

które języki badawcze mają mocniejsze systemy typów niż Haskell;
co poprawiają.

Jestem tylko programistą, więc nie znam wielu obiektów matematycznych używanych w teorii typów, proszę podać łagodne wyjaśnienia, jeśli możesz.

programming-languages type-theory

— Виталий Олегович
źródło

Co lepsze"?

— David Richerby,

@DavidRicherby Wydaje mi się, że to oznacza mocniejszy system typów

— Виталий Олегович

Czy po udowodnieniu, że system typów jest kompletny w Turinga , czy to naprawdę ma znaczenie? ;-)

— DevSolar,

Maszyny Turing są kompletne, dlaczego nie wykorzystasz ich do codziennych zadań programistycznych?

— Gallais,

Należy zauważyć, że oryginalny tekst wspomina o językach z bardziej zaawansowanymi systemami typów i nie czyni żadnych twierdzeń, że „bardziej zaawansowane” jest lepsze lub gorsze dla systemu typów.

— Peteris,

Odpowiedzi:

Pytanie jest nieco problematyczne, ponieważ opiera się na subiektywnej definicji „lepszego”.

Języki pisane zależnie, takie jak Agda , Idris i Coq, mają silniejszy system pisma niż Haskell. Oznacza to, że możesz użyć typów w tych językach, aby udowodnić, że masz o wiele więcej właściwości swojego kodu niż w Haskell. Oznacza to, że zostanie złapanych więcej niepoprawnych programów.

Jest to jednak oparte na cenie: wnioskowanie o typ i sprawdzenie, czy istnieją jakieś wartości danego typu, nie są już możliwe. Oznacza to, że dla tych języków musisz jawnie adnotować swój kod typami. Zasadniczo sprowadza się to do napisania własnych dowodów poprawności kodu.

Czy te języki są „lepsze” niż Haskell? Mogą sprawdzać zaawansowane dowody poprawności kodu, ale nie mogą automatycznie udowodnić właściwości kodu w sposób, w jaki może to zrobić Haskell.

Innym językiem badawczym, który jest „lepszy” niż Haskell, jest LiquidHaskell . Zasadniczo jest to Haskell z typami wyrafinowania przykręconymi do góry, w oparciu o specjalne komentarze.

Typy zawężania pozwalają ci na udoskonalanie typów za pomocą właściwości. Na przykład zamiast mieć Int, możesz określić {i : Int | i > 0}, podając typ wszystkich dodatnich liczb całkowitych. Wnioskowanie o typach jest rozstrzygalne w przypadku typów doprecyzowania, ale nie można udowodnić za pomocą nich tak wielu właściwości poprawności, jak w przypadku typów zależnych.

Istnieją inne systemy typu wyrafinowania, ale nie znam się na żadnym z nich.

— jmite
źródło

Dziękuję Ci! Czy można udowodnić, że system typów Haskell jest najsilniejszy, który wciąż pozwala na wnioskowanie typu?

— Виталий Олегович

Haskell zdecydowanie NIE jest najsilniejszy, który pozwala na wnioskowanie typu. Wymienione typy udoskonaleń pozwalają na wnioskowanie o typie, a do Haskell dodaje się wiele rozszerzeń GHC, które pozwalają na nieco mocniejszy system typów.

— jmite

Ponadto istnieje wiele systemów typów, a wiele z nich jest nieporównywalnych: pod pewnymi względami będą silniejsze niż Haskell, ale pod innymi słabsze niż Haskell. Nie ma liniowego uporządkowania systemów typów od najsilniejszych do najsłabszych.

— jmite

Teraz chcę udowodnić, że nie ma najsilniejszego systemu typów, który pozwalałby na wnioskowanie typu. Musi się oprzeć udowodnieniu bezużytecznych faktów.

— Andrej Bauer,

Ten fakt nie wydaje mi się bezużyteczny. Wiedza, że istnieje najsilniejszy system typów z wnioskowaniem typu, byłaby bardzo interesująca, szczególnie jeśli okazałaby się możliwa do wdrożenia.

— rationalis

Rodzina języków ML (StandardML, OCaml ) wywodzi się z podobnej tradycji jak Haskell i dlatego mają podobne systemy typów. Nie są one jednak dokładnie takie same jak Haskell, a niektóre ich funkcje mogą ci bardziej odpowiadać (nie ma czegoś takiego jak obiektywnie lepszy system pisma , ponieważ istnieją systemy pisma w językach programowania, które pomagają ludziom ). Oto niektóre cechy OCaml, których Haskell albo nie ma (ale może mieć podobną podobną koncepcję), albo Haskell ma, ale działa inaczej:

Warianty polimorficzne .
Obiekty z podtypami głębi i klasami .
Functors , czyli mapy między modułami (Haskell ma moduły), a nawet moduły pierwszej klasy

I proszę, nie ma potrzeby przekształcania tego w strzelaninę ML-Haskell, inaczej zacznę link do postów na blogu Boba Harpera ;-)

— Andrej Bauer
źródło

Język badawczy Clean ma lepszy system typów niż Haskell, ponieważ ma typy unikatowości . Idee typów wyjątkowości są ściśle związane z logiką liniową , która jest bliższa ograniczonemu do zasobów „światowi rzeczywistemu” niż logika klasyczna.

Język anty-badawczy Rust ma również system pisma z unikalnymi cechami, które są bliższe „rzeczywistemu światu” niż klasyczne systemy pisma czystego. Większość pomysłów, które wpłynęły na system typów, opublikowano całkowicie niezależnie od Rust na długo przed jego istnieniem. Ale sposób połączenia tych starych pomysłów jest wyjątkowy i zasługiwałby również na prawdziwe publikacje badawcze, nawet jeśli istnieją znane luki i niespójności.

— Thomas Klimpel
źródło

Jakoś „opublikowane” i „anty-badania” nie idą w parze.

— Andrej Bauer,

Unikalność jest z pewnością interesującą koncepcją, ale IMO bardziej dotyczy semantyki niż funkcji systemu typów jako takiej. Czy to naprawdę sprawia, że system typów jest zdecydowanie lepszy ? Czy Clean może zrobić nowe rzeczy, które Haskell dodał do swojego systemu typów, polimorfizmu wyższego rzędu itp. - czy niektóre z nich są nawet możliwe, gdy system typów musi już poradzić sobie z wyjątkowością?

— leftaroundabout

@leftaroundabout Jak dobrze znasz typy wyjątkowości lub logikę liniową? Jeśli x ma unikalny typ, to na przykład f (x, x) nie jest dobrze wpisane. Możliwe jest rozszerzenie programu Haskell o obsługę typów unikatowości. Semantyka przenoszenia w C ++ może być również postrzegana jako poprawa obsługi typów uniquencess na istniejącym systemie typów.

— Thomas Klimpel,

Znam semantykę ruchów w C ++, być może dlatego mam wrażenie, że wyjątkowość jest „czymś w rodzaju systemu typów”. Interesujące jest dla mnie to, czy w pełni propagowane na zewnątrz typy unikatowości utrudniają inne funkcje zaawansowanego systemu typów?

— leftaroundabout

@leftaroundabout Odniesienia do wartości brzmią dla mnie jak system typowy. Dlaczego typy unikatowości powinny utrudniać inne zaawansowane funkcje typów? W najgorszym przypadku te zaawansowane funkcje po prostu nie miałyby zastosowania do typów wyjątkowości. Oczywiście funkcje „świata rzeczywistego”, takie jak typy wyjątkowości, oznaczają poszerzanie się zamiast głębokości, a czas poświęcony na poszerzenie nie będzie już potrzebny na głębsze. Mam jednak wrażenie, że typy wyjątkowości zapewniają dobrą równowagę między teorią a praktyką, więc myślę, że czas byłby dobrze spędzony.

— Thomas Klimpel,