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"):
// (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:
… 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.
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.
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 + 1Note that there are a few typed languages that support biased record concatenation:
r // s){ ...r, ...s })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 + 1However, PureScript is not using the approach described in the paper and I prefer the approach from the paper because it leads to simpler inferred types and constraints. 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.
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 (
However, not all row variables are created equal. For example, consider this other record type:
Both
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 cases3:
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.
Case 2, where one record type is open (e.g.
We solve this case by solving
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,
We can similarly replace
Now we can unify
This is where we need to introduce some formal notation for potential fields (henceforth, just "fields"), which can be either
So, for example:
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
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:
… but we don't know which record
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.
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
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,
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 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 = mconcatTreating
… because there we can desugar
… which evaluates to:
… and we can resugar that to the shorthand version:
… which we can read as saying "either
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 VariableIf 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
This means that we can now mark fields explicitly absent (using
record types now include 0 or more row variables
Traditional type inference algorithms for row polymorphism let a record have at most one row variable, but this representation lets us have more 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
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:
newtype Identifier = Identifier Text
data Expression
= Variable Identifier
| Lambda Identifier Expression
| Apply Expression Expression
| Let Identifier Expression Expression
| Record (Map Identifier Expression)
| FieldAccess Expression Identifier
| FieldExtension Expression Identifier Expression
| FieldRemoval Expression Identifier
| RecordConcatenation Expression Expression
| Addition Expression Expression
| Boolean Bool
| String Text
| Number DoubleWe'll also define a context (
type Context = [(Identifier, Type)]The declarative typing rules in natural deduction form are:
Those rules are simple, but they also leave out a lot of details (like how to unify records, which is the hard part of the algorithm). That's why the rest of the post walks through the algorithmic semantics.
I'll present the algorithmic semantics alongside Haskell code fragments and you can also find the complete Haskell code in the Appendix (and on GitHub) so you don't have to assemble the Haskell code fragments yourself.
The algorithmic semantics differ from the natural deduction semantics by generating constraints as part of unification:
data Constraint
= UnifyTypes Type Type
| UnifyFields Field Field
| UnifyRows Row Row… and our typing judgments now infer a list of constraints in addition to inferring a type:
import Control.Monad.RWS
(RWST(..), MonadReader(..), MonadState(..), MonadWriter(..))
infer
:: ( MonadReader Context m -- Our type checking context
, MonadWriter [Constraint] m -- Accumulated constraints
, MonadState Variable m -- Supply of fresh variables
, MonadError TypeError m -- Type errors if inference fails
)
=> Expression -> m TypeWe then resolve these constraints in a subsequent constraint resolution step.
The algorithmic semantics for constraint generation are very similar to the natural deduction semantics except that wherever we need to guess a type (or field, or row) we generate a fresh type variable (or field variable, or row variable) and any necessary constraints:
The corresponding Haskell implementation is a very direct translation of the typing rules, except I'll use complete words instead of letters to name things:
freshVariable :: MonadState Variable m => m Variable
freshVariable = state (\n -> (n, n + 1))
freshType :: MonadState Variable m => m Type
freshType = do
variable <- freshVariable
return (VariableType variable)
freshField :: MonadState Variable m => m Field
freshField = do
variable <- freshVariable
return (Absent [variable])
freshRow :: MonadState Variable m => m Row
freshRow = do
variable <- freshVariable
return (Row [variable])
unify :: MonadWriter [Constraint] m => Type -> Type -> m ()
unify left right = tell [UnifyTypes left right]
infer
:: ( MonadReader Context m
, MonadWriter [Constraint] m
, MonadState Variable m
, MonadError TypeError m
)
=> Expression -> m Type
infer (Variable identifier) = do
context <- ask
case lookup identifier context of
Just assignmentType ->
return assignmentType
Nothing ->
throwError UnboundVariable
infer (Lambda identifier body) = do
inputType <- freshType
outputType <- local ((identifier, inputType) :) (infer body)
return (FunctionType inputType outputType)
infer (Apply function argument) = do
functionType <- infer function
inputType <- infer argument
outputType <- freshType
unify functionType (FunctionType inputType outputType)
return outputType
infer (Let identifier assignment expression) = do
assignmentType <- infer assignment
local ((identifier, assignmentType) :) (infer expression)
infer (Record fields) = do
fieldTypes <- traverse infer fields
return (RecordType (fmap present fieldTypes) mempty)
infer (FieldAccess record identifier) = do
recordType <- infer record
fieldType <- freshType
row <- freshRow
unify recordType (RecordType [(identifier, present fieldType)] row)
return fieldType
infer (FieldExtension record identifier expression) = do
recordType <- infer record
expressionType <- infer expression
field <- freshField
row <- freshRow
unify recordType (RecordType [(identifier, field)] row)
return (RecordType [(identifier, present expressionType)] row)
infer (FieldRemoval record identifier) = do
recordType <- infer record
field <- freshField
row <- freshRow
unify recordType (RecordType [(identifier, field)] row)
return (RecordType [(identifier, absent)] row)
infer (RecordConcatenation leftRecord rightRecord) = do
leftRecordType <- infer leftRecord
rightRecordType <- infer rightRecord
leftRow <- freshRow
rightRow <- freshRow
unify leftRecordType (RecordType [] leftRow )
unify rightRecordType (RecordType [] rightRow)
return (RecordType [] (leftRow <> rightRow))
infer (Addition leftNumber rightNumber) = do
leftNumberType <- infer leftNumber
rightNumberType <- infer rightNumber
unify leftNumberType NumberType
unify rightNumberType NumberType
return NumberType
infer (Boolean _) = return BooleanType
infer (String _) = return StringType
infer (Number _) = return NumberTypeTo solve these generated constraints, we'll define a solver function, denoted by
… where
In Haskell our solver function's type is:
data Constrained = Constrained [Constraint] Type
solve
:: ( MonadError TypeError m -- Constraint resolution can fail
, MonadState Variable m -- We'll still need fresh variables
)
=> [Constraint] -- "stuck" constraints that cannot be reduced
-> Constrained -- a constrained type to reduce
-> m Constrained -- the final constrained typeThis function will process the constraints one-by-one until reaching the end of the list (the base case), where the solver returns all "stuck" constraints:
solve stuck (Constrained [] _T) = do
return (Constrained stuck _T)Constraints like these are easy to solve:
Our solver just drops those trivial constraints, proceeding to solve the remainder of the constraints:
solve stuck (Constrained (constraint : constraints) _T) = do
let next = Constrained constraints _T
…
case constraint of
UnifyTypes BooleanType BooleanType -> solve stuck next
UnifyTypes StringType StringType -> solve stuck next
UnifyTypes NumberType NumberType -> solve stuck next
…We can also unify two function types by unifying their inputs and outputs:
… and unify two present fields (with no field variables) by unifying their types:
solve stuck (Constrained (constraint : constraints) _T) = do
…
case constraint of
…
UnifyTypes (FunctionType _A0 _B0) (FunctionType _A1 _B1) -> do
let newConstraints =
UnifyTypes _A0 _A1
: UnifyTypes _B0 _B1
: constraints
solve stuck (Constrained newConstraints _T)
UnifyFields (Present _A0 []) (Present _A1 []) -> do
let newConstraints = UnifyTypes _A0 _A1 : constraints
solve stuck (Constrained newConstraints _T)The next few cases for our solver will cover substitution for types, rows, and fields. For example, if we unify a type variable with a type (e.g.
This means we need to define a function to substitute a type
… such that:
Note that the above definition also requires also defining type substitution on fields (e.g.
In fact, we can keep overloading this function to also work on constraints:
… and constrained types, too:
However, for future similar functions I'll skip these sorts of tedious overloaded definitions and only define the most interesting cases (typically the base case).
The Haskell version of type substitution is:
import Data.Data.Lens (biplate)
import qualified Control.Lens as Lens
substituteType :: Variable -> Type -> Type -> Type
substituteType a _A (VariableType a')
| a == a' = _A
| otherwise = VariableType a'
substituteType a _A (FunctionType _B0 _C0) = FunctionType _B1 _C1
where
_B1 = substituteType a _A _B0
_C1 = substituteType a _A _C0
substituteType a _A (RecordType fields _P) =
RecordType (Lens.over biplate (substituteType a _A) fields) _P
substituteType _ _ BooleanType = BooleanType
substituteType _ _ StringType = StringType
substituteType _ _ NumberType = NumberTypeIf you're wondering what this is about:
substituteType a _A (RecordType fields _P) =
RecordType (Lens.over biplate (substituteType a _A) fields) _PHere we're making use of a clever trick so that we don't need to write multiple overloaded definitions of the same function. If we use the biplate optic from Haskell's lens package then we can automatically overload substituteType to work on any type that may have Types stored somewhere inside of it. In the above Haskell snippet we don't need to define a separate version of this function that works on fields; instead, the code uses Lens.over biplate to lift our substituteType function to transform every Type inside of fields.
We also need our solver to substitute rows, so we'll define a row substitution function:
… that substitutes a row
substituteRow :: Variable -> Row -> Row -> Row
substituteRow p (Row ps) (Row ps') = Row (concatMap replace ps')
where
replace p' = if p == p' then ps else [p']Similar to before, we'll overload this row substitution function to also work on types, fields, constraints, and constrained types, but this time I won't spell out those cases.
The substitution function for fields is the trickiest one:
… but we can make use of the earlier
In other words, we split a field into chunks delimited by
substituteField :: Variable -> Field -> Field -> Field
substituteField f _F field =
mconcat (List.intersperse _F (chunks field))
where
chunks (Present _A fs) =
case List.break (== f) fs of
(_, []) ->
[Present _A fs]
(prefix, _ : suffix) ->
Present _A prefix : chunks (Absent suffix)
chunks (Absent fs) =
case List.break (== f) fs of
(_, []) ->
[Absent fs]
(prefix, _ : suffix) ->
Absent prefix : chunks (Absent suffix)Now we can use these three substitution functions to solve constraints where one or the other side is a variable:
There are also symmetric rules for the constraints
occursCheck :: MonadError TypeError m => Variable -> Variable -> m ()
occursCheck a b
| a == b = throwError OccursCheckFailed
| otherwise = return ()
…
solve stuck (Constrained (constraint : constraints) _T) = do
let other = Constrained (stuck ++ constraints) _T
…
case constraint of
…
UnifyTypes (VariableType a) _A -> do
Lens.traverseOf_ biplate (occursCheck a) _A
solve [] (Lens.over biplate (substituteType a _A) other)
UnifyRows (Row [p]) _P -> do
Lens.traverseOf_ biplate (occursCheck p) _P
solve [] (Lens.over biplate (substituteRow p _P) other)
UnifyFields (Absent [f]) _F -> do
Lens.traverseOf_ biplate (occursCheck f) _F
solve [] (Lens.over biplate (substituteField f _F) other)
…Carefully note that our solver needs to perform substitution on all other constraints in the list, including the stuck ones, since they might no longer be stuck after substitution.
The above Haskell snippet demonstrates another useful application of biplate: we can write an occursCheck that just works on Variables and automatically lift it to work on types, rows, and fields.
If a constraint unifies any row (
deleteRow :: Row -> Row -> Row
deleteRow (Row _P) (Row _Q) = Row (_Q \\ _P)… and overload that function to work on constrained types so that we can solve a constraint with an empty row:
solve stuck (Constrained (constraint : constraints) _T) = do
let other = Constrained (stuck ++ constraints) _T
…
case constraint of
…
UnifyRows (Row []) _P -> do
solve [] (Lens.over biplate (deleteRow _P) other)Similarly, if a constraint unifies zero or more field variables with an empty field (i.e.
deleteFields :: [Variable] -> Field -> Field
deleteFields fs (Present _A gs) = Present _A (gs \\ fs)
deleteFields fs (Absent gs) = Absent (gs \\ fs)… and then overload that function to solve constraints with an empty field:
solve stuck (Constrained (constraint : constraints) _T) = do
let other = Constrained (stuck ++ constraints) _T
…
case constraint of
…
UnifyFields (Absent []) (Absent fs) -> do
solve [] (Lens.over biplate (deleteFields fs) other)Robert Virding, who developed Erlang with me, was famed for his comment. … Singular. The entire stuff he wrote had one comment in the middle of the pattern matching compiler. There was a single line that said "and now for the tricky bit". - Joe Armstrong, The Mess We're In
Field instantiation is the "tricky bit" of this algorithm, so I'll go a bit slower here.
I can explain the interesting part by revisiting the original pathological example:
If we run that through constraint generation we will generate the following constrained type:
Our solver would then drop the trivial
… which would leave us with this simpler constrained type:
But how do we solve that last remaining constraint?
Earlier we said we need to fix field mismatches when unifying record types, but we can't use the same trick as before because the record type on the right has not one but two row variables. If the right record had just one field variable:
… then we could replace
… and then we could easily unify the two fields and the two rows. However, our record type has two row variables so we can't use the same trick … or can we?
Well, let's go back to the constrained type with two "sibling" row variables:
… and think through what would happen if we were to:
We can't perform either of those two substitutions individually, but we can perform them both simultaneously, and if we do so we get the following new constrained type:
… and now the fields and rows line up so we can decompose that type constraint into a field constraint and a row constraint:
… and then substitution solves the second constraint, leaving us with the same type as before (just with different variable names):
There are some limitations on the above trick, though. Specifically, we can only instantiate row variables within a record type subject to the following conditions:
we must instantiate all row variables within a record type simultaneously
This is because before instantiation every "sibling" row variable within a record type ranges over the same domain (the same potentially infinite set of fields) and if you instantiate some but not all of the row variables then you end up with siblings with mismatched domains.
we must instantiate the same set of fields for each row variable within a record type
If we instantiate different fields for sibling row variables then we end up with same domain mismatch problem.
I'll call the above two conditions the "domain conditions".
Actually, it's a bit more complicated than that because sibling row variables also show up in row constraints, too! For example, if we were solving a constrained type like:
… then to solve the first constraint we'd need to instantiate the field
We would do so by performing three simultaneous substitutions:
… and that would replace the
… leaving us with the following constrained type where all sibling row variables still share the same domain:
… and then the constraint solver would reduce that further to:
So let's go back and fix our two domain conditions to take row constraints into account:
we must instantiate all sibling row variables within a record type or row constraint simultaneously
we must instantiate the same set fields for each sibling row variable within a record type or row constraint
In fact, if we obey these two rules then field instantiation never needs to generate fresh row variables. We can reuse the old ones, but treat them all as having a new domain.
That means in the above example, we can reuse
We're going to need an efficient way to detect sibling row variables in order to satisfy those domain conditions. Fortunately, there's already a well-understood data structure for this purpose, which is a disjoint set. In fact, this data structure is already used quite heavily by many type checkers (where it's more commonly known as a union-find data structure).
As the name suggests, a disjoint set stores an outer set of pairwise disjoint inner sets (a.k.a. "partitions"). We'll use these disjoint partitions to represent sets of row variables that are linked via sibling relationships.
Disjoint sets efficiently support the following operations we need for this algorithm:
We'll use
Since all row variables in a row are siblings then our partition function converts any row into a disjoint set with a single partition:
Similarly, the disjoint set of a row constraint is a single partition linking all row variables from both rows together:
… and for all other constraints we partition both sides of the constraint and merge the two disjoint sets (which we'll denote using
Then we can continue overloading our partition function to work on types:
… fields:
… and constrained types:
For the Haskell implementation I used the disjoint-containers package which provides a DisjointSet type supporting these operations:
mempty (from the Monoid class) is the empty disjoint set(<>) (from the Semigroup class) merges two disjoint setssingletons converts any set into a disjoint set with a single partitionequivalences queries which partitions overlap with a given elementlinkRow :: Row -> DisjointSet Variable
linkRow (Row _P) = DisjointSet.singletons (Set.fromList _P)
linkConstraint :: Constraint -> DisjointSet Variable
linkConstraint (UnifyRows _P _Q) = linkRow (_P <> _Q)
linkConstraint other = Lens.foldMapOf biplate linkRow other
linkConstrainedType :: Constrained -> DisjointSet Variable
linkConstrainedType constrained = linkedRows <> linkedConstraints
where
linkedRows =
Lens.foldMapOf biplate linkRow constrained
linkedConstraints =
Lens.foldMapOf biplate linkConstraint constrained
equivalences :: Row -> DisjointSet Variable -> Row
equivalences (Row []) _ =
mempty
equivalences (Row (x : _)) disjointSet =
Row (Set.toList (DisjointSet.equivalences x disjointSet))Once we can identify all linked row variables then we can simultaneously instantiate them all, which we'll do using a family of field instantiation functions. This part is going to be the most tedious section to implement because this time we can't just define a single function and overload that function to work on everything.
First, we'll model a primitive instantiation (
type Instantiation = Variable -> Map Identifier FieldThen we'll define a function to lift instantiation to operate on a row (denoted
instantiateRow :: Instantiation -> Row -> Map Identifier Field
instantiateRow sigma (Row ps) = Map.unionsWith (<>) (map sigma ps)Now we define a function to instantiate a type (denoted
instantiateType :: (Variable -> Map Identifier Field) -> Type -> Type
instantiateType sigma (RecordType xs0 _P) = RecordType (xs1 <> ys) _P
where
xs1 = Lens.over biplate (instantiateType sigma) xs0
ys = instantiateRow sigma _P… and the other cases are just simple recursion:
instantiateType sigma (FunctionType _A0 _B0) = FunctionType _A1 _B1
where
_A1 = instantiateType sigma _A0
_B1 = instantiateType sigma _B0
instantiateType _ (VariableType a) = VariableType a
instantiateType _ BooleanType = BooleanType
instantiateType _ StringType = StringType
instantiateType _ NumberType = NumberTypeNext we'll need a function that instantiates constraints (denoted
… and the other cases are just simple recursion:
instantiateConstraints :: Instantiation -> [Constraint] -> [Constraint]
instantiateConstraints sigma = concatMap instantiateConstraint
where
instantiateConstraint (UnifyRows _P _Q) =
Map.elems (Map.intersectionWith UnifyFields fs0 fs1)
where
fs0 = instantiateRow sigma _P
fs1 = instantiateRow sigma _Q
instantiateConstraint (UnifyFields _F0 _G0) =
[ UnifyFields _F1 _G1 ]
where
_F1 = Lens.over biplate (instantiateType sigma) _F0
_G1 = Lens.over biplate (instantiateType sigma) _G0
instantiateConstraint (UnifyTypes _A0 _B0) =
[ UnifyTypes _A1 _B1 ]
where
_A1 = instantiateType sigma _A0
_B1 = instantiateType sigma _B0Finally, we can implement a function for instantiating constrained types (denoted
instantiateConstrained
:: (Variable -> Map Identifier Field) -> Constrained -> Constrained
instantiateConstrained sigma (Constrained _C0 _T0) = Constrained _C1 _T1
where
_C1 = instantiateConstraints sigma _C0
_T1 = instantiateType sigma _T0Phew! What a bear to spell out all of that.
Now we can get to the "fun" part and specify the constraint resolution rules for record unification. The simplest rule unifies two record types that share the same fields, which we can solve by unifying their rows and respective fields:
solve stuck (Constrained (constraint : constraints) _T) = do
…
case constraint of
…
UnifyTypes (RecordType xs0 _P) (RecordType xs1 _Q)
| Map.keysSet xs0 == Map.keysSet xs1 -> do
let newConstraints =
UnifyRows _P _Q
: Map.elems (Map.intersectionWith UnifyFields xs0 xs1)
++ constraints
solve stuck (Constrained newConstraints _T)
| Row [] <- _PThe next rules all cover the case where there is a field mismatch, meaning the two records might share some fields in common (
If there is a field mismatch and both records are closed then we:
solve stuck (Constrained (constraint : constraints) _T) = do
…
case constraint of
…
UnifyTypes (RecordType xs0 _P) (RecordType xs1 _Q)
…
| Row [] <- _P
, Row [] <- _Q -> do
let ys = Map.difference xs0 xs1
let zs = Map.difference xs1 xs0
let newConstraints =
Map.elems (Map.intersectionWith UnifyFields xs0 xs1)
<> [ UnifyFields _G absent | _G <- Map.elems ys ]
<> [ UnifyFields absent _H | _H <- Map.elems zs ]
<> constraints
solve stuck (Constrained newConstraints _T)If there's a field mismatch and only one of the records is closed (e.g.
Here we'll use
solve stuck (Constrained (constraint : constraints) _T) = do
let other = Constrained (stuck ++ constraints) _T
let everything = Constrained (constraint : stuck ++ constraints) _T
…
case constraint of
…
UnifyTypes (RecordType xs0 _P) (RecordType xs1 _Q)
…
| Row [] <- _P -> do
let ys = Map.difference xs0 xs1
let zs = Map.difference xs1 xs0
let _S = linkConstrainedType everything
let toEntry q = do
freshFields <- traverse (\_ -> freshField) ys
return (q, freshFields)
let Row qs = equivalences _Q _S
entries <- traverse toEntry qs
let table = Map.fromList entries
let sigma p = Map.findWithDefault Map.empty p table
let absents = fmap (\_ -> absent) zs
let prefix =
instantiateConstraints
sigma
[ UnifyTypes
(RecordType (xs0 <> absents) _P)
(RecordType xs1 _Q)
]
let Constrained suffix _T1 =
instantiateConstrained sigma other
solve [] (Constrained (prefix <> suffix) _T1)The last rule covers the case where there is a field mismatch and both records are open, where we:
solve stuck (Constrained (constraint : constraints) _T) = do
let everything = Constrained (constraint : stuck ++ constraints) _T
…
case constraint of
…
UnifyTypes (RecordType xs0 _P) (RecordType xs1 _Q)
…
| otherwise -> do
let ys = Map.difference xs0 xs1
let zs = Map.difference xs1 xs0
let _S = linkConstrainedType everything
let toEntry fs p = do
freshFields <- traverse (\_ -> freshField) fs
return (p, freshFields)
let Row ps = equivalences _P _S
let Row qs = equivalences _Q _S
entries0 <- traverse (toEntry ys) qs
entries1 <- traverse (toEntry zs) ps
let table = Map.fromList (entries0 ++ entries1)
let sigma p = Map.findWithDefault Map.empty p table
solve [] (instantiateConstrained sigma everything)… and that's it. That's the complete logic for unifying record types.
There are two cases where constraint resolution produces an error:
solve stuck (Constrained (constraint : constraints) _T) = do
…
case constraint of
…
-- Type mismatch fallthrough case
UnifyTypes left right -> do
throwError (TypeMismatch left right)
-- Field mismatch
UnifyFields (Present _ _) (Absent []) -> do
throwError FieldMismatch
UnifyFields (Absent []) (Present _ _) -> do
throwError FieldMismatchSome constraints (like
In Haskell we add any constraints we can't solve yet to the list of stuck constraints and keep going:
solve stuck (Constrained (constraint : constraints) _T) = do
…
case constraint of
…
UnifyRows _ _ -> do
solve (constraint : stuck) next
UnifyFields _ _ -> do
solve (constraint : stuck) next… and that completes the implementation of our solver!
Finally, the Haskell implementation ties everything together by generating constraints, and then solving the generated constraints:
run :: Expression -> Either TypeError Constrained
run expression = do
(constrained, _, _) <- runExcept (runRWST inference [] 0)
return constrained
where
inference = do
(type_, constraints) <- listen (infer expression)
solve [] (Constrained constraints type_)Normally this would be clumsy to test in a Haskell REPL because you'd have to read and write syntax trees:
ghci> run (Lambda "r" (Lambda "s" (Addition (FieldAccess (RecordConcatenation (Variable "r") (Variable "s")) "x") (Number 1))))
Right (Constrained [UnifyFields (Absent [6,7]) (Present NumberType [])] (FunctionType (RecordType (fromList [("x",Absent [6])]) (Row [2])) (FunctionType (RecordType (fromList [("x",Absent [7])]) (Row [3])) NumberType)))Fortunately, you don't need to do that, though, because I also included a companion project for this post on GitHub that wraps the core implementation in a simple REPL that parses Nix-like expressions and pretty-prints the inferred type:
>>> r: r.x + 1
{ x : Number, c } -> NumberFor example, if we input the original pathological expression the type checker infers the correct constrained type:
>>> r: s: (r // s).x + 1
(g h = present Number) => { x ? g, c } -> { x ? h, d } -> NumberAlso, if we change that expression to drop the x field from the right
record then the type inference algorithm correctly deduces that the Number has
to come from the left record:
>>> r: s: (r // (s without x)).x + 1
{ x : Number, e } -> { x ? c, f } -> Number… and if we drop the x field from both records then type inference fails:
>>> r: s: ((r without x) // (s without x)).x + 1
Field mismatchHere are some other example expressions and their inferred types:
>>> woman: woman with queen = true
{ queen ? b, c } -> { queen : Boolean, c }
>>> woman: woman // { queen = true; }
{ queen ? d, b } -> { queen : Boolean, b }>>> r: r with x = r.x + 1
{ x : Number, e } -> { x : Number, e }>>> r: s: let m = r // s; in { x = m.x; other = m without x; }
(i j = present g) =>
{ x ? i, c } ->
{ x ? j, d } ->
{ other : { x ? absent, c d }, x : g }{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedLists #-}
import Control.Monad.Except (MonadError(..), runExcept)
import Data.Data (Data)
import Data.Data.Lens (biplate)
import Data.DisjointSet (DisjointSet)
import Data.List ((\\))
import Data.Map (Map)
import Data.Text (Text)
import Data.String (IsString)
import Control.Monad.RWS
(RWST(..), MonadReader(..), MonadState(..), MonadWriter(..))
import qualified Control.Lens as Lens
import qualified Data.DisjointSet as DisjointSet
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
newtype Identifier = Identifier Text
deriving stock (Data)
deriving newtype (Eq, Ord, IsString, Show)
data Expression
= Variable Identifier
| Lambda Identifier Expression
| Apply Expression Expression
| Let Identifier Expression Expression
| Record (Map Identifier Expression)
| FieldAccess Expression Identifier
| FieldExtension Expression Identifier Expression
| FieldRemoval Expression Identifier
| RecordConcatenation Expression Expression
| Addition Expression Expression
| Boolean Bool
| String Text
| Number Double
deriving stock (Show)
newtype Variable = ID Int
deriving stock (Data)
deriving newtype (Eq, Ord, Num, Show)
data Field = Present Type [Variable] | Absent [Variable]
deriving stock (Data, Show)
present :: Type -> Field
present fieldType = Present fieldType []
absent :: Field
absent = Absent []
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
newtype Row = Row [Variable]
deriving newtype (Monoid, Semigroup)
deriving stock (Data, Show)
data Type
= BooleanType
| StringType
| NumberType
| RecordType (Map Identifier Field) Row
| FunctionType Type Type
| VariableType Variable
deriving stock (Data, Show)
type Context = [(Identifier, Type)]
data TypeError
= UnboundVariable Identifier
| OccursCheckFailed
| TypeMismatch Type Type
| FieldMismatch
deriving stock (Show)
data Constraint
= UnifyTypes Type Type
| UnifyFields Field Field
| UnifyRows Row Row
deriving stock (Data, Show)
data Constrained = Constrained [Constraint] Type
deriving stock (Data, Show)
freshVariable :: MonadState Variable m => m Variable
freshVariable = state (\n -> (n, n + 1))
freshType :: MonadState Variable m => m Type
freshType = do
variable <- freshVariable
return (VariableType variable)
freshField :: MonadState Variable m => m Field
freshField = do
variable <- freshVariable
return (Absent [variable])
freshRow :: MonadState Variable m => m Row
freshRow = do
variable <- freshVariable
return (Row [variable])
unify :: MonadWriter [Constraint] m => Type -> Type -> m ()
unify left right = tell [UnifyTypes left right]
infer
:: ( MonadReader Context m
, MonadWriter [Constraint] m
, MonadState Variable m
, MonadError TypeError m
)
=> Expression -> m Type
infer (Variable identifier) = do
context <- ask
case lookup identifier context of
Just assignmentType ->
return assignmentType
Nothing ->
throwError (UnboundVariable identifier)
infer (Lambda identifier body) = do
inputType <- freshType
outputType <- local ((identifier, inputType) :) (infer body)
return (FunctionType inputType outputType)
infer (Apply function argument) = do
functionType <- infer function
inputType <- infer argument
outputType <- freshType
unify functionType (FunctionType inputType outputType)
return outputType
infer (Let identifier assignment expression) = do
assignmentType <- infer assignment
local ((identifier, assignmentType) :) (infer expression)
infer (Record fields) = do
fieldTypes <- traverse infer fields
return (RecordType (fmap present fieldTypes) mempty)
infer (FieldAccess record identifier) = do
recordType <- infer record
fieldType <- freshType
row <- freshRow
unify recordType (RecordType [(identifier, present fieldType)] row)
return fieldType
infer (FieldExtension record identifier expression) = do
recordType <- infer record
expressionType <- infer expression
field <- freshField
row <- freshRow
unify recordType (RecordType [(identifier, field)] row)
return (RecordType [(identifier, present expressionType)] row)
infer (FieldRemoval record identifier) = do
recordType <- infer record
field <- freshField
row <- freshRow
unify recordType (RecordType [(identifier, field)] row)
return (RecordType [(identifier, absent)] row)
infer (RecordConcatenation leftRecord rightRecord) = do
leftRecordType <- infer leftRecord
rightRecordType <- infer rightRecord
leftRow <- freshRow
rightRow <- freshRow
unify leftRecordType (RecordType [] leftRow )
unify rightRecordType (RecordType [] rightRow)
return (RecordType [] (leftRow <> rightRow))
infer (Addition leftNumber rightNumber) = do
leftNumberType <- infer leftNumber
rightNumberType <- infer rightNumber
unify leftNumberType NumberType
unify rightNumberType NumberType
return NumberType
infer (Boolean _) = return BooleanType
infer (String _) = return StringType
infer (Number _) = return NumberType
occursCheck :: MonadError TypeError m => Variable -> Variable -> m ()
occursCheck a b
| a == b = throwError OccursCheckFailed
| otherwise = return ()
substituteType :: Variable -> Type -> Type -> Type
substituteType a _A (VariableType a')
| a == a' = _A
| otherwise = VariableType a'
substituteType a _A (FunctionType _B0 _C0) = FunctionType _B1 _C1
where
_B1 = substituteType a _A _B0
_C1 = substituteType a _A _C0
substituteType a _A (RecordType fields _P) =
RecordType (Lens.over biplate (substituteType a _A) fields) _P
substituteType _ _ BooleanType = BooleanType
substituteType _ _ StringType = StringType
substituteType _ _ NumberType = NumberType
deleteRow :: Row -> Row -> Row
deleteRow (Row _P) (Row _Q) = Row (_Q \\ _P)
substituteRow :: Variable -> Row -> Row -> Row
substituteRow p (Row ps) (Row ps') = Row (concatMap replace ps')
where
replace p' = if p == p' then ps else [p']
deleteFields :: [Variable] -> Field -> Field
deleteFields fs (Present _A gs) = Present _A (gs \\ fs)
deleteFields fs (Absent gs) = Absent (gs \\ fs)
substituteField :: Variable -> Field -> Field -> Field
substituteField f _F field =
mconcat (List.intersperse _F (chunks field))
where
chunks (Present _A fs) =
case List.break (== f) fs of
(_, []) ->
[Present _A fs]
(prefix, _ : suffix) ->
Present _A prefix : chunks (Absent suffix)
chunks (Absent fs) =
case List.break (== f) fs of
(_, []) ->
[Absent fs]
(prefix, _ : suffix) ->
Absent prefix : chunks (Absent suffix)
linkRow :: Row -> DisjointSet Variable
linkRow (Row _P) = DisjointSet.singletons (Set.fromList _P)
linkConstraint :: Constraint -> DisjointSet Variable
linkConstraint (UnifyRows _P _Q) = linkRow (_P <> _Q)
linkConstraint other = Lens.foldMapOf biplate linkRow other
linkConstrainedType :: Constrained -> DisjointSet Variable
linkConstrainedType constrained = linkedRows <> linkedConstraints
where
linkedRows =
Lens.foldMapOf biplate linkRow constrained
linkedConstraints =
Lens.foldMapOf biplate linkConstraint constrained
equivalences :: Row -> DisjointSet Variable -> Row
equivalences (Row []) _ =
mempty
equivalences (Row (x : _)) disjointSet =
Row (Set.toList (DisjointSet.equivalences x disjointSet))
type Instantiation = Variable -> Map Identifier Field
instantiateRow :: Instantiation -> Row -> Map Identifier Field
instantiateRow sigma (Row ps) = Map.unionsWith (<>) (map sigma ps)
instantiateType :: Instantiation -> Type -> Type
instantiateType sigma (RecordType xs0 _P) = RecordType (xs1 <> ys) _P
where
xs1 = Lens.over biplate (instantiateType sigma) xs0
ys = instantiateRow sigma _P
instantiateType sigma (FunctionType _A0 _B0) = FunctionType _A1 _B1
where
_A1 = instantiateType sigma _A0
_B1 = instantiateType sigma _B0
instantiateType _ (VariableType a) = VariableType a
instantiateType _ BooleanType = BooleanType
instantiateType _ StringType = StringType
instantiateType _ NumberType = NumberType
instantiateConstraints :: Instantiation -> [Constraint] -> [Constraint]
instantiateConstraints sigma = concatMap instantiateConstraint
where
instantiateConstraint (UnifyRows _P _Q) =
Map.elems (Map.intersectionWith UnifyFields fs0 fs1)
where
fs0 = instantiateRow sigma _P
fs1 = instantiateRow sigma _Q
instantiateConstraint (UnifyFields _F0 _G0) = [ UnifyFields _F1 _G1 ]
where
_F1 = Lens.over biplate (instantiateType sigma) _F0
_G1 = Lens.over biplate (instantiateType sigma) _G0
instantiateConstraint (UnifyTypes _A0 _B0) = [ UnifyTypes _A1 _B1 ]
where
_A1 = instantiateType sigma _A0
_B1 = instantiateType sigma _B0
instantiateConstrained :: Instantiation -> Constrained -> Constrained
instantiateConstrained sigma (Constrained _C0 _T0) = Constrained _C1 _T1
where
_C1 = instantiateConstraints sigma _C0
_T1 = instantiateType sigma _T0
solve
:: (MonadError TypeError m, MonadState Variable m)
=> [Constraint] -> Constrained -> m Constrained
solve stuck (Constrained [] _T) = do
return (Constrained stuck _T)
solve stuck (Constrained (constraint : constraints) _T) = do
let other = Constrained (stuck ++ constraints) _T
let next = Constrained constraints _T
let everything = Constrained (constraint : stuck ++ constraints) _T
case constraint of
UnifyTypes BooleanType BooleanType -> solve stuck next
UnifyTypes StringType StringType -> solve stuck next
UnifyTypes NumberType NumberType -> solve stuck next
UnifyTypes (FunctionType _A0 _B0) (FunctionType _A1 _B1) -> do
let newConstraints =
(UnifyTypes _A0 _A1: UnifyTypes _B0 _B1 : constraints)
solve stuck (Constrained newConstraints _T)
UnifyFields (Present _A0 []) (Present _A1 []) -> do
let newConstraints = UnifyTypes _A0 _A1 : constraints
solve stuck (Constrained newConstraints _T)
UnifyTypes (VariableType a) _A -> do
Lens.traverseOf_ biplate (occursCheck a) _A
solve [] (Lens.over biplate (substituteType a _A) other)
UnifyTypes _A (VariableType a) -> do
Lens.traverseOf_ biplate (occursCheck a) _A
solve [] (Lens.over biplate (substituteType a _A) other)
UnifyRows (Row [p]) _P -> do
Lens.traverseOf_ biplate (occursCheck p) _P
solve [] (Lens.over biplate (substituteRow p _P) other)
UnifyRows _P (Row [p]) -> do
Lens.traverseOf_ biplate (occursCheck p) _P
solve [] (Lens.over biplate (substituteRow p _P) other)
UnifyFields (Absent [f]) _F -> do
Lens.traverseOf_ biplate (occursCheck f) _F
solve [] (Lens.over biplate (substituteField f _F) other)
UnifyFields _F (Absent [f]) -> do
Lens.traverseOf_ biplate (occursCheck f) _F
solve [] (Lens.over biplate (substituteField f _F) other)
UnifyRows (Row []) _P -> do
solve [] (Lens.over biplate (deleteRow _P) other)
UnifyRows _P (Row []) -> do
solve [] (Lens.over biplate (deleteRow _P) other)
UnifyFields (Absent []) (Absent fs) -> do
solve [] (Lens.over biplate (deleteFields fs) other)
UnifyFields (Absent fs) (Absent []) -> do
solve [] (Lens.over biplate (deleteFields fs) other)
UnifyTypes (RecordType xs0 _P) (RecordType xs1 _Q)
| Map.keysSet xs0 == Map.keysSet xs1 -> do
let newConstraints =
UnifyRows _P _Q
: Map.elems (Map.intersectionWith UnifyFields xs0 xs1)
++ constraints
solve stuck (Constrained newConstraints _T)
| Row [] <- _P
, Row [] <- _Q -> do
let ys = Map.difference xs0 xs1
let zs = Map.difference xs1 xs0
let newConstraints =
Map.elems (Map.intersectionWith UnifyFields xs0 xs1)
<> [ UnifyFields _G absent | _G <- Map.elems ys ]
<> [ UnifyFields absent _H | _H <- Map.elems zs ]
<> constraints
solve stuck (Constrained newConstraints _T)
| Row [] <- _P -> do
let ys = Map.difference xs0 xs1
let zs = Map.difference xs1 xs0
let _S = linkConstrainedType everything
let toEntry q = do
freshFields <- traverse (\_ -> freshField) ys
return (q, freshFields)
let Row qs = equivalences _Q _S
entries <- traverse toEntry qs
let table = Map.fromList entries
let sigma p = Map.findWithDefault Map.empty p table
let absents = fmap (\_ -> absent) zs
let prefix =
instantiateConstraints
sigma
[ UnifyTypes
(RecordType (xs0 <> absents) _P)
(RecordType xs1 _Q)
]
let Constrained suffix _T1 =
instantiateConstrained sigma other
solve [] (Constrained (prefix <> suffix) _T1)
| Row [] <- _Q -> do
let ys = Map.difference xs0 xs1
let zs = Map.difference xs1 xs0
let _S = linkConstrainedType everything
let toEntry p = do
freshFields <- traverse (\_ -> freshField) zs
return (p, freshFields)
let Row ps = equivalences _P _S
entries <- traverse toEntry ps
let table = Map.fromList entries
let sigma p = Map.findWithDefault Map.empty p table
let absents = fmap (\_ -> absent) ys
let prefix =
instantiateConstraints
sigma
[ UnifyTypes
(RecordType xs0 _P)
(RecordType (xs1 <> absents) _Q)
]
let Constrained suffix _T1 =
instantiateConstrained sigma other
solve [] (Constrained (prefix <> suffix) _T1)
| otherwise -> do
let ys = Map.difference xs0 xs1
let zs = Map.difference xs1 xs0
let _S = linkConstrainedType everything
let toEntry fs p = do
freshFields <- traverse (\_ -> freshField) fs
return (p, freshFields)
let Row ps = equivalences _P _S
let Row qs = equivalences _Q _S
entries0 <- traverse (toEntry ys) qs
entries1 <- traverse (toEntry zs) ps
let table = Map.fromList (entries0 ++ entries1)
let sigma p = Map.findWithDefault Map.empty p table
solve [] (instantiateConstrained sigma everything)
UnifyTypes left right -> do
throwError (TypeMismatch left right)
UnifyFields (Present _ _) (Absent []) -> do
throwError FieldMismatch
UnifyFields (Absent []) (Present _ _) -> do
throwError FieldMismatch
UnifyRows _ _ -> do
solve (constraint : stuck) next
UnifyFields _ _ -> do
solve (constraint : stuck) next
run :: Expression -> Either TypeError Constrained
run expression = do
(constrained, _, _) <- runExcept (runRWST inference [] 0)
return constrained
where
inference = do
(type_, constraints) <- listen (infer expression)
solve [] (Constrained constraints type_)To prove the left identity law:
… we only need to consider two cases:
… and for the second case we get:
To prove the right identity law:
… we also only need to consider two cases:
… and for the second case we get:
To prove the associativity law:
… we only need to consider four cases:
In each case both sides of the associativity law reduce to the same canonical form which is (respectively);
These I already know how to type-check because I already built this feature for Grace. If you want to learn more, check out my post on Type-safe eval in Grace, which touches upon computed imports. ↩
Nix calls records "attribute sets" and calls fields "attributes", but in this post I will use the terms "records" and "fields" consistently since the target audience of this post isn't just Nix users. ↩
We'll add a fourth case later on in this post, but these three cases still motivate why we prefer to unify rows sharing the same domain. ↩