Record type inference for dummies

The 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": { :name => "Alice", :age => 25 }

# … or equivalently: { name: "Alice", age: 25 } …, and Nix calls them "attribute sets": { name = "Alice"; age = 25; } If you've ever worked with JSON then you've worked with anonymous records because JSON objects (just like JavaScript objects) are anonymous records. Static typing A smaller number of statically typed programming languages support anonymous records because statically typed languages usually prefer named datatypes.

For example, Haskell does not support anonymous records and requires a datatype declaration for all records, like this: data Person = Person{ name :: Text, age :: Integer }

example :: Person example = Person{ name = "Alice", age = 25 } … but there are still some statically typed programming languages that do support anonymous records, like TypeScript: { name: "Alice", age: 25 } : { name: string, age: number } … or C# (which calls them "anonymous types"): new { Name = "Alice"; Age = 25 } … or PureScript (which calls them records): { name: "Alice", age: 25 } :: { name :: String, age :: Int } If all we needed was language support for record literals without any operations on records then it's fairly easy to infer their types. To do so, though, I'm going to introduce some type theory notation. Let's start by defining a basic abstract syntax tree that says that an expression () can be either:

a (e.g. ) a (e.g. ) a record containing 0 or more fields (e.g. )

The way we would write that2 formally is:

… and the equivalent Haskell code would be something like: type Identifier = Text

data Expression = Boolean Bool | String Text | Number Double | Record (Map Identifier Expression) Fields can store arbitrary expressions, which means you can nest records, like:

We'll also need to define an abstract syntax tree for our inferred types, which can be either:

the type the type the type a record type containing 0 or more fields (e.g. )

The notation we'd use for that is:

The equivalent Haskell code would be something like: data Type = BooleanType | StringType | NumberType | RecordType (Map Identifier Type) Now that we have a syntax for expressions and types we can define some type inference rules:

and always have type a (like ) always has type a (like ) always has type

We write out those rules using this notation:

If you've never seen this notation before, you can think of it as mathematical pseudocode for how to implement a type inference function.

The equivalent Haskell function would be something like: infer :: [(Identifier, Type)] -- ^ context, a.k.a. "Γ" (currrently unused) -> Expression -- ^ input expression -> Either Text Type -- ^ output inferred type (currently never fails) infer context (Boolean _) = return BooleanType infer context (String _) = return StringType infer context (Number _) = return NumberType

Note: You can find the complete Haskell code in the Appendix.

Now suppose that we wanted to infer the type of a record literal like this one:

Normally we'd reason about the expression's type by hand like this:

to infer the type of we need to infer the type of each field: A. first, infer the type of (which is ) B. then, infer the type of (which is )

now combine those into the final record type:

Type theorists have a notation for that sort of reasoning process, which looks like this:

That is known as a "typing derivation" and the way it works is that "outer" reasoning steps (like steps 1 and 2) go on the bottom and "inner" reasoning steps (like steps A and B) go on top. If we take that reasoning process and generalize it to all records we might write something like this:

… which you can read as saying "if you want to infer the type of a record then infer the type of each field and replace each field with its inferred type". In Haskell this would be: infer context (Record fields) = do fieldTypes <- traverse (infer context) fields return (RecordType fieldTypes) … and we can verify this all works in the Haskell REPL: ghci> :set -XOverloadedStrings -XOverloadedLists ghci> infer [] (Record [("name", String "Alice"), ("age", Number 25)]) Right (RecordType (fromList [("age",NumberType),("name",StringType)])) Field access Any programming language worth its salt3 will also support record field access using something like dot notation (e.g. ).

For example, in Nix that would look like this: nix-repl> { name = "Alice"; age = 25; }.name "Alice" So we'll add a type inference rule for field access, but first we need to extend our expression syntax to support dot notation:

… and now we can add this type inference rule:

This says that we can access a field named from an expression if 's inferred type is a record with a field named . The inferred type of the field becomes the inferred type of the field access. The equivalent Haskell code would be something like: data Expression = … | FieldAccess Expression Identifier

…

infer context (FieldAccess expression field) = do expressionType <- infer context expression case expressionType of RecordType fieldTypes -> case Map.lookup field fieldTypes of Just fieldType -> return fieldType Nothing -> Left "missing field" _ -> Left "not a record" This is the first type inference rule we've added that can fail. If we were to infer the type of an expression like then that wouldn't match that type inference rule (or any other rule) so we would reject the expression with a type error ("not a record"). However, the rule would also reject a field access if the field is missing, too. If we were to infer the type of that also doesn't match our type inference rule so we would reject the expression with a type error ("missing field"). Before we move on, let's test out this type inference rule on an example. Suppose that we want to infer the type of this expression:

Our reasoning process might go something like:

to know the type of the field access () I need the type of the record

to know the type of the record I need the type of the field

the type of the field (set to ) is

the type of the record is

the type of the field access () is

… and the equivalent formal derivation would be:

… and we can confirm in Haskell that the

inferred type is indeed : exampleRecord :: Expression exampleRecord = Record [("name", String "Alice"), ("age", Number 25)]

exampleAccess :: Expression exampleAccess = FieldAccess exampleRecord "age" ghci> infer [] exampleAccess Right NumberType Variables You might wonder why we don't just write the rule like this:

In other words, why don't we consult the expression's value instead of the expression's type when inferring the field's type? After all, that would make our reasoning process much more direct for that last example:

to know the type of the field access () I need the type of the field (set to )

the type of is

the type of the field access () is

… and the equivalent formal derivation would also be simpler:

Consulting the value instead of the type would work for our current (incredibly simple) programming language, but would no longer work once we add support for variables because then an expression like this would be rejected:

You can read that as assigning an expression () to a local variable () and then accessing the field from that variable. We can only infer a type for this expression if we consult 's type. We can't consult 's value because right now is just an unevaluated variable (not a record literal). We could evaluate our expression first to get 's value but that would defeat the purpose of type checking: normally you type check an expression before you evaluate the expression in order to catch mistakes before evaluation begins4. On that note, let's go ahead and add variables and variable assignment to our very minimal language:

Now is a valid expression (which evaluates to ) and so is:

… which evaluates to .

Note: I'm not going to spell out the rules for evaluation in this post since I'm just focused on explaining type inference.

The type inference rule for is the first time we'll actually use the context () that we've ignored so far:

This says that in order to infer the type of a expression we need to first infer the type of the right-hand side of each local variable assignment (, , …). We then extend our type inference context () with the inferred type of each assigned local variable () while inferring the type of the final result ().