El lenguaje de programación dependiente ( DML ) es un lenguaje de programación funcional , de alto nivel , multiparadigma y de propósito general propuesto por Hongwei Xi (Xi 2007) y Frank Pfenning . Es un dialecto del lenguaje de programación ML . El lenguaje de programación dependiente extiende el lenguaje de programación ML mediante una noción restringida de tipos dependientes : los tipos pueden depender de índices estáticos de tipo ( números naturales ). El lenguaje de programación dependiente emplea un demostrador de teoremas de restricción para decidir una teoría ecuacional fuerte sobre las expresiones de índice. Nat
Los tipos de DML no dependen de los valores de tiempo de ejecución: todavía hay una distinción de fase entre la compilación y la ejecución del programa. [1] Al restringir la generalidad de los tipos completamente dependientes , la verificación de tipos sigue siendo decidible , pero la inferencia de tipos se vuelve indecidible.
El ML dependiente ha sido reemplazado por ATS y ya no se encuentra en desarrollo activo.