alt Hacker News> But dependent types (and static types in general) don't exist at runtime!
That isn't entirely true when it comes to dependent types and can be seen as a design choice. Types can depend on values and those values can often exist at runtime. Erasure only applies to parts we can determine are not computationally relevant.
For example `Vec n a`. The `n` is a natural number you may need at runtime, such as to get the length without walking the list. A dependent pair `Sigma(n : Nat). Vec n a` carries that `n` at runtime as ordinary data.
In fact many dependently typed languages have techniques, such as quantitative type theory, to assert what is needed at runtime.
You've exactly described the answer, but to people who don't know much about dependent types, this may be a little unclear. The point is that there are two sorts of dependent types.
When people who don't know much about them think of dependent types, they are probably thinking of functions, which can take a value on the left hand side to be used in the type on the right. Confusingly, these are normally called "dependent products" in the type theory. However since this is confusing and they are generally written with a capital Pi, they are often just referred to as "Pis". For example
is a function that takes a nat (non-negative number) and returns a Vector whose length is that nat and which is encoded in the type.On the other hand, you are talking about pairs (confusingly: "dependent sums", here "sum" being something like a union/enum in type theory), often called "Sigmas". These are pairs (2-tuples) of values in which the type of the second value depends on the value of the first. So, your example, a pair where the vector length is held in the first element and the vector itself in the second. In this contrived example, Vector may not know its own length at runtime, so we need to package them up together.
These are both "dependent types", but people who are only passingly familiar with them might mostly know about the first.(Why are functions "dependent products" and pairs "dependent sums"? I've never understood this but I've heard hand-wavy explanations that infintitary products are functions and infinitary sums are products ¯\(ツ)/¯)