Há um trabalho recente de Paul-André Melliès e Noam Zeilberger que explora isso. Em particular, os Functors são Sistemas de Refinamento de Tipo e Teorema de Dualidade Isbell para Sistemas de Refinamento de Tipo . Há também um vídeo de uma palestra sobre o primeiro.
Eu acho que há muita confusão em torno dos tipos de refinamento, porque as pessoas pensam em sistemas específicos como representativos, o que faz com que as metas e os detalhes desses sistemas particulares sejam atribuídos à idéia geral. Em resumo, os sistemas de refinamento de tipo classificam os termos que existem independentemente, enquanto os tipos (sem refinamento), dependentes ou não, fazem parte dos termos. Isso pode parecer familiar e possivelmente até um pouco contraditório.
A parte aparentemente familiar e possivelmente contraditória aparece se você visualizar tipos à la Curry (extrinsecamente) versus tipos à igreja (intrinsecamente). Quando pensamos nos tipos à la Curry, pensamos nos tipos como classificando termos não tipados que já têm significado. Nos tipos à Igreja, os únicos termos que existem são termos bem digitados, ou seja, as restrições de tipo fazem parte da nossa sintaxe. Então, o que estou dizendo é que um sistema do tipo Curry é realmente um sistema de refinamento de tipos que refina termos não digitados, enquanto um sistema do tipo Igreja não é um sistema de refinamento de tipos. Isso significa que, por exemplo, podemos pensar no cálculo lambda simplesmente digitado como um sistema de refinamento de tipo ou como um sistema de tipo sem refinamento.
Obviamente, ninguém diz que nossos termos devem ser termos não digitados. Poderíamos também aplicar um sistema de refinamento de tipo a termos digitados e, historicamente, esse é o contexto em que os tipos de refinamento (por esse nome) surgiram. No entanto, os aplicativos para digitação suave ilustram algo mais próximo da situação descrita acima.
Até agora, não disse nada sobre tipos dependentes. A razão é que é uma preocupação completamente ortogonal. Eu diria que os sistemas de tipo dependente arquetípico são geralmente apresentados no estilo da Igreja e, portanto, não são sistemas de refinamento de tipo, mas o NuPRL (baseado na Teoria do Tipo Computacional , uma variante da teoria do tipo dependente mais arquetípica, a teoria do tipo Martin-Löf) é descaradamente um sistema de refinamento de tipo, como descrevi. Os termos do NuPRL podem nem ter tipos! É certo que o fato de "PRL" representar "Program Refinement Logic" também pode ser uma dica. Por outro lado, Tipos de refinamento para ML descreve um sistema de tipos de refinamento, possivelmente a origem do termo, que não é de forma alguma um sistema de tipos dependentes.
Quanto aos triplos Hoare, eles são um sistema de refinamento de tipo. Na verdade, eles são usados como exemplo de um sistema de refinamento de tipo no primeiro artigo. No entanto, a Teoria dos Tipos Hoare fornece algo que pode ser visto como um sistema do tipo não refinado para um idioma que triplique o Hoare.
Para ter uma resposta sobre o "poder" de diferentes sistemas, é necessário especificar um (s) sistema (s) de família (s) específico (s) e um (s) sistema (s) de tipo de refinamento (s) (família de). O termo "sistema de tipos dependentes" abrange uma classe muito ampla de sistemas de tipos e "sistemas de refinamento de tipos" é ainda mais amplo. Mesmo assim, os termos não são mutuamente exclusivos, portanto não haveria uma comparação entre "sistemas de tipos dependentes" e "sistemas de tipos de refinamento". No entanto, se por "sistema de tipos dependentes" você estiver pensando em algo como Coq , e em "sistema de tipos de refinamento" algo como Tipos de Líquidosentão é bem unilateral. Coq é geralmente visto como poderoso o suficiente para lidar com praticamente toda a matemática na prática; você poderia literalmente implementar e provar corrigir um solucionador SMT na Coq e depois usá-lo; e um análogo muito próximo ao tipo de subconjunto pode ser formulado. (O NuPRL literalmente tem tipos de subconjuntos.) Por outro lado, os solucionadores de SMT são geralmente restritos a teorias decidíveis em que a Coq não tem essa limitação; e muitos sistemas, como Liquid Types, têm uma linguagem limitada e não extensível para especificar predicados. (Obviamente, por "sistema de tipos dependentes", você pode significar ML dependente e por "sistema de refinamento de tipos" NuPRL [que também é um sistema de tipos dependentes], que seria unilateral da outra maneira.)
