En la teoría de tipos , un tipo de refinamiento [1] [2] [3] es un tipo dotado de un predicado que se supone que es válido para cualquier elemento del tipo refinado. Los tipos de refinamiento pueden expresar condiciones previas cuando se usan como argumentos de función o condiciones posteriores cuando se usan como tipos de retorno : por ejemplo, el tipo de una función que acepta números naturales y devuelve números naturales mayores que 5 puede escribirse como. Por tanto, los tipos de refinamiento están relacionados con la subtipificación conductual .
Historia
El concepto de tipos de refinamiento se introdujo por primera vez en los tipos de refinamiento de 1991 de Freeman y Pfenning para ML , [1] que presenta un sistema de tipos para un subconjunto de NM estándar . El sistema de tipos "preserva la capacidad de decisión de la inferencia de tipos de ML" al mismo tiempo que "permite que se detecten más errores en tiempo de compilación". En tiempos más recientes, se han desarrollado sistemas de tipos de refinamiento para lenguajes como Haskell , [4] [5] TypeScript [6] y Scala .
Ver también
Referencias
- ^ a b Freeman, T .; Pfenning, F. (1991). "Tipos de refinamiento para ML" (PDF) . Actas de la Conferencia ACM sobre diseño e implementación de lenguajes de programación . págs. 268-277. doi : 10.1145 / 113445.113468 .
- ^ Hayashi, S. (1993). "Lógica de tipos de refinamiento". Actas del Taller sobre Tipos de Pruebas y Programas . págs. 157-172. CiteSeerX 10.1.1.38.6346 . doi : 10.1007 / 3-540-58085-9_74 .
- ^ Denney, E. (1998). "Tipos de refinamiento para especificación". Actas de la Conferencia Internacional IFIP sobre Conceptos y Métodos de Programación . 125 . Chapman y Hall. págs. 148-166. CiteSeerX 10.1.1.22.4988 .
- ^ Vazou, Niki. Haskell líquido: tipos de refinamiento para Haskell . El 45 ° Simposio ACM SIGPLAN sobre principios de lenguajes de programación (POPL 2018).
- ^ Volkov, Nikita (2015). "Tipos de refinamiento como una biblioteca Haskell" .
- ^ Panagiotis, Vekris; Cosman, Benjamin; Jhala, Ranjit (2016). "Tipos de refinamiento para TypeScript". Actas de la 37ª Conferencia ACM SIGPLAN sobre diseño e implementación de lenguajes de programación . págs. 310-325. arXiv : 1604.02480 . doi : 10.1145 / 2908080.2908110 .