But, its still hard for me to grok it properly. Can someone provide a brief explanation of the central idea(s) of type theory, some idea of how it is useful in practice (e.g., to type systems), and a reading list (hopefully not too dense) of the foundational ideas?
Also, I'd like to explore some type system ideas in a new programming language. What other topics might be useful to invest time into studying?
So, allow me to put down some ideas with no particular structure.
* A good type system should maximise the number of correct programs that can be written, while minimising the number of incorrect programs that can be written - Simon Peyton Jones
* A good starting point is the lambda calculus, because it has only three expressions (vars, abstractions, applications). If you add types, you get the simply-typed lambda calculus. STLC guarantees termination.
* Most type systems distinguish terms and types. Some type systems additionally have kinds (types of types).
* In the STLC, you can express terms which depend on other terms. But one could add the ability for terms to depend on types (polymorphism), types to depend on terms (dependent types) and types to depend on types (type operators). The idea of adding functionality this way is sometimes rendered as The Lambda Cube.
* Hindley-milner is a popular type system. It has 6 typing rules. The first 3 (var, app, abs) correspond to the 3 expressions of the lambda calculus. There is also (let, gen, and inst). Let is more-or-less the same as abs. Gen and inst are for polymorphism. That is, gen recognises an expression like 'id x = x' and says 'not only could x be any type, but it could be different types depending on who calls it'. This is sometimes called a polytype, or a 'forall'. The inst rule does the reverse, it can take a 'forall a. a -> a' and instantiate it to a monotype 'Bool -> Bool'.
* It was recognised that this type system 'was the same thing' as 1st order logic, e.g. modus ponens corresponds to the App rule. The observation that type systems correspond to logic systems is the Curry-Howard isomorphism.
For Hindley Milner, read https://legacy-blog.akgupta.ca/blog/2013/05/14/so-you-still-...
For curry-howard (and basically everything else I scribbled above) watch https://m.youtube.com/watch?v=IOiZatlZtGU
Some applied references/examples can often be found within discussions on designing/implimenting a given programming language (virtual machine, compiled, interpreted).
Computational Type Theory : http://www.scholarpedia.org/article/Computational_type_theor...