Ajouter des types de raffinement à Rust : une étude de faisabilité
Cet article explore la faisabilité d'ajouter des types de raffinement au langage de programmation Rust. S'appuyant sur l'expérience avec YAIOUOM, un analyseur statique utilisant des types de raffinement pour vérifier les unités de mesure, l'auteur examine les approches pour implémenter des types de raffinement au sein du système de types de Rust. Plusieurs options sont proposées, notamment des modifications de la résolution de traits, l'unification des variables de type et l'introduction d'un mécanisme de mot-clé branchable pour la vérification de types post-compilation. Une approche optimiste — ignorant les informations sur les unités en début de compilation et vérifiant plus tard — est jugée plus pratique. La conception de l'API et la gestion des messages d'erreur sont discutées. Les travaux futurs comprennent la collecte de commentaires, l'écriture d'un pilote rustc prenant en charge les plugins et l'implémentation de plusieurs types de raffinement, potentiellement incluant une nouvelle version de YAIOUOM et des sous-ensembles de Flux ou Liquid Haskell.