Isn't "Dependent types" just re-inventing how Fortran handles non allocatable array and character variables i.e. those who's length is declared at compile time using a parameter?
It's a bit more than that. Let's assume Vector is a typed list type of know length
[1,2,3] : Vector 3 Int
we can write `append` which combines Vectors
append : (Vector n a, Vector m a) -> Vector (n + m) a
which works as you expect because the expression in the type (n+m) is written in the value language.
Here's another (slightly pathological) dependent type. Normally `if` statements require that the then and the else branches result in the same type, but in a DT language you can write
if' : (cond : Bool) -> a -> b -> (if cond then a else b)
In other words, `if'` takes the type where you first provide it a boolean, we'll call it `cond`, and then two differently type continuation parameters. The type of the result is an expression: "if cond is true then this is the type of the first continuation, otherwise this is the type of the second continuation".
Both of these examples would be proud to call themselves trivial. The DT rabbit hole goes very deep.
The article unfortunately does quite a poor job of explaining what dependent types are and why they're valuable. They're a lot more complicated than just "storing the length of a vector in its type". Dependent types allow you to create types where one type in a signature 'depends' on the value of another type in the same signature. This is very powerful, but unfortunately easily understandable examples are still somewhat hard to come by.
Longer answer: Sort of. An array has an element type and length associated with it (and it ATS at least, the type-level length isn't kept at run-time) and that length is set when the array is created, and modified if elements are added or removed. However, functions can require parameter types or provide return values of "array T n | n > 0 && n < m" --- the array cannot be empty and has to be smaller than some limit.
There's a good deal more to dependent types, but they are much more flexible than simply attaching the length of the array to its type.
Common Lisp does not have dependent types. The example given is unfortunate because it often leads people to think they already have (and understand) dependent types, when that isn't the case.
Here's another (slightly pathological) dependent type. Normally `if` statements require that the then and the else branches result in the same type, but in a DT language you can write
In other words, `if'` takes the type where you first provide it a boolean, we'll call it `cond`, and then two differently type continuation parameters. The type of the result is an expression: "if cond is true then this is the type of the first continuation, otherwise this is the type of the second continuation".Both of these examples would be proud to call themselves trivial. The DT rabbit hole goes very deep.