Comment by randomNumber7

Why is type theory always tied to functional programming? Wouldn't it be possible to use some of the ideas in imperative languages?