ML dependiente es un lenguaje de programación funcional experimental propuesto por Hongwei Xi ( Xi 2007 ) y Frank Pfenning . El ML dependiente amplía el ML mediante una noción restringida de tipos dependientes : los tipos pueden depender de índices estáticos de tipo Nat ( números naturales ). ML dependiente emplea un demostrador de teoremas de restricción para decidir una teoría de ecuaciones sólida sobre las expresiones de índice.
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 dependientes completos, 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.
Referencias
- ^ Aspinall y Hofmann, 2005. p. 75.
Otras lecturas
- Xi, Hongwei (marzo de 2007). "ML dependiente: un enfoque para la programación práctica con tipos dependientes" . Revista de programación funcional . 17 (2): 215–286. doi : 10.1017 / S0956796806006216 . S2CID 45996427 .
- David Aspinall y Martin Hofmann (2005). "Tipos dependientes". En Pierce, Benjamin C. (ed.) Temas avanzados en tipos y lenguajes de programación . Prensa del MIT.