Hay trabajos recientes de Paul-André Melliès y Noam Zeilberger que exploran esto. En particular, los documentos Functors son Sistemas de refinamiento de tipo y un teorema de dualidad de Isbell para sistemas de refinamiento de tipo . También hay un video de una charla sobre el primero.
Creo que hay mucha confusión sobre los tipos de refinamiento debido a que las personas piensan que los sistemas particulares son representativos, lo que hace que los objetivos y detalles de esos sistemas particulares se atribuyan a la idea general. En resumen, los sistemas de refinamiento de tipos clasifican los términos que existen independientemente, mientras que los tipos (sin refinamiento), dependientes o no, son parte de los términos. Esto puede sonar familiar y posiblemente incluso un poco contradictorio.
La parte aparente potencialmente familiar y posiblemente contradictoria se produce si ve tipos à la Curry (extrínsecamente) versus tipos à la Church (intrínsecamente). Cuando pensamos en los tipos à la Curry, pensamos en los tipos como clasificar términos sin tipo que ya tienen significado. En los tipos a la Iglesia, los únicos términos que existen son términos bien escritos, es decir, las restricciones de tipo son parte de nuestra sintaxis. Entonces, lo que digo es que un sistema de tipo de estilo Curry es en realidad un sistema de refinamiento de tipo que refina términos sin tipo, mientras que un sistema de tipo de Iglesia no es un sistema de refinamiento de tipo. Esto significa que, por ejemplo, podemos pensar en el cálculo lambda simplemente tipado como un sistema de refinamiento de tipo o como un sistema de tipo de no refinamiento.
Por supuesto, nadie dice que nuestros términos tienen que ser términos sin tipo. También podríamos aplicar un sistema de refinamiento de tipos a los términos escritos e, históricamente, este es el contexto en el que surgieron los tipos de refinamiento (con ese nombre). Sin embargo, las aplicaciones de tipeo suave ilustran algo más cercano a la situación descrita anteriormente.
Hasta ahora no he dicho nada sobre los tipos dependientes. La razón es que es una preocupación completamente ortogonal. Yo diría que los sistemas de tipos dependientes arquetípicos generalmente se presentan en un estilo de la Iglesia, y por lo tanto no son sistemas de refinamiento de tipos, sino NuPRL (basado en la teoría de tipos computacional , una variante de la teoría de tipos dependiente más arquetípica, la teoría de tipos de Martin-Löf) es descaradamente un sistema de refinamiento de tipo como lo he descrito. ¡Los términos en NuPRL pueden incluso no tener tipos! Es cierto que el hecho de que "PRL" significa "Lógica de refinamiento del programa" también podría ser un indicio. Por otro lado, Tipos de refinamiento para ML describe un sistema de tipo de refinamiento, posiblemente el origen del término, que de ninguna manera es un sistema de tipo dependiente.
En cuanto a los triples Hoare, son un tipo de sistema de refinamiento. En realidad, se usan como ejemplo de un sistema de refinamiento de tipo en el primer artículo. Sin embargo, la teoría del tipo de Hoare ofrece algo que puede verse como un sistema de tipo sin refinamiento para un lenguaje que tiene triples de Hoare.
Para tener una respuesta sobre el "poder" de los diferentes sistemas, debe especificar un sistema (s) de tipo dependiente particular (familia de) y un sistema (s) de tipo de refinamiento particular (familia de). El término "sistema de tipo dependiente" cubre una clase muy amplia de sistemas de tipo, y "sistemas de refinamiento de tipo" es aún más amplio. Incluso entonces, los términos no son mutuamente excluyentes, por lo que no sería una comparación entre "sistemas de tipos dependientes" y "sistemas de tipos de refinamiento". Sin embargo, si por "sistema de tipo dependiente" está pensando en algo como Coq , y para "sistema de tipo de refinamiento" algo como Tipos de líquidoentonces es bastante unilateral. Coq generalmente se considera lo suficientemente potente como para manejar prácticamente todas las matemáticas en la práctica; literalmente podría implementar y probar que un solucionador SMT es correcto dentro de Coq y luego usarlo; y se puede formular un análogo muy cercano al tipo de subconjunto. (NuPRL literalmente tiene tipos de subconjuntos). Por otro lado, los solucionadores SMT generalmente están restringidos a teorías decidibles donde Coq no tiene esa limitación; y muchos sistemas como Tipos líquidos tienen un lenguaje limitado y no extensible para especificar predicados. (Por supuesto, por "sistema de tipo dependiente" se podría decir ML dependiente , y por "sistema de refinamiento de tipo" NuPRL [que también es un sistema de tipo dependiente] que sería unilateral en el otro sentido).
