[blog post] Dependent types in (half of) D

[thedeemon via Digitalmars-d-announce]

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.