Record type inference for dummies

A developer explains the basics of type inference for anonymous records, arguing that good type inference for such records is a key missing feature in statically typed languages. The post introduces type theory notation and inference rules for record types, aiming to bridge the gap between programming language experts and lay programmers.

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 languages 1 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 https://xkcd.com/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": js { :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 - a e.g. - a e.g. - a record containing 0 or more fields e.g. The way we would write that 2 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 salt 3 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 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 However, the rule would also reject a field access if the field is missing, too. If we were to infer the type of 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 - the type of the record is - to know the type of the record I need the type of the - 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 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 We can't consult could evaluate our expression first to get before you evaluate the expression in order to catch mistakes before evaluation begins 4. On that note, let's go ahead and add variables and variable assignment to our very minimal language: Now … 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 This says that in order to infer the type of a data Expression = … | Let Identifier, Expression Expression … infer context Let expression = do infer context expression infer context Let x, assignment : assignments expression = do assignmentType <- infer context assignment infer x, assignmentType : context Let assignments expression This rule pairs with the type inference rule for variables, which is: … which you can read as saying "to infer the type of a variable named data Expression = … | Variable Identifier infer context Variable identifier = do case lookup identifier context of Just assignmentType - return assignmentType Nothing - Left "unbound variable" Armed with those two new rules we can now write out a typing derivation to infer the type of our earlier example: This is essentially saying: has type because… has type because … has type - … therefore has type - … therefore has type … and we can confirm that in Haskell, too: exampleLet :: Expression exampleLet = Let "r", Record "x", Number 1 FieldAccess Variable "r" "x" ghci infer exampleLet Right NumberType Functions If that's all our programming language needed then type inference for anonymous records would be easy and most statically typed programming languages would support anonymous records. However, every programming language also supports functions and that's where type inference begins to get tricky. To see why, consider this TypeScript function: js const getName = person = person.name; … which in the lambda calculus would be written as getName = person: person.name; What type would we infer for the function In order to answer that question we need to first extend our syntax to use … and we also need to add a new syntax for function types: … where Then we can add a type inference rule for functions: This is the first type inference rule we've written that can't just be directly translated to Haskell code as written it is possible to codify using unification https://en.wikipedia.org/wiki/Unification computer science Application: type inference or similar, but that's outside the scope of this post . However, you can read that rule as saying that Even without code, we can still use that rule to reason through what the type for In other words, However, this is not exactly the type most programming languages would infer or expect. Specifically, most programming languages do not support an ellipsis like Subtyping Some statically typed programming languages like TypeScript treat a record type like Under this approach the ellipsis is redundant because all record types have an implied ellipsis. That means that in TypeScript you can write: js const getName = person: { name: string } = person.name; … and getName will still work even if you call it on a larger record e.g. { name: "Alice", age: 25 } 5. This approach works okay, but there is an even better approach for handling extra record fields, which brings us to: Row polymorphism The second approach is that instead of dropping the ellipsis we name the ellipsis, meaning that instead of this: … we write something like this: This is the approach taken by languages like PureScript and Elm, where PureScript will write that type like this: { name :: String | other } … and Elm uses a similar syntax: { other | name : String } This has some nice upsides, which we'll get to in the next section, but first let's formalize what it means to "name the ellipsis". First, we'd create a new class of identifier known as a "row variable" : "Row" is an antiquated name for "a set of fields". Remember that the research into this sort of type inference occurred a long time ago, before JSON even existed. However, the upside of the name is that type theorists get to be a little cheeky and use the greek letter "rho" to represent a "row". Then we'd change the abstract syntax for record types to permit an optional row variable: … and update our type inference rule for field access to use a row variable instead of an ellipsis: This approach of using named ellipses is known as "row polymorphism" because it lets us abstract be "polymorphic" over the set of other fields "row" . Record extension You might wonder: why do we want to abstract over the set of other fields? In particular, why do we need to give a name to these other fields? One reason why is to support our next record operator: record extension. We'll use this syntax: … which you can read as "extend the record So let's add that to our abstract syntax for expressions: Now what type would we infer for a record update? Our first stab at type inference rule might look like this: … but that is not correct because the field