Comment by siraben

I study type systems and programming language theory at university, and I encourage friends studying CS to at least have some understanding of type theory, such as well-known type systems (simply-typed, System F) and properties like soundness or uniqueness of typing. Why? Because as programmers we argue to death comparing the expressiveness and properties of type systems of our favorite programming languages, or we're picking up a language with features like traits or type inference. Type theory really lets you learn the heart of such features in a small, idealistic setting and specifies things rigorously and uniformly, (since languages tend to come up with their own names and examples for things like ad-hoc polymorphism, AKA typeclasses/traits/protocols/concepts), and they appear no matter the paradigm.