There is plenty of work in PL that covers why type theory is useful. Check out the classic paper by Philip Wadler called &quot;Theorems for free&quot; that covers some of the terrific benefits of parametric polymorphism.<p>There has also been a good amount of discussion generated by organizations such as Jane Street concerning the benefits of static typing and type inference in practice. Notably, the free documentation (that is completely coupled with the code) that you get when you design software that takes advantage of the type system.