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

[Timon Gehr via Digitalmars-d-announce]

On 07/30/2015 05:45 PM, thedeemon wrote:
> 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.

You need to consider the type system and the evaluation semantics. What 
are they for the "interpreted meta-programming part of D"? (I can find 
the semantics, but not a non-trivial type system.)

> Are you saying there cannot be an interpreted dependently typed
> language? (hint: Idris has a REPL)

Obviously I'm not saying this, because it is nonsense.
I'm saying that e.g. Python is not such a language, and neither is the 
language which is interpreted by the D compiler while generating an 
executable.

> 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.
>

The real difference is (roughly!) that the dependently typed interpreted 
program always fails if it would fail in any possible execution (and 
usually in more cases than this one) (assuming type-safety).
"Dynamically typed" interpreted languages on the other hand only fail if 
the particular execution exposed fails. This is what we are looking at here.