Agda is a proof assistant. I've used Coq, but not Agda -- I imagine they're similar. You wouldn't use it for general development.
Qi is interesting but the development community is much smaller than its competitors (mainly Haskell). You probably want to look into Shen, not Qi. Qi development has mostly stalled.
In the dependently typed family of languages it's a little bit arbitrary to divide between programming languages and proof assistants since everyone in this space can be made to play both roles in a pinch. I think most people think of Coq as more on the proof assistant side and Agda more on the programming language side.
Sort of. Dependent types doesn't explain Coq's requirement for pure, total functions. Unless this restriction is weakened I cannot see it as being useful in any general-purpose domain. Agda may be looser.
I'm not sure what you're saying. I was saying that simply being dependently typed doesn't necessitate pure total functions. Obviously, these features can be considered either highly suggested or necessary for ITPs. There are a number of ways you can get around totality with dependent types.
