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:

1. które języki badawcze mają mocniejsze systemy typów niż Haskell;
2. 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.

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.

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:

1. Warianty polimorficzne .
2. Obiekty z podtypami głębi i klasami .
3. 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 ;-)

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.