On Thursday, 30 July 2015 at 13:25:31 UTC, Timon Gehr wrote:
There is no dependent typing here. Failures occur during interpretation.
Type theory doesn't say anything about interpretation and compilation. Are you saying there cannot be an interpreted dependently typed language? (hint: Idris has a REPL) Also, during compilation dependently typed languages evaluate a lot of code (do CTFE in D terms), and some fails occur during this process. So this is not the real difference.
