Sure, no problems.
I think there's a few misconceptions in your blog, for instance "
First, we need to create our list without putting any elements in it, but doesn’t this violate the constraint?" isn't much of a problem, and has never stopped the C++ guys (e.g. http://www.boost.org/doc/libs/1_50_0/doc/html/array.html ). The trick is to have a constructor similiar to the one in Kotlin. e.g.
FixedSizeArray[Size: Int, Type](init: (int: Index) -> Type)
(i.e. a function that can initialize it). You can also fill the Array with some default value (mutability and dep typing are largely orthogonal!)
Before I start providing examples, I should make it clear that I'm just advocating a generic system more along the lines of D or C++, than some full blown dependent typing like Agda.
So my background is from C++, and the last 9 or so months I've been using Scala. Here's some cases I've run into, that either scala's dependent method types helped -- or I wish I had a more C++ish type system:
Example 1: We are working on an abstraction layer on top of Hadoop, where hadoop requires that all Key and Values implement the "Writable" interface. So we want to provide a default implementation for all the common types. This is straight forward, until you run into types that people wrote code generators for [because the type system limited them]. E.g. Tuple1, ... Tuple23, ProductN, FunctionN, etc. etc. So now we have to decide between copying and pasting hundreds of lines of code, or writing our code generation for scala's code generated stuff ewwwww. Had this been a case of Tuple[N: Int] (like the new C++11 one), this would've been far superior and we could've written it properly.
Example 2: [Note this is a simplification of the problem we solved using Scala's dependent typing here: https://github.com/NICTA/scoobi/blob/master/src/main/scala/com/nicta/scoobi/application/Persister.scala#L33 ] I'm going to give a far more understandable analogy here.
Let's say you want to do a database/relational style equijoin of something that has the type Collection<K, V> and Collection<K, W> -- for arguments sake, lets say you want to end up with something of the type Collection<K, #(V, W)>. This is good and true, but it doesn't really hold when you nest them:
a join b join c
You wouldn't want to end up with Collection<K, #(V, #(W, X)> but you'd rather: Collection<K, #(V, ,W, X)> -- in short, you want a different depending on one of the types ;D This problem actually comes up a lot when you understand it. For instance, I find boost::asio parser nicer to use than the scala parser combinators because of this issue (and because its smart enough to know when you parse something that returns a 'Unit' you don't want to add it to the type etc.)
Example 3: For the love of god, I really something that has half the power of C++'s boost::multi_index
Example 4: For efficiency, sometimes you want to move things from being stored in each instance of the object, but rather in the type. Like in Scala's persistent HashMap they have:
"Note: the builder of a hash map returns specialized representations EmptyMap,Map1,..., Map4 for maps of size <= 4.". But with a nice type system, you can just do this: https://github.com/espringe/wisp/blob/87e2e682b5230ae9fa373cc6af23b2f6ea1e7266/persistent/map.hpp#L59
without having to (again!) resort to code generation. As an added bonus, you have some nice typesaftey (Map1 can only point to a Map2 etc.)
Example 5: Type safe feature vectors. We do a lot of machine learning, and having typesafe feature vectors would be simply amazing. A feature vector is basically the result of data extraction, and what you train your machine learning algorithm on. They are typically are from a few hundred elements, to a few thousand. They're fixed width, and fixed type. They generate a model which takes in data of the same. Right now we have to throw away all type saftey, basically. But evne if we could preserve the size would be very useful, and stop a lot of mistakes. And having fulll type information (i.e a big ass tuple, where every element in the tuple must meet some requirement) would just be great
That's just off the top of my head, but I could probably provide some more if you're still not convinced :)