[jmaa]

No; lookup Calculus of Construction. Dependent types allows you to specify an dependence between different values in your type directly within your type system; which has great implications for type safety and so on.

A classic example is that you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }" (read as "the set of real 2-tuples, where their norm is equal to 1".) This is not possible in most languages; the closest you can get in most languages is "{ (x,y) : x,y in R }".

My personal pet peeve with dependent types and proof-driven programming in general is the wealth of options in formulating propositions. I've seen at least five different ways of defining equivalency.

[fuoqi]

>you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }"

Which is not possible for any language targeting real machines since floats have fixed precision.

[icen]

You can specify the 2-vectors on the unit circle as "{ (x, y) : x, y in R | x^2 + y^2 - 1 < 0.000001 }" instead.

[mehrdadn]

To clarify, "great implications" can mean "undecidability".