From what I gather, this happens at runtime, which makes me feel it's a bit unfortunate to call it dependent types, or at least my view of dependent types is of

From what I gather, this happens at runtime, which makes me feel it's a bit unfortunate to call it dependent types, or at least my view of dependent types is of it being a compile-time guarantee. Take for example Liquid Haskell[0] where you can, at compile time, make guarantees about your code. For example, here's a function that makes division safe, by never allowing the second value, y, to be 0, {-@ safeDiv :: Int -> {v:Int | v != 0} -> Int @-} safeDiv :: Int -> Int -> Int safeDiv x y = x `div` y The second annotation is plain Haskell meaning it takes 2 `Int`s and returns an `Int`, with the third line being the function body. The first {-@ .. -} annotation is the one Liquid Haskell reads, stating it takes an `Int` as the first argument, another `Int`, which we now refer to as v, that is not 0, and finally returns an `Int`. Another practical language with dependent types is Idris[1], which supports full dependent types with dependent pattern matching. Finally, for the "why would I use this", I recommend checking out Gabriel Gonsalez's keynote, from Haskell eXchange 2017, "Scrap your Bounds Checks with Liquid Haskell"[2] [0] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/ [1] https://www.idris-lang.org https://www.idris-lang.org [2] https://skillsmatter.com/skillscasts/10690-keynote-scrap-your-bounds-checks-with-liquid-haskell https://skillsmatter.com/skillscasts/10690-keynote-scrap-you...