Problemy w systemie-typie Haskella

Question

Znalazłem kilka odpowiedzi (tutaj w języku SO), mówiących, że Haskell ma wiele "ciemnych kątów" w swoim typie systemu, a także pewne dziurawe dziury. Czy ktoś mógłby to rozwinąć?

góry dzięki

Answer 1

Chyba powinienem odpowiedzieć na to pytanie, zwłaszcza, że ​​dwie osoby tej pory błędnie zinterpretował moje uwagi ...

chodzi non-zakończenie, uwaga w kwestii był nieznaczny hiperbola dla dramatycznego efektu, i odniósł się do braku wypowiedzenia na poziomie o wartości. Było to w kontekście porównywania twierdzeń Haskella do z dowodami, w odpowiedzi na kogoś, kto wymienił wymuszone przez prawo właściwości poprawności jako coś, co szczególnie docenili. W tym sensie obecność ⊥ zamieszkujących w inny sposób pustych typów jest "wadą", ponieważ zmienia ona znaczenie typu, takiego jak A -> B z "dany A, tworzy B" na "dany A, albo tworzy B lub rozbija się program "z oczywistych względów nieco mniej satysfakcjonujący z punktu widzenia poprawności danych.

Jest również całkowicie nieistotny dla prawie wszystkich codziennych programów i nie gorszy niż jakikolwiek inny język ogólnego przeznaczenia, ponieważ, oczywiście, możliwość braku zakończenia jest wymagana dla Turinga-kompletności.

Nie mam żadnego problemu z UndecidableInstances. Właściwie to nurtuje mnie mniej niż ⊥ na poziomie wartości, ponieważ powoduje tylko awarię GHC podczas kompilacji, a nie gotowego programu. OverlappingInstances to już inna kwestia, a ad hoc mishmash rozszerzeń GHC, które dostarczają małych kawałków rzeczy, które najbardziej naturalnie wymagają określonych typów, z pewnością kwalifikuje się jako "niechlujny".

Pamiętaj jednak, że większość rzeczy, na które narzekam w Haskell, stanowi problem tylko z powodu bardzo solidnych podstaw. Większość systemów typów w innych statycznie napisanych językach nie jest nawet wystarczająco spójna, aby można je było nazwać "niewłaściwymi" w porównaniu z innymi, a oczyszczanie rzeczy, które nazywam "niechlujnymi", jest aktywnym i ciągłym obszarem badań.

Answer 2

Więc masz na myśli mówiąc Camccann „system typu Haskell jest pełna dziur, ze względu na nontermination i innych brudnych kompromisów”? Myślę, że mówi o rozszerzeniu UndecidableInstances i prawdopodobnie kilku innych.

Potem odniosłeś się do Normana, mogę tylko przypuszczać, mówiąc: "System typu Haskella jest ambitny i potężny, ale jest ciągle ulepszany, co oznacza, że ​​istnieje pewna niekonsekwencja w wyniku historii.". Jestem pewien, że miał coś na myśli, ale pozwoli mu to wyjaśnić, kiedy zobaczy to pytanie.

Answer 3

System typu Haskella nie ma żadnych problemów ani dziurawych dziur. Haskell 98 może być w pełni sformułowany. Posiada on tak zwaną właściwość "głównego typu", co oznacza, że ​​każde dane wyrażenie ma najwyżej jeden ogólny typ. Istnieje jednak szereg wyrażeń, które są dobre, użyteczne i poprawne, ale nie wpisują się w Haskell 98. Najważniejsze z nich to typy o wyższej randze. forall a b. (a -> b) -> a -> b to (nieinteresujący) przykład typu rank-jeden, który oznacza, że ​​forall jest tylko na zewnątrz. forall b. -> (forall a. a -> a) -> b -> b jest przykładem bezużytecznego, ale możliwego typu, który nie ma pozycji pierwszej i nie może być wyrażony w Haskell98. Wyższe typy w rankingu są jedną z wielu rzeczy, które przerywają główną właściwość typu.

Jako że dodaje się coraz więcej rozszerzeń do podstawowego systemu Haskell98, zaczynają się pojawiać kompromisy pomiędzy zdolnością do pisania naprawdę potężnych typów, które wyrażają zarówno różne rodzaje polimorfizmu i różne rodzaje ograniczeń, jak i możliwość posiadania tak dużej ilości możliwie jak najdokładniejszy kod. Na samym skraju tego, co możliwe, typy mogą stać się chaotyczne i skomplikowane, a czasami można wpaść na rzeczy, które wydają się działać, ale nie działają. Ale w tym momencie zazwyczaj robisz coś, co nazywa się "programowaniem na poziomie typu", w którym duża część twojej logiki aplikacji została wbudowana w same typy i poprzez kombinację trików typeclass, do których kompilator włączyłeś, zasadniczo, uruchamianie typów jako programu w czasie kompilacji.

Nie zgadzam się, przy okazji, z twierdzeniem Camccanna, że ​​potencjalna nieterminacja jest nieuporządkowanym kompromisem w sprawdzaniu typu. Myślę, że jest to bardzo przydatna funkcja, w rzeczywistości warunek wstępny - kompletność na poziomie typu i ryzykujesz tylko wtedy, gdy wyraźnie poprosisz kompilator, aby zaczął pozwalać na wiele podejrzanych rzeczy.