After reading the literature on type theory (especially the constructive kind - CTT) I'm left wondering "why" should one study type theory, specifically within the confines of "computing" in general?
I understand how type systems (loosely speaking) were created to avoid various paradoxes and the correspondence between philosophy, logic, lambda-calculus and the how it comes together for CTT to serve as a foundation of mathematics. Fair enough.
Now, functional programming (FP) languages like Haskell, Scala that can be used in large projects are based on an inconsistent logic - making any kind of (automated) formal reasoning about them nearly impossible - but that seems to be the very need/power of TT! E.g., theorem proving and proof assistants and the notion of programs as proofs. But none of this carries over to FP languages.
So my question is trying to understand the bigger role i.e., interplay of TT and computing taken together. Most FP languages have just "good enough" type systems (e.g., Haskell > Java). The problem of "type inference" is in some way similar to "logical inference" and doesn't seem all that complicated for simple types. I'm guessing things become undecidable after a particular threshold. Fair enough. I understand its need till this level. But is that it? It seems one can understand type systems/inference without really diving into the details of TT per se.
Since FP languages don't really borrow much from TT other than "type systems/inference", why bother studying the theory in depth especially within computation theory? It seems that after studying a good deal of TT, for fun, I'm still left wondering "what did I gain" - both as a theoretician and a software practitioner? What "is" the aha understanding that one gains at a deeper level - since very little of TT's power/awesomeness actually gets carried over to commercially viable FP languages (and not Agda, Epigram etc.,)?
(PS: Here's a similar question on Math.SE- but that's from a mathematical POV and I get that from that perspective. I'm struggling to see TT's importance when concerned about computing and software engineering in general)