Mechanized type inference for record concatenation

# Mechanized type inference for record concatenation Source: [https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation](https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation) 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](https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation#user-content-fn-computed) - computed record[2](https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation#user-content-fn-attribute)fields and field accesses - `//`\(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](https://www.sciencedirect.com/science/article/pii/089054019190050C)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](https://github.com/Gabriella439/record-concatenation)that you can use to test the reference Haskell implementation\. This post builds upon my previous post:[Record type inference for dummies](https://haskellforall.com/2026/06/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](https://pursuit.purescript.org/packages/purescript-record/4.0.0/docs/Record#v:merge)\) … 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 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\. ## 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 \(and\) and an implicit set of*potential fields*denoted by a "row variable" \(\)\. This row variable stands in for all other fields that*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: Bothandrange over two potentially infinite sets of fields \(two domains\), but they do not range over the**same**two domains\. Specifically,ranges over "all fields that are neithernor" andranges over "all fields that are not" soranges over one more potential field \(\) than\. That means we can't compareandas\-is because that wouldn't be an apples\-to\-apples comparison\. 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](https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation#user-content-fn-case4): - **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 solvingto 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 mentionsand only the right record type mentions\. However, we can fix themismatch by taking\(all fields that are not\) and "splitting out" an explicit field forand leaving behind a new row variablerepresenting all fields that are neithernor: Here we've introduced a new bit of syntax,, to denote thatis a*potential field*, meaning that we're still not sure whetheris present or not\. However, whether or notis presentno longer ranges over\. We can similarly replacewith an explicit mention ofand a new row variablerepresenting all fields that are neithernor: Now we can unifyandbecause they share same domain \(fields that are neithernor\) but how do we unifywith? ## Field annotations This is where we need to introduce some formal notation for potential fields \(henceforth, just "fields"\), which can be either\(with an associated field type\),, or unknown \(represented by a field variable, like\): So, for example: - means the record has a field namedstoring a - means the record has no field named - means that we don't know whether the fieldis present or not We also defineto be syntactic sugar forto support traditional record types, so if we were to unify these two types: … we would "desugar"to: … then desugarto: … 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 anfield: Then if we were to desugar the left record type: … we would get an irreconcilable mismatch because we can't unifywith, so unification fails\. ## 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: - andmust be records \(since we concatenate them using\) - must be a record field storing a\(since we addto it\) … but we don't know*which*recordcomes from becausecould be a field ofor a field ofor a field of*both*records \(in which case we'd source thefield fromsinceprefers the right record in case of overlap\)\. 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 anfield and they may also have some other fields, too\. Also, the function's output is a\. Additionally, the Wand algorithm would generate a constraint saying: …which you can read as saying that ourfield either comes from the left record \(ifis missing from the right record\) or from the right record \(regardless of whetheris present in the left record\)\. 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, and returnsif neither field is: You can think of this operator as analogous to theoperator, but merging field*types*instead of field*values*\. This operator simplifies constraints quite a bit\. For example, we can use this operator to simplify the inferred type ofto: … which is equivalent to the type the Wand algorithm infers\. > **Proof:**is true if and only ifis true, which you can demonstrate by computing a truth table for both constraints ranging over all nine permutations ofwhere\. 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 approachandare two different syntactic representations for the same field, and that's undesirable\. 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 abovemeans "zero or more repetitions", someans "zero or more field variables"\. In this representation,means that we know for sure that the field is present and*might*have typeunless a field variable inoverrides that type\. Vice versa,means that the field*might*be absent, unless a field variable inis\. We'll also add a little bit of syntactic sugar and writeas as shorthand foror more generally writeas a shorthand for\. 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 definein terms of this new representation: > 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\-mostfield \(if any\)\. If such afield exists then we discard everything to the left, and preserve all field variables to the right\. If no suchfield exists then we preserve all field variables\. This representation also gives us a simple algorithm for field equality:**two fields are equal if their canonical representations are equal**\. For example,andare both equal because they share the same canonical representation:\. 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 ``` Treatingas a function rather than syntax means that we can simplify any occurrence of, like in the constraint I proposed earlier: … because there we can desugarto: … which evaluates to: … and we can resugar that to the shorthand version:, which essentially deletes thefrom the constraint: … which we can read as saying "eitherorisand the right\-mostone stores a" ## 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](https://haskellforall.com/2026/06/record-type-inference-for-dummies)you can see that this is similar to before with a few differences: - the syntax for each field type changed fromto This 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 useas a shorthand for, though, so this syntax is a superset of our old syntax\. - 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 theoperator, but I included it for symmetry\. ## 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: ``` 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 Double ``` We'll also define a context \(\) as an ordered list of variables annotated with their types: ``` type Context = [(Identifier, Type)] ``` ## Natural deduction semantics 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](https://github.com/Gabriella439/record-concatenation)\) so you don't have to assemble the Haskell code fragments yourself\. ## Constraint generation 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 Type ``` We 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 NumberType ``` ## Constraint resolution To solve these generated constraints, we'll define a solver function, denoted by: … whererepresents some input constrained type andrepresents the final constrained type where as many constraints have been solved as possible and no reducible constraints remain\. 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 type ``` This 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) ``` ### Trivial constraints 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 … ``` ### Simple unification 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) ``` ### Substitution 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\.\) then we can satisfy the constraint using substitution\. This means we need to define a function to substitute a typeby replacing all occurrences of some type variablewith a replacement type\. … such that: Note that the above definition also requires also defining type substitution on fields \(e\.g\.\), so we can "overload" the same substitution function to work on fields: 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 = NumberType ``` If you're wondering what this is about: ``` substituteType a _A (RecordType fields _P) = RecordType (Lens.over biplate (substituteType a _A) fields) _P ``` Here's 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`Type`s 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 rowby replacing all occurrences of the row variablewith 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 earlieroperator to simplify the definition: In other words, we split a field into chunks delimited by, replace eachwithand then combine the result back together again using\. ``` 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,, and, but in this post I'll omit symmetric typing rules for the sake of space: ``` 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`Variable`s and automatically lift it to work on types, rows, and fields\. ### Deletion If a constraint unifies any row \(\) with an empty row \(\) then we can just delete all row variables mentioned within, becauseand setting a row variabletois the same thing as deleting that row variable\. So that means we'll define a function to delete row variables: ``` 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\.\) then we can also delete all of those field variables\. So we'll define a function to delete field variables: ``` 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) ``` ### Field instantiation \- Part 2 > 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](https://youtu.be/lKXe3HUG2l4?si=j1MrXyv9oAXc5s1R&t=645) 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 trivialconstraint and solve three more constraints by substitution: - substitutewith - substitutewith - substitutewith … 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 replacewith a fresh unknown field,, and a new row variable: … 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: - substitutewith - substitutewith 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\): ### Sibling row variables 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\. … which I'll call 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 fieldfor bothand\. However, we'd**also**need to instantiate the fieldforbecauseis a sibling ofandwithin theconstraint\. We would do so by performing three simultaneous substitutions: - substitutingwith - substitutingwith - substitutingwith … and that would replace therow constraint with two new constraints: … 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 reuseandinstead of introducingandand the result is still correct: ### Disjoint sets 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](https://en.wikipedia.org/wiki/Disjoint-set_data_structure)\. 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 all linked via sibling relationships\. Disjoint sets efficiently support the following operations we need for this algorithm: - there's an empty disjoint set \(with zero partitions\) - we can merge two disjoint sets by merging overlapping partitions - we can convert any set into a a disjoint set with a single partition - we can query which partitions overlap with a given set We'll use⟦⟧to denote the function that partitions row variables into a disjoint set\. In this disjoint set each partition will represent a set of row variables that are transitively linked via sibling relationships\. 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 sets - `singletons`converts any set into a disjoint set with a single partition - `equivalences`queries which partitions overlap with a given element ``` 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)) ``` ### Field instantiation \- Part 3 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 \(\) as a function from a row variable \(\) to a set of fields \(that we'll merge into a record type\): ``` type Instantiation = Variable -> Map Identifier Field ``` Then we'll define a lift instantiate to operate on a row \(denoted\) by instantiating each row variable and merging the results: ``` 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\), which updates record types by: - recursively instantiating each existing field - instantiating the row to generate new fields we add to the record ``` 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 = NumberType ``` Next we'll need a function that instantiates constraints \(denoted\)\. The trickiest case is instantiating a row constraint because we need to split out new field constraints: … 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 _B0 ``` Finally, 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 _T0 ``` Phew\! What a bear to spell out all of that\. ### Record unification 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 [] <- _P ``` The next rules all cover the case where there is a field mismatch, meaning the two records might share some fields in common \(\) but the left record might have extra fields \(\) and the right record might also have extra fields \(\)\. If there is a field mismatch and both records are closed then we: - unify the fields in common - unify any extra fields with ``` 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\.\) then the rule is: - partition all row variables within the constrained type - instantiate the open record's row**and its overlapping partitions**to add new variable fields \(e\.g\.\) to match the closed record - instantiate the closed record to add new absent fields \(e\.g\.\) to match the open record Here we'll useto denote the disjoint set returned by the first step andto denote all partitions that overlap with the row: ⟦⟧``` 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: - partition all row variables within the constrained type - instantiate both rows**and their overlapping partitions**to add new variable fields to match the other record ⟦⟧``` 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\. ### Errors There are two cases where constraint resolution produces an error: - type mismatch \(e\.g\. unifying awith aor unifying awith a record\) - field mismatch \(unifying afield with a strictlyfield\) ``` 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 FieldMismatch ``` ### Stuck constraints Some constraints \(like\) are "stuck", meaning that they cannot be reduced further unless one of the variables involved is solved or deleted\. These stuck constraints are either: - row constraints where both rows have more than one row variable: - field constraints of the form: 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\! ## Type inference 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](https://github.com/Gabriella439/record-concatenation)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 } -> Number ``` For 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 } -> Number ``` Also, 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 mismatch ``` Here 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 } ``` ## Appendix: Haskell implementation ``` {-# 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_) ``` ## Appendix: Monoid laws for To prove the left identity law: … we only need to consider two cases:\. For the first case we get: … and for the second case we get: To prove right identity law: … we also only need to consider two cases:\. For the first case we get: … and for the second case we get: To prove the associativity law: … we only need to consider four cases: - Case 0: - Case 1:and - Case 2:andand - Case 2:andand In each case both sides of the associativity law reduce to the same canonical form which is \(respectively\); - Case 0: - Case 1: - Case 2: - Case 3: 1. 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](https://haskellforall.com/2026/01/typesafe-eval), which touches upon computed imports\.[↩](https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation#user-content-fnref-computed) 2. 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\.[↩](https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation#user-content-fnref-attribute) 3. 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\.[↩](https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation#user-content-fnref-case4)