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.

Reply via email to