> 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.
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.