Haskell is an excellent imperative language and can simulate some aspects of dependent typing. There are also refinement types which are related. Typesafe prin

Haskell is an excellent imperative language and can simulate some aspects of dependent typing. There are also refinement types which are related. Typesafe printf is actually a very old trick, typed scheme and even Common Lisp have been showing off macro-based variants for some time. As for why there aren't more languages directly LIKE Idris and Agda? Probably because the technology and theory to actually make them feasible has existed for less than a full decade. Sorta like how people don't realize sort is an O(n) operation, CRDTs exist, or that we can write lazy succinct parsers of complex tree structures, or can write universal query-insensitive indicies over relational data.