[DylanSp]

I wouldn't call those dependent types, exactly, because it's still happening entirely at the type level. The defining characteristic of dependent type systems is that they allow mixing of type-level and value-level expressions. To use the classic example of appending one vector to another, Idris lets us express the type:

  app : Vect n a -> Vect m a -> Vect (n + m) a

where we're using the value-level addition operator to express the type of the result; specifically, that appending a Vect of length m to a Vect of length n will give a Vect of length (n + m). [1]

[1] Taken from https://www.idris-lang.org/pages/example.html

[dwohnitmok]

They are dependent types since they do depend on runtime values (notice in `DB` the `k` is a runtime value), rather than just types. They are, however, very restricted compared to more "full-spectrum" dependently typed languages.