Dlaczego Haskell nie ma abstrakcji lambda na poziomie typu?

Czy istnieją jakieś teoretyczne powody (na przykład, że sprawdzanie typu lub wnioskowanie o typach stałyby się nierozstrzygalne), lub praktyczne (zbyt trudne do prawidłowego wdrożenia)?

Obecnie możemy owijać w coś newtypepodobnego

newtype Pair a = Pair (a, a)

a następnie mieć Pair :: * -> *

ale nie możemy zrobić czegoś takiego λ(a:*). (a,a).

(Istnieje kilka języków, które je mają, na przykład Scala ma .)

— Petr Pudlák
źródło

Wybór jednego rodzaju systemu typów do użycia wyklucza inny rodzaj systemów typów, ponieważ całość musi być spójna. Poziom lambda na poziomie typu byłby bardzo dziwny w teorii kategorii ...

— tp1

stackoverflow.com/questions/4922560/... jest również powiązany.

— Edward Z. Yang

Wnioskowanie typu na podstawie lambda na poziomie typu wymagałoby unifikacji wyższego rzędu, co jest nierozstrzygalne. Jest to motywacja do ich niedopuszczenia. Ale podobnie jak w przypadku innych nierozstrzygalnych funkcji (takich jak wnioskowanie o typie dla GADT), może być możliwe wymaganie podpisów typów i zezwolenie na to. Nie jestem pewien, czy ktoś to zbadał.

— sierpień
źródło