The context behind this post is that I'm working on a type checker and language server for Nix and there are three features of the language which make it tricky to typecheck (which I'll dub the "three horsemen of Nix type inference"):
- computed imports (imports that depend on values in scope)
1 - computed record
fields and field accesses2
//
(the biased record concatenation operator) which is the subject of this post!
Here "biased record concatenation" means combining two records, preferring fields from one record if they overlap. For example, in Nix the //
operator prefers fields from the right record in case of overlap:
nix-repl> { x = 1; y = 2; } // { y = true; z = "hi"; }
{ x = 1; y = true; z = "hi"; }
The good news is that type inference for biased record concatenation is not a research problem because the algorithm was published in 1991 as Type inference for record concatenation and multiple inheritance by Mitchell Wand (henceforth "the Wand paper"). The bad news is that as far as I can tell no language in existence implements the type inference algorithm described in that paper, so even though it's not a research problem it's still not a solved problem.
A big reason why is that the paper isn't "easy to mechanize" meaning that it doesn't translate well to code. In this post I hope to fix that by by spelling out a formal algorithm equivalent to the original paper. In particular, I'll formalize the algorithm in three ways:
- a declarative natural deduction semantics
- an algorithmic semantics using constraint generation and resolution
- a reference Haskell implementation (≈400 lines of code)
… and I also published a companion project on GitHub that you can use to test the reference Haskell implementation.
This post builds upon my previous post: Record type inference for dummies. Reading that post will not necessarily prepare you for this post if you're a type theory newcomer, but it will at least help you understand the basic terminology/syntax and also appreciate why this is a challenging problem to solve.
Motivation #
Why do we even want to support type inference for this specific operator? After all, there are variations on this operator that are easier to type check, like a record concatenation operator that rejects conflicting fields. Maybe we should just use something like that instead?
Well, I know that Nix needs this specific operator and not other variations, because this operator (plus recursion) powers Nixpkgs support for "late binding" of dependencies, where you can override a package and all reverse dependencies pick up the overridden package. This is a critical feature in the age of rampant supply chain attacks because you need to be able to patch or upgrade a dependency and ensure that all downstream packages pick up the fixed dependency.
The fundamental reason why the //
operator is tricky to type-check is because late binding is tricky to type-check. We could replace Nix's //
operator with some other operator or language feature, but so long as Nixpkgs needs late binding then type inference will remain tricky.
I'm hoping that this post will not only progress the state-of-the-art for type checking Nix but also pave the way for more typed languages to support the Wand inference algorithm. That way we can get nicer inferred types with smaller constraints requiring fewer annotations.
Prior art #
Currently only one language I'm aware of (PureScript) supports biased record concatenation and also can infer a useful type for this example function (taken from the paper):
… or using Nix syntax:
r: s: (r // s).x + 1
Note that there are a few typed languages that support biased record concatenation:
- Dhall (using the same operator as Nix:
r // s
) - Typescript/Flow (using spread syntax:
{ ...r, ...s }
) - PureScript (using the
)Record.merge
function
… but Dhall, TypeScript, and Flow can only work forwards when performing type inference on this operator, meaning they require concrete types for the two input records (e.g. r
and s
).
For example, in TypeScript if you try to define
function example(r, s): number {
return { ...r, ...s }.x + 1;
};
… the type checker will complain that r
and s
have an inferred type of any
because the type checker cannot work backwards to infer useful types for the inputs.
PureScript is the only language in that list that can infer a useful and general type for that function without any annotation:
-- This type annotation is optional. PureScript already infers this
-- type
example
:: forall a b c d . Union b a c
=> Nub c (x :: Int | d)
=> Record a
-> Record b
-> Int
example r s = (merge s r).x + 1
However, PureScript is not using the approach described in the paper. As I mentioned earlier, no language implements the original paper because it's so loosely formalized, but I hope to fix that by translating the paper into an algorithm that any person (or any coding agent) can methodically translate to code.
Domains #
The Wand paper observes that you can think of a row-polymorphic record type such as this one:
… as a potentially infinite record consisting of explicit fields (potential fields denoted by a "row variable" (might be present, and we'll call those other fields the row variable's "domain".
However, not all row variables are created equal. For example, consider this other record type:
Both same two domains. Specifically,
The Wand paper builds on that idea to note that record unification gets much easier when both records share the same set of explicit fields, because then you only need to handle three cases 3:
Case 0: unifying two closed record types (e.g.) Since both records share the same set of explicit fields you can unify the two record types by unifying their respective field types (e.g.
). - Case 1: unifying two open record types (e.g.) Similar to
Case 0, except we also unify their row variables (e.g.) because they share the same domain. - Case 2, where one record type is open (e.g.) We solve this case by solving
to be the empty set of fields.
Field instantiation - Part 1 #
This means we need some way to fix any two record types to share the same set of explicit fields and we'll call this process field instantiation.
For example, if we were to unify these two record types:
… they start off with a mismatch where only the left record type mentions
Here we've introduced a new bit of syntax, potential field, meaning that we're still not sure whether
We can similarly replace
Now we can unify
Field annotations #
This is where we need to introduce some formal notation for potential fields (henceforth, just "fields"), which can be either
So, for example:
means the record has a field named storing a means the record has no field named means that we don't know whether the field is present or not
We also define
… we would "desugar"
… then desugar
… and then pairwise field unification produces:
… while row unification produces:
… and if we substitute those equations back into our types, we get the following unified type for both records (arbitrarily preferring
… which we can "resugar" to:
What would happen, though, if we were to unify two closed record types like these:
Well, we'd still make them agree on their explicit fields, but since the right record type is closed we have no potential fields to draw upon, so we can only introduce an
Then if we were to desugar the left record type:
… we would get an irreconcilable mismatch because we can't unify
Constraints #
Now let's revisit the same example from before:
What type should we infer for that example?
Before we dive into formal notation, let's think out loud in English. The part we know for sure is:
and must be records (since we concatenate them using ) must be a record field storing a (since we add to it)
… but we don't know which record both records (in which case we'd source the
The Wand inference algorithm handles this uncertainty by producing a type alongside a constraint (similar to PureScript). The base type the paper would infer (adapted to the notation I'm using in this post) would be:
… which says that our function's inputs are both records, each of which may or may not have an
Additionally, the Wand algorithm would generate a constraint saying:
…which you can read as saying that our
We could even present that constraint to the end user as part of the inferred type, like this:
However, I'm not really a fan of that notation and in this post I will propose a simpler notation for constraints, not just to shorten the type signature but also to support an algorithm that's easier to mechanize.
Field concatenation #
The notation I'll propose is to define a new type-level operator that "merges" two fields:
Specifically, this operator returns the right-most field that is
You can think of this operator as analogous to the types instead of field values.
This operator simplifies constraints quite a bit. For example, we can use this operator to simplify the inferred type of
… which is equivalent to the type the Wand algorithm infers.
Proof:is true if and only if is true, which you can demonstrate by computing a truth table for both constraints ranging over all nine permutations of where .
Now, there are multiple ways we could model this operator in our formal semantics. One approach is to define this operator as another type of field:
I'm not a fan of that approach because this is not a canonical representation for a field, meaning that our abstract syntax lets us represent the same field in multiple ways. For example, under this approach
A canonical representation is one in which every field has a unique syntactic representation and in my experience canonical representations promote simpler algorithms (and proofs). A better (canonical) way to represent fields while still supporting field concatenation is:
Here I've introduced a new bit of notation: the bar above
In this representation, might have type might be absent, unless a field variable in
We'll also add a little bit of syntactic sugar and write
Using Haskell code this would look like:
newtype Variable = ID Int
data Field
= Present Type [Variable]
-- ^ We haven't defined Type yet, but we're about to
| Absent [Variable]
present :: Type -> Field
present fieldType = Present fieldType []
absent :: Field
absent = Absent []
Now let's define
This definition obeys the following algebraic properties (monoid laws):
… and the proof of the monoid laws is included in the Appendix.
Conceptually, this canonical representation keeps track of the right-most
This representation also gives us a simple algorithm for field equality: two fields are equal if their canonical representations are equal.
For example,
In Haskell we'll use use the Semigroup
append operator, (<>)
, as the Haskell analog of
instance Semigroup Field where
_ <> Present a gs = Present a gs
Present a fs <> Absent gs = Present a (fs ++ gs)
Absent fs <> Absent gs = Absent (fs ++ gs)
instance Monoid Field where
mempty = Absent []
We can also define a convenience function to merge zero or more fields into a single field:
… which in Haskell is just mconcat
(the function that flattens a list into a single value using mempty
and (<>)
):
mergeFields :: [Field] -> Field
mergeFields = mconcat
Treating
… because there we can desugar
… which evaluates to:
… and we can resugar that to the shorthand version:
… which we can read as saying "either
Row concatenation #
We'll restructure row variables in a similar way, but we first need to introduce an abstract syntax for types:
… which in Haskell would be:
import Data.Map (Map)
newtype Identifier = Identifier Text
newtype Variable = ID Int
newtype Row = Row [Variable]
data Type
= BooleanType
| StringType
| NumberType
| RecordType (Map Identifier Field) Row
| FunctionType Type Type
| VariableType Variable
If you read my previous post on record type inference you can see that this is similar to before with a few differences:
the syntax for each field type changed from
toThis means that we can now mark fields explicitly absent (using
) or specify that we're not sure if a field is present (using ). However, we can still use as a shorthand for , though, so this syntax is a superset of our old syntax. - record types now include
0 or more row variablesTraditional type inference algorithms for row polymorphism let a record have
at most one row variable, but this representation lets us havemore than one row variable. These extra row variables reduce the number of constraints our type inference algorithm needs to track.
Now we can define an operator on rows that merges them:
… and the implementation of this operator is very simple:
instance Semigroup Row where
Row ps0 <> Row ps1 = Row (ps0 ++ ps1)
instance Monoid Row where
mempty = Row []
… or we could have just done:
newtype Row = Row [Variable]
deriving newtype (Semigroup, Monoid)
In other words, this operator literally just concatenates the two lists of row variables. It's hardly even worth defining the
Syntax #
Now I can formalize the full algorithm, which is based on the following abstract syntax for lambda calculus supplemented with record operations, addition, and scalar values: