Gibt es einige theoretische Gründe dafür (wie dass die Typprüfung oder die Typinferenz unentscheidbar werden würde) oder praktische Gründe (zu schwierig, richtig zu implementieren)?
Gegenwärtig können wir Dinge in newtypeÄhnliches
verpacken
newtype Pair a = Pair (a, a)
und dann haben Pair :: * -> *
aber wir können sowas nicht machen λ(a:*). (a,a).
(Es gibt einige Sprachen, in denen sie vorkommen, zum Beispiel Scala .)
haskell
abstraction
type-systems
lambda
Petr Pudlák
quelle
quelle
Antworten:
Eine Typinferenz mit Lambdas auf Typebene würde eine Vereinheitlichung höherer Ordnung erfordern, die nicht zu entscheiden ist. Dies ist die Motivation, sie nicht zuzulassen. Aber wie bei anderen unentscheidbaren Funktionen (wie der Typinferenz für GADTs) kann es möglich sein, Typensignaturen anzufordern und diese zuzulassen. Ich bin mir nicht sicher, ob das jemand untersucht hat.
quelle