Una característica teórico-tipológica y familia de sistemas en los que los tipos pueden depender de valores (términos), permitiendo que los tipos expresen especificaciones precisas, relacionen datos y pruebas e internalicen proposiciones como tipos.

Principio

Tipos como predicados: un tipo puede parametrizarse por un valor (por ejemplo, Vector n A) de modo que el tipado impone invariantes a nivel de valores; la correspondencia proposiciones‑tipos (Curry–Howard) se realiza con mayor expresividad.

Demostración

Definir un tipo de listas con longitud n como List A n y escribir una función append : ∀n m. List A n → List A m → List A (n + m); el tipo asegura en tiempo de compilación que la longitud del resultado es la suma de las longitudes de las entradas.

Aplicación incorrecta

Codificar propiedades indecidibles o costosas directamente en los tipos (por ejemplo, usar búsqueda arbitraria durante la comprobación de tipos) sin precaución, lo que puede hacer que la comprobación de tipos no termine o que los programas resulten impracticables de escribir y mantener.

Consecuencia

Permite incrustar especificaciones ricas en los tipos de modo que muchas propiedades de corrección son verificadas por el comprobador de tipos, posibilitando la extracción de programas a partir de pruebas constructivas y software de alta garantía cuando se diseña correctamente.

Inversión

Sistemas de tipos simples donde los tipos son independientes de valores en tiempo de ejecución (p. ej. sistemas simplemente tipados), que renuncian a especificaciones expresivas a favor de comprobación de tipos decidible y eficiente.

Límite

Se aplica cuando la disciplina de comprobación de tipos admite cálculo a nivel de valores y comprobaciones de terminación; los tipos dependientes no deciden propiedades semánticas arbitrarias y a menudo requieren restricciones de totalidad/terminación y obligaciones de prueba.

Tensión semántica

Tensión entre tipos dependientes expresivos que pueden declarar invariantes fuertes y el deseo de una comprobación de tipos decidible y eficiente con automatización; también la tensión entre usar tipos dependientes para pruebas frente a la ergonomía pragmática de la programación.

Síntesis

Los tipos dependientes extienden el sistema de tipos para que los tipos puedan referirse a valores, convirtiendo los tipos en especificaciones precisas y permitiendo que las pruebas sobre el comportamiento del programa coexistan con el código; sacrifican mayor expresividad y poder de verificación frente a una mayor complejidad en la comprobación de tipos y el desarrollo.