• thedeemon (5/5) Jul 30 2015 I had this idea for a long time but a recent talk about a real
• Andrei Alexandrescu (4/8) Jul 30 2015 Thanks to the person who put this on reddit:
• Timon Gehr (2/6) Jul 30 2015 There is no dependent typing here. Failures occur during interpretation.
• thedeemon (7/9) Jul 30 2015 Type theory doesn't say anything about interpretation and
• Timon Gehr (13/21) Jul 30 2015 You need to consider the type system and the evaluation semantics. What
• Timon Gehr (3/6) Jul 30 2015 (This is ambiguous. What I mean is: If there is some execution in which
• thedeemon (9/20) Jul 30 2015 I feel it too, but is this really about dynamic/dependent _types_

"thedeemon" <dlang thedeemon.com> writes:

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

Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:

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

Timon Gehr <timon.gehr gmx.ch> writes:

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.

"thedeemon" <dlang thedeemon.com> writes:

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.

Timon Gehr <timon.gehr gmx.ch> writes:

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.

Timon Gehr <timon.gehr gmx.ch> writes:

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

"thedeemon" <dlang thedeemon.com> writes:

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)