I had this idea for a long time but a recent talk about a real dependently typed language helped me with nice examples to demonstrate on. The interpreted part of D is actually dependently typed!

http://www.infognition.com/blog/2015/dependent_types_in_d.html

On 7/30/15 3:31 AM, thedeemon wrote:
> I had this idea for a long time but a recent talk about a real
> dependently typed language helped me with nice examples to demonstrate
> on. The interpreted part of D is actually dependently typed!
>
> http://www.infognition.com/blog/2015/dependent_types_in_d.html

Thanks to the person who put this on reddit: https://www.reddit.com/r/programming/comments/3f59f4/dependent_types_in_half_of_d/

Andrei

On 07/30/2015 09:31 AM, thedeemon wrote:
> I had this idea for a long time but a recent talk about a real
> dependently typed language helped me with nice examples to demonstrate
> on. The interpreted part of D is actually dependently typed!
>
> http://www.infognition.com/blog/2015/dependent_types_in_d.html

There is no dependent typing here. Failures occur during interpretation.

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.

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.

On 07/30/2015 06:13 PM, Timon Gehr wrote:
> ...
> The real difference is (roughly!) that the dependently typed interpreted
> program always fails if it would fail in any possible execution

(This is ambiguous. What I mean is: If there is some execution in which it would fail.)

On Thursday, 30 July 2015 at 16:13:46 UTC, Timon Gehr wrote:
> 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.)

Yes, this is what interests me too.

> The real difference is (roughly!) that the dependently typed interpreted program always fails If there is some execution in which it would fail.
> (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.

I feel it too, but is this really about dynamic/dependent _types_ or is it about static/dynamic checking? This is probably more about compilation semantics than actual type system.
Also, if we have some code paths that are incorrect but never used during compilation, isn't it a guarantee they will never be used at all at runtime so the compiled program is correct? (I'm not sure about all this)