Can we add dependent type into an existing imperative programming language?

Question

As we know, dependent type allows programmers to write bugless programs.
But as I know there's only very few languages support dependent type, like Haskell with extensions, Idris, Agda, F*, etc.

Since these are all functional languages, is there any possibility to add dependent type into an imperative language?

I've googled and found some papers like http://www.ats-lang.org/MYDATA/Xanadu-lics00.pdf or https://www.cs.bu.edu/~hwxi/academic/papers/XanaduAbs.ps, but they create their own languages.

Answer 1

So, it's possible, but there are certainly some barriers:

• What kinds of expressions are allowed in types? What does it mean for a type to have a side-effect? Can typrchecking my program perform IO?
• Just because dependent types are in the system doesn't mean they provide a type safe language. It may be possible to produce proofs of False if the underlying type system is not consistent.
• Many imperative languages don't have type systems complex enough to make dependent types useful. For example, Go has no higher kinded types, so if you can't index types by types, indexing types by values probably won't work.
• Depending on the language, some additional type annotations might be necessary to make type checking decidable.
• It may be hard to interpret dependent types in the context of side effects. What does a value of type $x=y$ even mean if $x,y$ can change their values at runtime? Does this mean a term can be well typed at one point, and dynamically become ill typed? Or can you only use dependent types for immutable values?

I'm sure that imperative dependent types are possible. In particular, I'd keep my eyes on Rust for adding these in a limited way.

But doing dependent types in a pure functional language is just so much easier.