El compilador del lenguaje de programación Gleam utiliza un módulo interno llamado exhaustiveness.rs para garantizar que las expresiones case cubran todos los valores posibles de sus argumentos. Este mecanismo, que opera durante la compilación, evita que el programa falle en tiempo de ejecución por valores no manejados y proporciona al desarrollador un diagnóstico preciso de qué patrones faltan. El artículo analiza la base teórica de esta funcionalidad, rastreando sus raíces en los trabajos de Lennart Augustsson sobre la compilación de la correspondencia de patrones en 1984-1985. Augustsson propuso un marco que agrupa las cláusulas por constructores y introduce variables frescas para subpartes, un método que sentó las bases para la implementación actual. Además, el texto explora la influencia de Luc Maranget, quien en 2007 introdujo el concepto de 'witness' o contraejemplo para identificar casos inexhaustivos mediante matrices de constructores y cláusulas. Esta metodología permite al compilador determinar si existe un valor que nunca coincidirá con ninguna de las cláusulas presentadas. Gleam ha optimizado este proceso al integrar la verificación en tiempo de compilación, utilizando estructuras de datos estáticamente tipadas en lugar de reglas de tiempo de ejecución, lo que permite una detección más precisa y eficiente. Este enfoque refleja la evolución de los lenguajes funcionales desde los años 90, donde la ergonomía de los diagnósticos y la riqueza de los patrones se convirtieron en prioridades clave para la seguridad del software.
