Adicionando Tipos de Refinamento ao Rust: Um Estudo de Viabilidade
Este artigo explora a viabilidade de adicionar tipos de refinamento à linguagem de programação Rust. Com base na experiência com o YAIOUOM, um analisador estático que utilizava tipos de refinamento para verificar unidades de medida, o autor examina abordagens para implementar tipos de refinamento dentro do sistema de tipos do Rust. Várias opções são propostas, incluindo modificações na resolução de traços, unificação de variáveis de tipo e a introdução de um mecanismo de palavra-chave plugável para verificação de tipos pós-compilação. Uma abordagem otimista — ignorando informações de unidade no início da compilação e verificando posteriormente — é considerada mais prática. O design da API e o tratamento de mensagens de erro são discutidos. O trabalho futuro envolve coletar feedback, escrever um driver rustc que suporte plug-ins e implementar vários tipos de refinamento, potencialmente incluindo uma nova versão do YAIOUOM e subconjuntos de Flux ou Liquid Haskell.