http://www.reddit.com/r/programming/comments/ehjs5/not_dependent_types_in_d/

Although this is way over my league (I've never used functional languages before), I guess invariants could help in maintaining a type with certain properties of those dependent types..?

Well, most of the papers that describe dependent types (that I've glanced over) use functional languages and a lot of type theory, so it's hard to grasp exactly what are the benefits of these dependent types, since I don't know much about either unfortunately.

On 12/7/10, bearophile <bearophileHUGS@lycos.com> wrote:
> http://www.reddit.com/r/programming/comments/ehjs5/not_dependent_types_in_d/
>
>
>

Andrej Mitrovic:

>Although this is way over my league (I've never used functional languages before),<

That's easy stuff, you probably need just few hours to get used to that.


>I guess invariants could help in maintaining a type with certain properties of those dependent types..?<

Yes, invariants may replace some of the purposes of dependent types, but currently in D invariants are verified at run-time, so the bugs are found in different moments or later.


> Well, most of the papers that describe dependent types (that I've glanced over) use functional languages

Some years ago the author of the ATS language has designed a small imperative language with dependent types named Xanadu. It's limited, but shows that functional languages are not strictly necessary:
http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html


>and a lot of type theory, so it's hard to grasp exactly what are the benefits of these dependent
types, since I don't know much about either unfortunately.<

Behind that feature there is a complex type system and a complex inferencer, but if you read the right articles/blog posts, I think you will be able to understand the purposes in a short time.

Bye,
bearophile