[rfw]

Unfortunately, the usefulness is limited – the size of all Vects must be known at compile time. While this does prevent a large class of bugs that arise from incorrect compile-time knowledge, the size of the class of runtime bugs affected by this is a lot smaller, as for each differently-lengthed Vect, a distinct instantiation of the Vect type needs to exist at compile-time.

[dllthomas]

Per my understanding, what's so exciting about this is precisely that you're wrong - it does not need to be known at compile time, but can prove symbolically that the resulting length will be X + Y. And of course, given that, it's not statically creating a distinct instantiation of the Vect type for every N at compile time!

[rfw]

Really? Color me corrected, then :) Does the compiler need a SAT solver then to make sure all the constraints hold?

[dllthomas]

I'm not sure the exact approach, but there's definitely some heavy lifting. My understanding is that most (all?) dependently typed languages are essentially theorem provers at heart.

[chenglou]

See my answer here: https://news.ycombinator.com/item?id=10856736

[pzone]

It should be able to use a Hindley-Milner algorithm.

[dllthomas]

As I understand it, type inference breaks down on dependent types.

[orblivion]

I've never actually used such a feature, but my understanding is that this is not strictly true. I think that the compiler can generically understand that this function adds two vectors and their lengths.

I'll see if I can contrive an example. Supposing you have a list L1 of vectors of length 5. You also have a vector V1 with user input, with length x (unknown at compile time). You then make a new list L2 by taking each vector in L1 and append V1 to it. L2 is now a list of vectors of length (5 + x). Even though x is unknown at compile time, the compiler still knows that all vectors in L2 are of the same length. It can make restrictions based on this fact.

It seemed strange to me when I heard this concept, I thought the compiler would need to consider infinite possibilities, but apparently similar things are possible even in Haskell. For instance, you can define a list as a recursive type that holds a value of a Null type (not just a null value of the list type) or another List. Apparently it can still reason about this.

However, these are things I've heard. Hopefully someone with more experience can chime in and let me know if I'm right here.

[kmicklas]

Not quite. Types can depend on runtime values. This can in effect _force_ the programmer to perform the required validation when accepting foreign data.

[lambdasquirrel]

Not only that but you can arbitrarily encode constraints. Want to check something silly like whether there's an even number of elements in a list? Yea you can do that, and pass it along. I can do stuff like, okay, I know the max size of the files we're going to accept is 1mb.

[dllthomas]

Almost arbitrarily - they must be computable... ;)

[kazagistar]

From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.

[kmicklas]

You're correct that Idris doesn't force termination. That doesn't let you compute non-computable functions though (e.g. the busy beaver function).