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