[pyrale]

Well, I can't be bothered to edit wikipedia, but it's a confusing claim. Dependent typing does not require runtime information, results can be produced at compile time. The dependent type depends on a value, but the interesting property of the value is independently tracked in the type system, it's not retrieved from runtime information.

The gist of how it works is so:

    createEmptyIntList() => List<size=0, content=int> {...}
    push(List<size=a, content=b>) => List<size=a+1, content=b> {...}
    firstElement(List<size=a, content=b> | a > 0) => b {...}

In this example, you don't need to know runtime values, you need to know that you can safely get the first element. For that, you just need to know that something has been pushed at least once in the list.

Since push returns a type that is different from createEmptyList, your typesystem has this information.