Total (fonctionnelle) de la langue est celui dans lequel tout peut être montré à la fin. De toute évidence, il ya beaucoup d'endroits où je ne veux pas ce lancer des exceptions est parfois à portée de main, un serveur web n'est pas censé pour terminer, etc. Mais parfois, j'aimerais un local totalité cochez la case pour activer certaines optimisations. Par exemple, si j'ai un prouvable-total fonction
commutativity :: forall (n :: Nat) (m :: Nat). n + m :~: m + n
commutativity = ...
ensuite, depuis :~:
a exactement un habitant (Refl
), GHC pourrait optimiser
gcastWith (commutativity @n @m) someExpression
==>
someExpression
Et ma preuve de commutativité va avoir un O(n)
d'exécution coût pour être libre. Alors, maintenant, pour ma question:
Quelles sont les difficultés subtiles dans la réalisation d'un ensemble checker pour Haskell?
Bien évidemment, une telle checker est conservateur et donc à chaque fois GHC n'est pas sûr que quelque chose est totale (ou la flemme de vérifier). on pourrait supposer qu'il ne l'est pas... me Semble qu'il pourrait ne pas être trop difficile de bricoler un pas intelligents vérificateur qui serait encore être très utile (au moins il devrait être très simple pour éliminer tous mes arithmétique des épreuves). Pourtant, je n'arrive pas à trouver tous les efforts pour construire une telle chose dans GHC, donc évidemment, je suis en manque de quelques très grandes contraintes. Allez-y ALORS, écraser mes rêves. :)
Pertinent, mais pas récente: sans faille Haskell par Neil Mitchell, 2005.