Seguramente se lo han preguntado, si esta tan bueno dependently typed, porque no lo implementa Haskell?
El problema es que debería romper la restricción de fase entre el tipo y niveles de valor que permite Haskell para ser compilado a código máquina eficiente. Con nuestro nivel actual de la tecnología, un lenguaje dependently typed debe correr sobre una maquina virtual o interprete.
Idris es compila a C pero tiene un garage collector, la verdad no se bien como lo hace. Alguien me ayuda?
