##  [Tipos Dependientes](/es/node/61345) 

 Definición

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

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

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

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

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

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

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 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

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.