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 .)
haskell
abstraction
type-systems
lambda
Petr Pudlák
źródło
źródło
Odpowiedzi:
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ł.
źródło