GoKawiilThe reason I'm writing this post is because I actually wanted to write a more advanced post on type inference for anonymous records, but then I realized that most of my readers wouldn't understand the latter post in isolation. So I figured I would write this introductory post to teach people new to type theory the basics.
The reason I'm writing both posts is because I believe that good type inference for anonymous records is one of the big things holding back statically typed languages1 and not enough people appreciate this or understand why. I also think that there is a large disconnect between what programming language experts understand is possible and what lay programmers are comfortable or familiar with. To make a play on XKCD #2501:
So this post (and the next one) are going to be an exposition of where the field of type theory was at over three decades ago, which our industry still hasn't really caught up to, yet.
Anonymous records
I mentioned that this is a post about type inference for anonymous records and I've met some programmers who either don't know what anonymous records are or at least don't recognize them by that name, so I'll briefly touch upon them.
An anonymous record is a record that doesn't require an associated datatype declaration, and they're quite common in dynamically typed languages. For example, JavaScript calls them "objects":
{ name : "Alice" , age : 25 }
Python calls them "dictionaries":
{ "name" : "Alice" , "age" : 25 }
Ruby calls them "hashes":
... continue reading