Tipos dependientes vs tipos de refinamiento

¿Alguien podría explicar la diferencia entre los tipos dependientes y los tipos de refinamiento? Según tengo entendido, un tipo de refinamiento contiene todos los valores de un tipo que cumple un predicado. ¿Existe una característica de los tipos dependientes que los distingue?

Si ayuda, me encontré con tipos refinados a través del proyecto Liquid Haskell, y tipos dependientes a través de Coq y Agda. Dicho esto, estoy buscando una explicación de cómo difieren las teorías.

Las principales diferencias son a lo largo de dos dimensiones: en la teoría subyacente y en cómo se pueden usar. Vamos a centrarnos en lo último.

Como usuario, la "lógica" de las especificaciones en LiquidHaskell y los sistemas de tipo de refinamiento en general, se restringe a fragmentos decidibles para que la verificación (e inferencia) sea completamente automática, lo que significa que uno no requiere "términos de prueba" del tipo necesario en su totalidad entorno dependiente Esto lleva a una automatización significativa. Por ejemplo, compare el orden de inserción en LH:

http://ucsd-progsys.github.io/lh-workshop/04-case-study-insertsort.html#/ordered-lists

vs. en Idris

https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr

Sin embargo, la automatización tiene un precio. No se pueden usar funciones arbitrarias como especificaciones como se puede en el mundo totalmente dependiente, lo que restringe la clase de propiedades que uno puede escribir.

Por lo tanto, un objetivo de los sistemas de refinamiento es extender la clase de lo que se puede especificar, mientras que la de los sistemas totalmente dependientes es automatizar lo que se puede probar. ¡Quizás haya un lugar de encuentro feliz donde podamos obtener lo mejor de ambos mundos!

$T$$P$$T$

$\{x:T_1 \to T_2 \mid P\}$ [1]. Tenga en cuenta que los tipos totalmente dependientes (como los tipos sigma) no están permitidos.

El sistema de tipo líquido, descrito en [1], es decidible y Liquid Haskell utiliza solucionadores SMT. Sin embargo, Liquid Haskell también requiere términos de prueba (o valores, como se los llama en un lenguaje de tipo no dependiente): si te sientas a escribir un programa de Liquid Haskell, escribes tus propias funciones, no solo los tipos.

[1] http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf

Los tipos dependientes son tipos que dependen de los valores de cualquier manera. Un ejemplo clásico es "el tipo de vectores de longitud n", donde nes un valor. Los tipos de refinamiento, como usted dice en la pregunta, consisten en todos los valores de un tipo dado que satisfacen un predicado dado. Por ejemplo, el tipo de números positivos. Estos conceptos no están particularmente relacionados (que yo sepa). Por supuesto, también puede razonablemente tener tipos de refinamiento dependientes, como "tipo de todos los números mayores que n".