Something

[bearophile]

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