Every time I read something about type theory I just can't get past the notation. I've taken two classes on it, and somehow it just never stuck. I struggled with it as much in those classes as I do now. Once I parse the statements the ideas always end up coming through as elegant and intuitive, but getting there is a slog. Does anyone else have this problem? Is my brain just broken w.r.t. type theory symbols?
Type theorists must use such strange notation to make sure there's never a collision between something in their meta language, and something that someone would actually use in a language. :)
A big topic in type theory nowadays is equational reasoning. The classic example is, how can you prove that two functions are observationally equivalent -- that they give the same output for all inputs? Bob discusses that in his book.
More generally, you can discuss various other notions of equivalence, both for functions and (in this case) types. So if we do allow a programmer to define their own notions of equivalence, is that good enough? Not quite -- it can be difficult to propagate this notion through to derivative constructs. You'd like for there to be a way to get all sorts of "free" theorems basically. So I think that is what this blog post is beginning to talk about, in somewhat technical terms.
But, to be perfectly honest, I'm a systems-focused PL graduate student and have spent quite a bit of time studying this stuff and doubt that I could easily produce a more accessible version of this post. I tried (in the comments block here) and ran on to about two pages before realizing I had only covered the back story on his "trinity" analogy without even getting to this post itself. Someone far smarter than I probably could, but don't feel disappointed if you found this post mathematically challenging even if you normally follow PL theory. It took me a solid cup of coffee and a half an hour to deeply understand what he was saying.
Pierce's TAPL primarily covers the type side of this "trinity" and TAPL2 really only has one relevant chapter, covering Dependent Types.
Type theorists must use such strange notation to make sure there's never a collision between something in their meta language, and something that someone would actually use in a language. :)