Y a-t-il des raisons théoriques à cela (comme que la vérification de type ou l'inférence de type deviendrait indécidable) ou des raisons pratiques (trop difficiles à mettre en œuvre correctement)?
Actuellement, nous pouvons envelopper des choses newtypecomme
newtype Pair a = Pair (a, a)
puis avoir Pair :: * -> *
mais nous ne pouvons pas faire quelque chose comme ça λ(a:*). (a,a).
(Il existe certaines langues qui en ont, par exemple Scala .)
haskell
abstraction
type-systems
lambda
Petr Pudlák
la source
la source
Réponses:
L'inférence de type avec des lambdas de niveau type nécessiterait une unification d'ordre supérieur, ce qui est indécidable. C'est la motivation pour les interdire. Mais comme cela s'est produit avec d'autres fonctionnalités indécidables (comme l'inférence de type pour les GADT), il pourrait être possible d'exiger des signatures de type et de l'autoriser. Je ne sais pas si cela a fait l'objet d'une enquête par qui que ce soit.
la source