Very nice, haven't heard of this before. I think an ideal target for a dependently typed language is scientific array programming, so that you can ensure the sizes of your matrix and array operations check out before performing long-running tasks. If a good array library can be built (e.g. port Haskell's Repa) then it might provide a great foundation for this.
I love the concept, but the tutorial somewhat puts me off (admission: I only read the first third).<p>I mean, using an "element from a finite set" to index a vector? Back home, we use natural numbers for that. Idris <i>also</i> has natural numbers, but somehow we still have to, essentially, use the "finite set of values we don't care about, but that we can order if we want to since, after all, the set has a finite number of elements" concept for what's essentially an array lookup.<p>Why can't there be a type of "natural numbers under N"?<p>Or am I all misunderstanding things, and <i>is</i> the "finite set" exactly that type, just explained in a very not straight forward way?<p>Also, impressively, the author claims it has C-style speed. Does that mean that looking up a value in a vector by means of an element in a finite set is actually translated to a single *(vect+index)? (in C-terms)
Down for me, google cache: <a href="http://webcache.googleusercontent.com/search?q=cache:dtmf_mGqwA4J:idris-lang.org" rel="nofollow">http://webcache.googleusercontent.com/search?q=cache:dtmf_mG...</a>
Is this, by any chance, specifically tailored to programming control systems for time machines[1]?<p>[1]: <a href="http://tardis.wikia.com/wiki/Idris" rel="nofollow">http://tardis.wikia.com/wiki/Idris</a>
Am I correct in my understanding of these types?<p><pre><code> Vect a n = vector of a with known length n
(n ** Vect a n) = vector of a with unknown length n
</code></pre>
When I think of it this way it's obvious why filter takes a Vect and returns a pair. Though it seems ugly to have to write each vector function to take both "static" and "dynamic" vectors.
This looks really cool. I haven't looked into dependently typed languages in depth, but this is the first one I've seen that looks like a programming language to write programs in.