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.