Type Inference (Part 1)

A tutorial series on type inference begins, covering the Damas-Hindley-Milner type system, unification, bidirectional type-checking, Algorithm J, row polymorphism, newtype declarations, type annotations, mutually recursive declarations, and side-effects/value restriction. The series assumes familiarity with abstract syntax trees, type systems, and OCaml, with code available in a companion repository.

Type Inference Part 1 June 25, 2026 june-25-2026 Welcome to part 1 of my tutorial series on type inference This post will cover - The Damas-Hindley-Milner type system - Unification - Bidirectional type-checking - Algorithm J - Row polymorphism - Newtype declarations - Type annotations - Mutually recursive declarations - Side-effects / value restriction We assume you understand - Abstract Syntax trees - Vaguely understand what a type system is. - Have some familiarity with reading OCaml. All the code in this article can be found in the companion repository https://github.com/smasher164/hm tut https://github.com/smasher164/hm tut . Each file under the lib directory corresponds to the features added in each section of this article. Type inference is the process of taking some expression that represents part of a program and returning its type. If the expression is invalid, i.e. it does some invalid operation according to the rules of your language like adding a bool to a string , type inference will fail. If the expression lacks the sufficient information to return a type, i.e. it is missing a binding in its scope or type information for a binding, type inference will fail. In this way, type inference is a superset of type-checking. Another term that is used synonymously is type reconstruction. What type inference is useful for: - Reducing the number of type annotations you have to write. - Validating that a program is type-safe, i.e. the program is safe to compile and execute and won't encounter a TypeError. - Using types to generate code. For example, knowing the types of a struct's fields can help you determine the struct's layout. Aside The formal definition of type safety is that "well-typed programs do not get stuck". What this means is if you have an interpreter for a language, and you pass it a program that's been successfully type-checked, it will never reach an unexpected state where it doesn't know how to evaluate something. For example, a multiplication operator in a VM might expect there to be two operands on the stack. Having fewer than two operands would be unexpected. Different kinds of type systems have different requirements and limitations to type inference. For instance, subtyping might allow a List<Square to be passed into any function that expects a List<Rectangle . Overloading might require some automatic resolution scheme based on the number of parameters, types, etc... to find the correct overload for a function. A borrow checker might want to infer the lifetime of a function parameter based on the lifetime of another. In the case of this article, we'll be covering an ML-like type system. ML has the unique property of being able to infer the type of an expression in a program without any annotations. What's more is that the types it infers for an expression are as general as they can be. Aside This is known as the principal type property. If an expression's principal type is P and the expression can also be given the type T, you can always substitute some of the type variables in P to get T. For most expressions, ML will return types based on the constructors used. For example, an expression like true && false would be inferred as bool . A lambda like fun x - x when applied to true would be given the type bool - bool . However, for let bindings, ML will perform a process called let generalization . What happens here is that the type of the variable bound by the let declaration will be made as polymorphic as possible. So for example, in php let id = fun x - x in id true the variable named id will be given the type forall 'a. 'a - 'a . For folks more familiar with languages like Java, it'd be like if we declared id as T id<T T x { return x; } When id gets applied to true , its type gets instantiated such that bool the type of true can be substituted into it, resulting in a concrete instance of id whose type is bool - bool , where the resulting type of the expression id true ends up being bool . How do we actually do this process of generalization and instantiation ? How are we able to invoke this generic function without passing in a type argument? How does the type of a function get inferred based on the type of its argument? There are certain rules, known under Damas-Hindley-Milner typically shortened to HM for Hindley-Milner type inference, that we have to follow to make inferring types like this possible. The specific implementation of HM we will be covering in this series is called Algorithm J. Another approach to implementing HM is called Algorithm W, but we won't be covering its implementation here, as we'll expand on later. The key difference between Algorithm J and Algorithm W is that the former uses mutable references, while the latter takes a constraint generation/rewriting approach. We'll start by addressing the question of how we infer the type of a function based on the argument it's applied to. Already, this kind of inference is more powerful than the kind present in languages like Java or Go. Let's start with our signature for infer . js let rec infer env : env exp : exp : texp = ... infer takes the environment in the form of an env and an expression in the form of an exp , returning a typed expression in the form of texp . type env = id bind list This is where our variable bindings will go during the type-checking process. It will grow as we introduce new bindings. id is just a type alias for string. Represents identifiers like variables, type names, and type variables. type id = string We'll declare bind to be a sum type, since we'll introduce other kinds of bindings like type declarations later. type bind = | VarBind of ty A variable binding maps to a type. So for example, if the user wrote php fun x - foo x the body of the lambda needs to see x . In this case, the top of env would look like ...| "x": Bool | exp represents an expression in our program. This is basically our abstract syntax tree AST . For now, we'll just focus on function application, variables, and booleans. type exp = | EBool of bool true/false | EVar of id x | ELam of id exp fun x - x | EApp of exp exp f arg texp represents a typed expression, a.k.a an expression that holds a ty . There's a number of ways a type-checker could choose to define this. You can simply return a type and keep around a map from exp |= ty . You could parameterize the definition of exp so that it can be extended with more variants or fields. In our case, we're going to take a more straightforward approach of defining another typed AST that just duplicates all the variants of our untyped AST. type texp = | TEBool of bool ty | TEVar of id ty | TELam of id texp ty | TEApp of texp texp ty And the types held by ty can be A type type ty = | TyBool Bool | TyArrow of ty ty Function type: T1 - T2 | TyVar of tv ref Type variable: held behind a mutable reference. We will discuss tv 's role shortly. Unification unification Here's the expression we're trying to type-check: php fun x - x true As an AST, this looks like EApp ELam "x", EVar "x" , EBool true We'd like to infer types for this expression so that we get TEApp TELam "x", TEVar "x", ?0 , ?1 , TEBool true, ?2 , ?3 where each ? holds the type for that subexpression. How do we fill in those holes? To start off, let's try and fill in the information we already know. - The type of EBool true should be TyBool . - The return type of the lambda should be the same as its parameter's type, i.e. the type of x . - The parameter type of the lambda should be the same as the type of the lambda's argument, i.e. the type of EBool true . - The type of the application should be the same as the return type of the lambda. If we wrote these constraints out symbolically, it would look like ?2 = TyBool ?1 = TyArrow ?0, ?0 ?1 = TyArrow ?2, ?3 The types represented by a ? are called type variables . If we successfully solve for all of these type variables, we'll have type-checked our program. The above constraints are basically a system of equations involving types. If you've taken an algebra class, you might recall that one way of solving a system of equations is substitution. That is, you get a variable on its own to one side, and plug the other side in wherever that variable shows up in the other equations. So far, our set of solutions contains {?2 = TyBool} . We can start by plugging in TyBool wherever we see ?2 . We then get ?1 = TyArrow ?0, ?0 ?1 = TyArrow TyBool, ?3 Now we have two equations set to the same variable. Let's set them equal to each other. TyArrow ?0, ?0 = TyArrow TyBool, ?3 At this point, we recurse down and solve the corresponding types in the arrow. ?0 = TyBool ?0 = ?3 We can expand our solution set to {?2 = TyBool, ?0 = TyBool, ?1 = TyArrow TyBool, TyBool } Substituting TyBool for ?0 , we get TyBool = ?3 and our final solution set is {?2 = TyBool, ?0 = TyBool, ?1 = TyArrow TyBool, TyBool , ?3 = TyBool} . And that's it, we've inferred all the types for this expression. What does this look like in the failure case? Let's take the following example: php fun f - f true true As an AST it looks like EApp ELam "f", EApp EVar "f", EBool true , EBool true At a glance, we can tell this shouldn't type-check. If evaluated, it's going to try applying a bool like it's a lambda. Let's generate our type equations to see what happens when we try to solve them. Since we know that TEBool is going to have the type TyBool , we don't need an extra equation. TEApp TELam "f", TEApp TEVar "f", ?0 , TEBool true, TyBool , ?1 , ?2, , TEBool true, TyBool , ?3 Let's try to generate type equations for this example. Here's the information we know: - The parameter type of the lambda is the same as its argument type, a TyBool . - The parameter type of the lambda is the type of f . - The type of the application is the same as the return type of the lambda. - The parameter type of the lambda needs to be a TyArrow to be applied to true . - The return type of the lambda is the return type of f . Writing these constraints out more precisely: ?2 = TyArrow TyBool, ?3 ?2 = TyArrow ?0, ?1 ?0 = TyArrow TyBool, ?1 To solve this system of equations, we can start by setting the two definitions of ?2 equal to each other. TyArrow TyBool, ?3 = TyArrow ?0, ?1 ?0 = TyArrow TyBool, ?1 Now let's substitute TyArrow TyBool, ?1 for every occurrence of ?0 . TyArrow TyBool, ?3 = TyArrow TyArrow TyBool, ?1 , ?1 Now we start to recurse down both sides and... TyBool = TyArrow TyBool, ?1 And immediately, we reach a contradiction. TyBool is not an arrow type -- it is just TyBool . Since this equation would have to hold in order for this program to type-check, the program does not type-check. This process of solving equations on types is called unification . When we unify two types, we are trying to make them equal to each other by solving any type variables in them. If there's no solution to those type variables such that the two types can be made equal, then like with the previous example, the program will not type-check. The Algorithm W that was mentioned earlier is just doing unification by building up a solution set, which is substituted in for all the type variables. However, building up a solution set this way gets a bit unwieldy and slow-performing, since we have to rewrite our entire set of equations every time we want to perform a substitution. That may be fine for visualizing these small examples, but in a large program there can be many thousands of constraints. We can speed up this substitution process by observing that rewriting the equations is essentially broadcasting to the world the solution to some type variable. And "broadcasting updates to some data" is exactly the problem that mutable references were created to solve. We make each of those type variables a mutable reference, and any equation that mentions that variable automatically sees updates to that type variable. This is the essence of Algorithm J. When we solve that variable, we simply update the type at that reference. This is what the tv ref is meant to be. A type variable type tv = | Unbound of id Unbound type variable: Holds the type variable's unique name. | Link of ty Link type variable: Holds a reference to a type. An unsolved type variable is what we consider Unbound , as in unbound to any type. It has a unique identifier like "?0" , "?42" . A solved type variable is what we consider "bound". Here, we call it Link , as in "linked" to a type. Why "link" and not "bound"? Well you can imagine a type like ref TyVar Link ref TyVar Link TyBool , i.e. a chain of links that end up at some type. Linking is a convenient way to make a type equal to another one. We simply update its type variable to be a Link to the other type like so tv := Link other type Try unification try-unification Here's a small tool for visualizing the process of unification. Enter a few constraints of the form T1 = T2 one per line , then click Step to watch each one break down and link type variables to their solutions. Now let's consider what the implementation of infer actually looks like. Given some exp , we want to return a texp its typed version . Let's start by matching on the exp php let rec infer env : env exp : exp : texp = match exp with | EBool b - ... | EVar name - ... | ELam param, body - ... | EApp fn, arg - ... We'll take it case-by-case. The EBool case is trivially known, since its type is TyBool . php | EBool b - TEBool b, TyBool A true/false value is of type Bool. Aside The formation rule for booleans looks like This is basically an axiom that says Bool is a known type. The typing rule for booleans would look like This basically says given b which is one of true or false , b is of type Bool under the typing context Γ . For EVar , there is some mention of a variable -- the x being passed as an argument to foo in fun x - foo x , for example. We want to return the type of that variable. In order to do that, this variable must have already been declared somewhere before this occurrence, like as the parameter to a lambda. Because of that, we know it should be in the environment. We just have to search our environment from the innermost scope to outermost for this variable, and grab its type. Let's write that function js Lookup a variable's type in the environment. let lookup var type name e : env : ty = match List.Assoc.find e ~equal name with | Some VarBind t - t | - raise undefined error "variable" name We just call a function from the List.Assoc module and search an association list for a VarBind that matches name . After invoking this helper on our environment, we get a type associated with the variable name and return it up. So all in all, the EVar case looks like php | EVar name - Variable is being used. Look up its type in the environment, let var ty = lookup var type name env in TEVar name, var ty Aside The typing rule for variables would look like This basically says that if x has a binding to the type T inside the context environment Γ , then we can assume that under the context Γ , x has the type T . Bewildering, I know. The next case is ELam . Given some lambda like fun param - body , we want to return its type, which will be a TyArrow . First, we need the type for param . If you recall from the example, param 's type gets inferred based on the argument of the lambda. What we need to do is associate it with a fresh Unbound type variable call it ty param , so then when the argument's type is available, the type variable will get bound to it they will be unified . Let's take a look at how fresh unbound var looks. fresh unbound var creates a fresh type variable with a unique id. The unique id is based on an increasing counter variable called gensym counter that gets incremented every time we call this function. We just convert it to a string and make it the basis of the id. Global state that stores a counter for generating fresh unbound type variables. let gensym counter = ref 0 Generate a fresh unbound type variable. let fresh unbound var = let n = gensym counter in Int.incr gensym counter; let tvar = "?" ^ Int.to string n in TyVar ref Unbound tvar After creating a fresh type variable for the param , we add an entry to our env ironment for the param and this type variable. Then we can type-check the body of the lambda with that new environment. Finally, the resultant type will be the arrow type going from ty param with whatever the type of the lambda's body is. So ultimately, the ELam case looks like php | ELam param, body - Instantiate a fresh type variable for the lambda parameter, and extend the environment with the param and its type. let ty param = fresh unbound var in let env' = param, VarBind ty param :: env in Typecheck the body of the lambda with the extended environment. let body = infer env' body in Return a synthesized arrow type from the parameter to the body. TELam param, body, TyArrow ty param, typ body I'll briefly mention that typ just takes a texp and returns its ty field, since we'll sometimes need to grab the ty from the result of a recursive call to infer . js Get the type of a typed expression. let typ texp : texp : ty = match texp with | TEBool - TyBool | TEVar , ty - ty | TEApp , , ty - ty | TELam , , ty - ty Aside The formation rule for function types looks like This says that if A and B are types, then A - B is a type. The typing rule for lambdas looks like If under the context Γ , x the parameter 's type being A lets us infer that e the body 's type is B , then we can assume that the lambda's type is A - B . The final case is EApp . Given some function fn and an argument arg , we want to return the type of the result after applying fn to arg . We'll first want the types of fn and arg . We can simply call infer recursively on fn and arg , respectively. fn 's type should be some TyArrow ?A, ?B . arg 's type will be some ?C . We know from the discussion on constraints before, that TyArrow ?A, ?B = TyArrow ?C, ?D , where ?D is some unbound type variable. ?D is the type we want to return for this EApp . To accomplish this, we create a fresh unbound type variable to represent ?D , a.k.a the return type of the TyArrow . Then we synthesize a TyArrow ?C, ?D type and unify it with fn 's type. This is the first case where unification gets involved. The fresh type variables created by the ELam case can get resolved here. All in all, the final case of infer , EApp , looks like php | EApp fn, arg - To typecheck a function application, first infer the types of the function and the argument. let fn = infer env fn in let arg = infer env arg in Instantiate a fresh type variable for the result of the application, and synthesize an arrow type going from the argument to the result. let ty res = fresh unbound var in let ty arr = TyArrow typ arg, ty res in Unify it with the function's type. unify typ fn ty arr; Return the result type. TEApp fn, arg, ty res Aside The typing rules for lambda application look like If under the context Γ , f the lambda 's type is A - B and x the argument 's type is A , then f x f applied to x 's type is B . The crux of implementing this case is in how unify works, so let's discuss that now. js Unify two types. If they are not unifiable, raise an exception. let rec unify t1 : ty t2 : ty : unit = Follow all the links. If we see any type variables, they will only be Unbound. let t1, t2 = force t1, force t2 in match t1, t2 with | when equal t1 t2 - ... | TyArrow f1, d1 , TyArrow f2, d2 - ... | TyVar tv, ty | ty, TyVar tv - ... | - ... So to start off, we accept two types that we're going to try to equate. We force them and then match on both. force just dereferences all the Link s in a type variable. js let rec force ty : ty : ty = match ty with | TyVar { contents = Link ty } - force ty | ty - ty Now, we know that if we match on a type variable, that it's definitely Unbound , and won't have to do any dereferencing inside the body of unify . Let's take unify case-by-case. First, we just try checking if the two types are equal, according to OCaml's definition of equality. Note: we could've explicitly written out this case as TyBool, TyBool - , but structural equality handles this for us. php | when equal t1 t2 - The types are trivially equal e.g. TyBool . Next, we'll deal with the TyArrow case. If both types are TyArrow , a.k.a we're trying to equate TyArrow A, B = TyArrow C, D , we should try to unify A C and unify B D . This corresponds to our example earlier where we recursed down the corresponding types. php | TyArrow f1, d1 , TyArrow f2, d2 - If both types are function types, unify their corresponding types with each other. unify f1 f2; unify d1 d2; Finally, we get to the interesting case--when one of the types is a type variable. You might be wondering why this case is interesting. After all, if one of the types is a type variable, isn't all we have to do just to bind it to the other type, like tv := Link ty ? You're right that we have to bind it, but there's also the question of what will happen if we try to unify two types that can form cycles? Let's trace through the following example and see what happens: unify TyArrow ?0, ?0 TyArrow TyArrow TyBool, ?0 , ?0 unify ?0 TyArrow TyBool, ?0 ?0 := Link TyArrow TyBool, ?0 unify ?0 ?0 unify TyArrow TyBool, ?0 TyArrow TyBool, ?0 unify TyBool TyBool unify ?0 ?0 <-- uh-oh cycle We created a cycle in the first part of the unification by binding ?0 to TyArrow TyBool, ?0 . Then the second part of unification unify ?0 ?0 dereferences them and recursively processes the corresponding types in the arrow. When it does that, it eventually hits unify ?0 ?0 again, resulting in infinite recursion. This happens because the type pointed to by the type variable ?0 mentions ?0 , a.k.a a cycle. For this reason, before we bind a type variable to another type, we want to ensure that the type variable is not mentioned in that other type. One might ask, "aren't recursive types useful for things like trees and lists?" They are, but that is a different kind of recursive type than the one we are talking about. A recursive tree like type tree = | Leaf | Branch of int tree tree can always be compared by its name tree . However, with the recursive types we're talking about disallowing, the tree type is an infinite structure that needs to be compared while memoizing cycles. Aside One can think of cyclic types like these as recursive type aliases or anonymous recursive types. The formal name for these is equirecursive types , and they exist in some languages like OCaml with the -rectypes flag, and MLScript, which implements algebraic subtyping. A tree type would be expressed as μT. Leaf | Branch int, T, T . Notice how the recursion is extracted out as the parameter T . μ is basically a fixed-point combinator for types. When unifying a type variable with another type, we can normalize both types into this μ constructor, and then compare them. With nominal types and pattern matching, we explicitly fold and unfold types. This is what's called an iso-recursive type . This process of checking for a cycle before binding a type variable is called an occurs check, since we are checking that a type variable does not occur in the type we are binding to. Here is how an occurs check looks. We again match on the forced type, recursively call occurs if it's a TyArrow , and if we encounter a TyVar that's the same reference as the src , we have a cycle. Occurs check: check if a type variable occurs in a type. If it does, raise an exception. let rec occurs src : tv ref ty : ty : unit = Follow all the links. If we see a type variable, it will only be Unbound. match force ty with | TyVar tgt when phys equal src tgt - src type variable occurs in ty. raise OccursCheck | TyArrow from, dst - Check that src occurs in the arrow type. occurs src from; occurs src dst; | - With that, the TyVar case of unification can be written as php | TyVar tv, ty | ty, TyVar tv - If either type is a type variable, ensure that the type variable does not occur in the type. occurs tv ty; Link the type variable to the type. tv := Link ty Our last case for unification covers any pair of types that don't match the previous cases, and hence don't unify. php | - Unification has failed. raise unify failed t1 t2 where unify failed is just a helper that constructs an exception that prints out the types that failed to unify: js let unify failed t1 t2 = UnificationFailure Printf.sprintf "failed to unify type %s with %s" ty debug t1 ty debug t2 With that, unification is done and so is our implementation of type inference. Let's test it out with some examples. In our case, a program is just an expression. We'll define an alias for it, since we'll change this as we add extensions to the language. type prog = exp You can find and run these examples in lib/one.ml lib/one.ml . Examples examples php typecheck prog fun x - x true EApp ELam "x", EVar "x" , EBool true Output: bool php typecheck prog fun f - f true true EApp ELam "f", EApp EVar "f", EBool true , EBool true Output: UnificationFailure "failed to unify type bool - ?1 with bool" Simple extensions simple-extensions Let's extend our language with some simple extensions, namely if expressions for branching on a bool , let bindings with type annotations, mutually recursive let rec bindings, and nominal type declarations. If expressions if-expressions To start, if expressions require us to add a new variant to our exp type exp = ... | EIf of exp exp exp if <exp then <exp else <exp and texp types. type texp = ... | TEIf of texp texp texp ty as well as update our typ helper to extract the ty field php let typ texp : texp : ty = match texp with ... | TEIf , , , ty - ty In terms of type inference, we only need to add one case to infer to handle EIf , since we haven't added any new types. First, we must ensure that the condition is of type bool , by calling infer on the condition and unify ing the resultant type with TyBool . Then, we must ensure that the then branch and else branch have the same types, by calling infer on both branches, and unify ing their types together. The resultant type of the if can be either one of the types of those branches, since they're the same. php | EIf cond, thn, els - Check that the type of condition is Bool. let cond = infer env cond in unify typ cond TyBool; Check that the types of the branches are equal to each other. let thn = infer env thn in let els = infer env els in unify typ thn typ els ; Return the type of one of the branches. we'll pick the "then" branch TEIf cond, thn, els, typ thn Aside The typing rules for if expressions are This says if under the context Γ , cond the expression in the condition 's type is Bool , e1 the expression in the then branch 's type is T , and e2 the expression in the else branch 's type is T , then if cond then e1 else e2 's type is T . That was pretty quick Let's test it out. You can find and run these examples in lib/two.ml lib/two.ml . Examples examples-2 php if true then false else fun x - x true EIf EBool true, EBool false, EApp ELam "x", EVar "x" , EBool true Output: bool php if true then false else fun x - x EIf EBool true, EBool false, ELam "x", EVar "x" Output: UnificationFailure "failed to unify type bool with ?0 - ?0" Let bindings let-bindings A let binding is an expression like let x = true in f x or let x : bool = true in f x . Basically, it's a way of binding an identifier with an optional annotation to the result of evaluating some expression, and using that binding in the evaluation of another expression. Apart from the optional annotation, let x = exp in body is basically sugar for fun x - body exp . However, since we want to handle type annotations, and set ourselves up for generalization later on, we will handle this case independently. To start, we'll need to add an ELet variant to our exp type. We separate out the binding portion as let decl and body portion as exp for readability and easier destructuring. js type exp = ... | ELet of let decl exp let x : <type-annotation = <exp in <exp and let decl = id ty option exp We similarly update our texp . type texp = ... | TELet of tlet decl texp ty and tlet decl = id ty option texp Let's look at type inference for our ELet case. php | ELet id, ann, rhs , body - ... First, we want to infer the type of the right-hand-side of the binding. If there is a type annotation, we want to check that the inferred type unifies with the annotation. This pattern of comparing an inferred type with a declared type will come up again and again in our type-checker. We can extract it out into a helper called check . js let rec check env ty exp = let texp = infer env exp in try unify ty typ texp ; texp with UnificationFailure - raise type error ty This is actually the checking mode of bidirectional type-checking. infer is what's called inference mode or sometimes synthesis mode : given an expression, we produce its type. check is its dual: given an expression and an expected type, we verify the expression has that type. We use checking mode when the expected type is known from the context like an annotation , and inference mode when it isn't. Now we can match against the annotation and check that rhs satisfies it. php let rhs = match ann with | Some ann - check env ann rhs | None - infer env rhs in We then extend our environment with the binding and its type. js let env = id, VarBind typ rhs :: env in Finally, we infer the body of the binding the part after the in with the extended environment. This is the type we return up. js let body = infer env body in TELet id, ann, rhs , body, typ body Our ELet case ends up looking like php | ELet id, ann, rhs , body - let rhs = match ann with | Some ann - check env ann rhs | None - infer env rhs in let env = id, VarBind typ rhs :: env in let body = infer env body in TELet id, ann, rhs , body, typ body Aside Here are the typing rules for ELet . We split them into two rules, one for a let binding without an annotation and one for a let binding with an annotation. This says that under the context, if rhs can be inferred to be the type A , and the context extended with x having the type A lets us give body the type B , then the entire expression let x = rhs in body can be given the type B . This says that if A is a valid type, rhs can be inferred to be the type A , and the context extended with x annotated with the type A lets us give body the type B , then the entire annotated expression let x: A = rhs in body can be given the type B . Note that the only thing that's really changed here is that we need to make sure that A is a well-formed annotation. Other than that, the first rule is deriving A and in the second, A is an annotation supplied by the programmer. Now let's test it out You can find and run these examples in lib/three.ml lib/three.ml . Examples examples-3 js typecheck prog let x = true in if x then false else true ELet "x", None, EBool true , EIf EVar "x", EBool false, EBool true Output: bool php typecheck prog let x : bool = fun y - y in x ELet "x", Some TyBool, ELam "y", EVar "y" , EVar "x" Output: TypeError "expression does not have type bool" Mutually recursive definitions mutually-recursive-definitions If we wanted to write a recursive factorial function or mutually recursive is even / is odd functions, we need to add a let rec construct. To make type inference work in this situation, we need factorial and is even / is odd in the environments of the function bodies when type-checking them. We also want to make sure there aren't any duplicate definitions. To start, we'll add an ELetRec variant to our exp type. js type exp = ... | ELetRec of let decl list exp let rec <decls in <exp We similarly update our texp . type texp = ... | TELetRec of tlet decl list texp ty Let's take a look at type inference for ELetRec . php | ELetRec decls, body - ... First, we'd like to extend the environment with all of the declarations in the recursive let binding. We map over the declarations, creating a VarBind for each one, using an annotation if it exists--otherwise just a fresh type variable. php let env decls = List.map decls ~f: fun id, ann, - let ty decl = match ann with | Some ann - ann | None - fresh unbound var in id, VarBind ty decl in let env = env decls @ env in Next, we use the extended environment to check that the right-hand-side of each let binding matches its corresponding type in the environment. We zip over the VarBind list we created earlier as well as the let declarations themselves, checking that the right-hand-side's type matches the type in the VarBind . We return up a tlet decl corresponding to the typed let declaration, ultimately giving us a tlet decl list , which is what's needed in the TELetRec . js let decls = List.map2 exn env decls decls ~f: fun id, VarBind ty bind , ann, rhs - let trhs = check env ty bind rhs in id, ann, trhs in Finally, we infer the body of the let rec using the extended environment, returning up that type. js let body = infer env body in TELetRec decls, body, typ body Overall, our ELetRec case looks like php | ELetRec decls, body - let env decls = List.map decls ~f: fun id, ann, - let ty decl = match ann with | Some ann - ann | None - fresh unbound var in id, VarBind ty decl in let env = env decls @ env in let decls : tlet decl list = List.map2 exn env decls decls ~f: fun id, VarBind ty bind , ann, rhs - let trhs = check env ty bind rhs in id, ann, trhs in let body = infer env body in TELetRec decls, body, typ body Aside Here's the typing rule for ELetRec . decls is the set of names being bound in the let-rec. A x is the type for binding x and rhs x is its right-hand-side. Γ rec is the context Γ extended with all of the bindings, so each rhs x can refer to any of them. This rule basically says that if each rhs x has the type A x under Γ rec , and the body has the type B under Γ rec , then let rec { x = rhs x | x ∈ decls } in body has type B . For annotated bindings, assuming A x is well-formed, A x comes from its annotation with its quantified type variables made rigid in Γ rec . That's our let rec case Let's test it out with some examples. At this point, manually writing out the AST is going to get tedious, so I'll just show the source. If you're following along with the repo, you'll notice that we've integrated so that we can avoid writing the AST out by hand. You can find and run these examples in lib/four.ml lib/four.ml . Examples examples-4 php typecheck source {| let rec f = fun x - if x then g x else x and g = fun x - if x then f x else x in f true |} Output: bool php typecheck source {| let rec f = fun x - if x then g x else x and g : bool - bool - bool = fun x - if x then f x else x in f true |} Output: UnificationFailure "failed to unify type bool - bool with bool" Type declarations type-declarations An example type declaration in this language will be of the form php type Foo = { bar: bool baz: bool - bool } Note that the type name corresponds to a record. It can be constructed and projected selected from with php let foo : Foo = {bar = true, baz = fun x - x} in foo.baz A declaration is nominal . So another type with the same fields like php type Qux = { bar: bool baz: bool - bool } cannot be used in place of Foo . For example, this program won't type-check: php let qux : Qux = {bar = true, baz = fun x - x} in let foo : Foo = qux Type error: expected Foo, got Qux Nominal types or newtypes are called that because you only need to compare their names to know they are different, and this is how our unify will treat them as well. However, if you notice in the previous examples, we construct these records without mentioning the type name on the record literal, i.e. there is no Foo{...} form. So while we can compare types by their name to know that they are different, we will still have to infer that a record literal corresponds to some pre-declared type. The secret sauce we need to do that is called rows , which we'll describe shortly. Let's discuss the implementation of our nominal types. First, let's introduce type declarations type constructors to our language. type tycon = { name : id; ty : record ty; } and record ty = id ty list Our prog is now more than just an exp . Rather, it is now a list of type constructors and an exp . type prog = tycon list exp We also need a way of referring to a user-defined type by name. type ty = ... | TyName of id Type name: Foo Types get added to the environment just like variables. When we search for and find a type in the environment, we get back a TypeBind holding our tycon type bind = ... | TypeBind of tycon A type binding maps to a type constructor. At the expression-level, we need a way to construct these records by specifying all of its fields. type exp = ... | ERecord of record lit {x = true, y = false} We'll add a way to update fields using a with expression, producing a record of the same type with the provided fields set to different values type exp = ... | EWith of exp record lit { r with x = true, y = false} and a way to access fields also called projection type exp = ... | EProj of exp id r.y where record lit is a list of field name, expression pairs and record lit = id exp list Correspondingly, we update texp and define tyrecord lit type texp = ... | TERecord of tyrecord lit ty | TEWith of texp tyrecord lit ty | TEProj of texp id ty and tyrecord lit = id texp list We can go ahead and declare the lookup tycon helper that similar to lookup var type will search the env for a TypeBind with a name. js Lookup a type constructor in the environment. let lookup tycon name e : env : tycon = match List.Assoc.find e ~equal name with | Some TypeBind t - t | - raise undefined error "type" name Finally, in order to infer that a record literal constructs some predeclared type, we need that secret sauce I mentioned earlier. Remember how unification used type variables in place of types we hadn't figured out yet? We want to use those type variables for records as well, but we also want to say "we haven't figured out the type of this record yet, but we know it should have these fields". To do this, we are going to stash a constraint inside our Unbound type variable called a row constraint . Basically, a row is a set of label, type pairs, a.k.a a set of field names and their types they can also correspond to variant names and their types, but we will not be covering those in this post . If you recall, record ty is exactly the structure we want to represent such a set. Our constraints, then, are how we indicate that a type variable should have at least certain fields or exactly certain fields. and row constraint = | NoRow No row constraint. | OpenRow of record ty Must contain at least these fields from EProj/EWith . | ClosedRow of record ty Must contain exactly these fields from ERecord . and so we extend the definition of an Unbound type variable to be and tv = A type variable | Unbound of id row constraint ... NoRow is there to represent a regular type variable as we used it earlier, OpenRow is there to say that a type must have at least these fields, and ClosedRow says that a type must have exactly these fields. For example, A::{x: int, ...} says that the type A must be a record type that at least has a field named x whose type is int . Similarly, B::{x: int, y: int} says that the type B must be a record type that exactly has the fields x and y which are both of the type int . During type inference, we will encounter places where given two types that both contain row constraints, we will need to combine them. For this reason, we will define a union rows helper. js let rec union rows env row a: row constraint row b: row constraint : row constraint = match row a, row b with ... If NoRow is unioned with something else, that other row is the result. php | NoRow, row | row, NoRow - row If two OpenRow s are unioned together, we want to merge their fields, producing a new OpenRow . If they both share fields of the same name, unify their types together. php | OpenRow row a, OpenRow row b - OpenRow List.dedup and sort row a @ row b ~compare: fun f1,t1 f2,t2 - if String.equal f1 f2 then unify env t1 t2; 0 else Poly.compare f1,t1 f2,t2 If an OpenRow is unioned with a ClosedRow , we return the ClosedRow . However, we need to ensure that the fields in the OpenRow are a subset of the fields in the ClosedRow , since an OpenRow says we want at least those fields held by its constraint. For this case, we will define a fld exists helper that checks that a field name exists in a record ty and if so, that its type unifies with our expected type. php and fld exists env rcd: record ty id ty = List.exists rcd ~f: fun f,t - String.equal f id && unify env t ty; true Using this, our next case inside union rows is as follows: php | OpenRow o row, ClosedRow c row | ClosedRow c row, OpenRow o row - List.iter o row ~f: fun id,ty - if not fld exists env c row id ty then raise row mismatch row a row b ; ClosedRow c row Now if two ClosedRow s are unioned together, we need to ensure they have the same exact fields. We can first check that their length is the same and then check that each of the first row's fields is present in the second. | ClosedRow flds1, ClosedRow flds2 when Int.equal List.length flds1 List.length flds2 - List.iter flds1 ~f: fun id,ty - if not fld exists env flds2 id ty then raise row mismatch row a row b ; ClosedRow flds1 Finally, in any other case, we can say that the rows don't match. We raise a RowMismatch exception. php | - raise row mismatch row a row b Let's see how these constraints come up during type inference. We'll start off by extending infer to handle the record literal ERecord . Off the bat, even though we don't currently know the name of its type, we know exactly the fields it must have, so it must be a ClosedRow of some kind. Also, to know the type of a record, we need to know the type of each of its fields, so we should call infer on each field's type. php | ERecord rec lit - let rec lit = List.map rec lit ~f: fun id, x - id, infer env x in We get back a tyrecord lit . Since we want to return up its type, we want to map over and get the name and type of each field to get our record ty . php let flds = List.map ~f: fun id, x - id, typ x rec lit in Finally, to represent the type we'll return up, we create an Unbound type variable with a ClosedRow constraint holding flds . fresh unbound var ~row: ClosedRow flds Overall, our ERecord case of infer will look like this: php | ERecord rec lit - let rec lit = List.map rec lit ~f: fun id, x - id, infer env x in let flds = List.map ~f: fun id, x - id, typ x rec lit in TERecord rec lit, fresh unbound var ~row: ClosedRow flds The next expression we have to typecheck is EWith , which is of the form { r with x = true } . Basically, given some record and some fields that are being assigned, we need to ensure that the record has at least the fields that are being assigned. That is, the type we return for an EWith rcd, flds expression is an Unbound type variable with an OpenRow constraint holding the types of flds . We start by inferring the type of the record. php | EWith rcd, flds - let rcd = infer env rcd in And like before, we want to map over the flds and infer the type of each one of them, followed by mapping over the tyrecord lit to get a record ty . php let rec lit = List.map flds ~f: fun id, x - id, infer env x in let flds = List.map ~f: fun id, x - id, typ x rec lit in We can now generate an Unbound type variable for the return type holding the OpenRow constraint. js let row = fresh unbound var ~row: OpenRow flds in We want to ensure that the type of rcd is equivalent to row , since EWith guarantees that the input and the output type are the same. This is why we'll unify them. unify env typ rcd row; We can then return the TEWith up with the typed record, fields, and unified type. Overall, our EWith case should look like this: php | EWith rcd, flds - let rcd = infer env rcd in let rec lit = List.map flds ~f: fun id, x - id, infer env x in let flds = List.map ~f: fun id, x - id, typ x rec lit in let row = fresh unbound var ~row: OpenRow flds in unify env typ rcd row; TEWith rcd, rec lit, typ rcd The last expression we need to infer the type of is EProj , which involves accessing a field from a record. We follow a similar approach here. Given an EProj rcd, fld , we synthesize an Unbound type variable with an OpenRow constraint containing fld and its type, unifying the type variable with the type of rcd . php | EProj rcd, fld - let rcd = infer env rcd in let fld ty = fresh unbound var in let row = fresh unbound var ~row: OpenRow fld, fld ty in unify env typ rcd row; TEProj rcd, fld, fld ty Those are all the changes to infer . We need to now update unify to handle type names and row constraints. The bulk of the new logic happens when we try to unify TyVar with some other type. Since TyVar can now hold a row constraint , if the other type is record-shaped, we need to combine the constraints of both types. We start off by destructuring the type variable. and unify env t1 : ty t2 : ty : unit = ... | TyVar tv, ty | ty, TyVar tv - let Unbound , tv row = tv in We then want to match against ty and depending on what it is, union its rows with tv row . First, if ty is a TyName , we want to look up that type name in the environment, get its underlying record, and union its rows with tv row . php match ty with | TyName tname - let tc = lookup tycon tname env in ignore union rows env tv row ClosedRow tc.ty ... Next we handle the case where ty is a type variable that is distinct from tv . php | TyVar other when not phys equal tv other - let Unbound id, other row = other in We will union tv row with other row . Let's define a helper row iter that walks the fields in a row constraint . php let row iter row : row constraint f = match row with | NoRow - | OpenRow flds | ClosedRow flds - List.iter flds ~f First, we should make sure tv isn't mentioned inside the fields' types inside other row . php row iter other row fun , ty - occurs tv ty ; Then we can call our union rows helper and set other 's row to be the unioned row. js let row = union rows env tv row other row in other := Unbound id, row Next, if tv row is a NoRow , i.e. it's a regular type variable without a row constraint, we do a standard occurs check between tv and ty . php | when equal tv row NoRow - If either type is a type variable, ensure that the type variable does not occur in the type. occurs tv ty Otherwise, it must mean that tv row has some row constraint and ty is not record-shaped, which means unification has failed. php | - ty is not record-like. Can't unify with a row. raise unify failed t1 t2 ; If we haven't failed unification by now, we can Link ty to tv . Overall, the TyVar case of the match looks like php | TyVar tv, ty | ty, TyVar tv - let Unbound , tv row = tv in match ty with | TyName tname - let tc = lookup tycon tname env in ignore union rows env tv row ClosedRow tc.ty | TyVar other when not phys equal tv other - Union the rows of these two distinct type variables. let Unbound id, other row = other in row iter other row fun , ty - occurs tv ty ; let row = union rows env tv row other row in other := Unbound id, row | when equal tv row NoRow - If either type is a type variable, ensure that the type variable does not occur in the type. occurs tv ty | - ty is not record-like. Can't unify with a row. raise unify failed t1 t2 ; Link the type variable to the type. tv := Link ty Finally, unify needs to handle the trivial case where two TyName s have the same name. and unify env t1 : ty t2 : ty : unit = ... | TyName a, TyName b when equal a b - The type names are the same. With that, we've added type declarations and inference for record literals into our language. Aside Here is the formation rule for user-defined types This rule basically says if T is a user-defined type, in order for it to be well-formed, each of its field's types must be well-defined. Note: From this point on, Γ needs to be threaded throughout formation rules for well-formedness to hold, including WF-Bool and WF-Arrow. For example, WF-Arrow relies on A and B being well-formed for A - B to be well-formed. The typing rule for records: This says that if there is a type T in the context whose fields match that of the record, the record's type is T. The rule for with expressions: This says that if r is a record of type T that contains each of the fields in the with expression, then the returned value of the with expression is also of type T. and for projection: This says that if r is a record of type T containing a field f, then r.f has the type of that field in T. Let's take a look at some examples. You can find and run these examples in lib/five.ml lib/five.ml . Examples examples-5 php typecheck source {| type Foo = { x : bool, y : bool - bool } let foo : Foo = { x = true, y = fun x - x } in foo.y true |} Output: bool js typecheck source {| type Foo = { x : bool } let foo : Foo = { x = true } in { foo with y = true } |} Output: RowMismatch "{y: bool, ...} and {x: bool}" Polymorphism polymorphism Up until now, the language we have type-checked does not have any polymorphism. For example, in the following program, f cannot be applied both to a value of type A and to a value of type B . php type A = {} type B = {} let f = fun x - x in let a : A = {} in let b : B = {} in let = f a in f b Our type inference algorithm gives f the type A - A , so when it tries to type-check the application to B , it fails. We'd have to rewrite the example to have a separate fA and fB to get it to type-check. php let fA = fun x - x in let fB = fun x - x in let a : A = {} in let b : B = {} in let = fA a in fB b But when we look at f , nothing about its definition requires it to be restricted to A . How do we make f polymorphic or generic over its arguments? Instantiation instantiation We'd like f 's type to be something like forall 'a. 'a - 'a . But hang on, how would we even use a type like that? We can't exactly unify 'a with A . We need to treat 'a as a placeholder or type parameter that gets substituted with a concrete type argument. This process of taking a generic type and replacing its type parameters with concrete types is called instantiation . When f gets applied to an A or B , we look up its type which will now be generic , and instantiate it to have its type parameters substituted with fresh type variables. So for example, when f is applied to an A , forall 'a. 'a - 'a gets instantiated to get ?0 - ?0 . Then A - ?1 gets unified with ?0 - ?0 as normal, resulting in A - A as the type of the concrete instance of f . Likewise, when f is applied to a B , forall 'a. 'a - 'a gets instantiated to get ?2 - ?2 , and the same process will result in its concrete type becoming B - B . To get generic instantiation working, we first want to introduce generic ty that contains a type as well as a list of type parameters. A generic type. Should be read as forall p1..pn. ty, where p1..pn are the type parameters. It is separated from ty because in HM, a forall can only be at the top level of a type. type generic ty = { type params: id list; ty : ty; } You might be wondering why generic ty is not just another variant under ty , like Forall of id list ty . The short answer is that this kind of polymorphism is not possible in HM, because you no longer get complete type inference and lose principal types. In HM, the type parameters in a generic type are always at the outermost level. So you can have forall 'a 'b. 'a - 'b , but you cannot have forall 'a. 'a - forall 'b. 'b . Supporting the latter would be called higher-rank polymorphism not to be confused with rank polymorphism . For example, this function can't be written in HM. It accepts a polymorphic identity function as a parameter and instantiates it with two different types. php fun f g: forall a. a - a = g 1, g "hello" However, this is not very limiting in practice. Most of the polymorphic functions you'd ever want to write can be written in HM. Aside There are some useful exceptions though. For example, Haskell can use the ST monad to scope an action to a particular thread with the signature php runST :: forall a. forall s. ST s a - a Another example is with existentials, like Rust's dyn traits or Go's interface values. These can be encoded with higher-rank polymorphism. exists X. T which is roughly like dyn Trait can be written as forall Y. forall X. T - Y - Y . However, this latter feature can be added on its own, and doesn't necessarily need higher-rank polymorphism/polymorphic lambda calculus/System F. Next, we will update the definition of VarBind to hold a generic ty instead of a ty . This is needed because, if you consider the example above, f 's type in the environment needs to be generic so it can be instantiated. So now bind is defined as type bind = | VarBind of generic ty A variable binding maps to a generic type. | TypeBind of tycon A type binding maps to a type constructor. Our lookup var type function should be modified accordingly to return a generic ty . js Lookup a variable's type in the environment. let lookup var type name e : env : generic ty = match List.Assoc.find e ~equal name with | Some VarBind t - t | - raise undefined error "variable" name We also want to update the type annotations in let bindings to be generic, so if someone were inclined, they could write let f : forall 'a. 'a - 'a . and let decl = id generic ty option exp ... and tlet decl = id generic ty option texp Now let's discuss the changes to type inference. The first thing that's different is that when we look up a variable in our environment, we get a generic ty . In order to actually use it, we need to instantiate it to turn it into a regular ty , where the type parameters are substituted in for fresh type variables. So in our EVar case, after calling lookup var type , we want to inst antiate the var ty before returning it up. php | EVar name - Variable is being used. Look up its type in the environment, let var ty = lookup var type name env in instantiate its type by replacing all of its quantified type variables with fresh unbound type variables. TEVar name, inst var ty Now let's delve into how inst is implemented. Let's run through a simple example first, to get the point across. Given the generic type forall 'a 'b. 'a - 'b - 'a , if a had the fresh type variable ?0 and b had the fresh type variable ?1 , the instantiated type should be ?0 - ?1 - ?0 . More concretely, if the generic ty is { type params = "'a"; "'b" ; ty = TyArrow TyName "'a", TyArrow TyName "'b", TyName "'a" } the instantiated type is something like js let a = TyVar ref Unbound "?0", NoRow in let b = TyVar ref Unbound "?1", NoRow in TyArrow a, TyArrow b, a Note: I bound the TyVar s to variables here to show that the references would be the same. The actual implementation of inst just needs to create a hash table mapping from a type parameter to a fresh unbound type variable, traverse over the type, and replace each reference to that type parameter with that type variable. Instantiate a generic type by replacing all the type parameters with fresh unbound type variables. Ensure that the same ID gets mapped to the same unbound type variable by using an id, ty Hashtbl. let inst gty: generic ty : ty = let tbl = Hashtbl.create module String in List.iter gty.type params ~f: fun pid - Hashtbl.set tbl ~key:pid ~data: fresh unbound var ; let rec inst' ty = match force ty with | TyName id as ty - match Hashtbl.find tbl id with | Some tv - tv | None - ty | TyArrow from, dst - TyArrow inst' from, inst' dst | ty - ty in if Hashtbl.is empty tbl then gty.ty else inst' gty.ty The next place things are different is ELet and similarly ELetRec . Let's look at how ELet changes first. Because a let binding can have annotations and we now have generic types, those annotations can be polymorphic. Perhaps more interestingly, when a let binding is unannotated, it gets inferred to be as polymorphic as possible. This latter behavior is what we mentioned at the beginning of the tutorial as generalization . We'll cover the simple case of polymorphic bindings first, which is basically no inference, or rather, how to typecheck a let binding that has a polymorphic type annotation. What do we want from a polymorphic type annotation? Imagine we had the following program php let f : forall 'a. 'a - 'a = fun x - let y : 'a = x in y in f true Notice how the annotation on f introduces 'a with a forall . 'a is a type variable that can range over any type, so it can be instantiated with for example, int , bool , string , etc... On the right-hand-side of the let binding, we see a function whose body has another let binding, this time with an annotation mentioning the same 'a . Basically, if f gets instantiated with an int , the instantiation's type would be int - int , and the inner let binding's type would be int . We can say that the 'a introduced by forall 'a on f 's annotation is scoped to the right-hand-side of f 's binding. Another factor we should consider when we have type variables inside annotations is rigidity. What would happen if we tried to instantiate a generic annotation? Let's try to type-check the following program and see what happens: php let f : forall 'a 'b. 'a - 'b = fun x - x in f To be clear, we do not want this to type-check. We assigned an identity function the generic type forall 'a 'b. 'a - 'b , but that implies 'a and 'b must be distinct types, whereas in an identity function like fun x - x , the input type must match the output type. However, when we instantiate this type, we see TyArrow ?a, ?b which check tries to unify with the function's type TyArrow ?0, ?0 , so unify TyArrow ?0, ?0 TyArrow ?a, ?b unify ?0 ?a ?0 := Link ?a unify ?0 ?b force ?0 = ?a unify ?a ?b ?a := Link ?b We just unified ?a with ?b and type-checking passed, which is not what we want. So how do we fix this? Well imagine that instead of working with Unbound type variables for ?a and ?b , we were working with TyName "a" and TyName "b" . Two TyName s with different names are inherently unequal and do not unify. That's the key. We treat type variables as TyName s on their own. unify TyArrow ?0, ?0 TyArrow TyName "a", TyName "b" unify ?0 TyName "a" ?0 := Link TyName "a" unify ?0 TyName "b" force ?0 = TyName "a" unify TyName "a" TyName "b" unify TyName "a" TyName "b" fails, and so this program doesn't type-check. What TyName is doing here is serving as a rigid type variable. That is, unless the type variables have the same name, they do not unify. Instead of our typical instantiation, we will turn all the type variables in a generic ty into TyName s a.k.a rigid type variables , and extend our environment to hold those names. Extending our environment this way gives us scoping for these type variables, hence these are scoped and rigid type variables, a lot of jargon to say that the type variables in an annotation get put in our environment and get referenced as type names. To implement this, first, we will introduce another kind of binding to our environment called TypeVarBind . This just indicates that a name we look up is in fact a type variable. type bind = ... | TypeVarBind A type variable binding marks some rigid type. Then, we'll update our environment to hold TypeVarBind s for every type parameter in our generic type. This is where we make our annotation rigid. We don't need to modify the body of the type, because if we aren't calling inst , references to the type variable are just TyName s. Turn a generic ty into its rigid form, so that when annotations are instantiated, they don't produce Unbound type variables that can unify with each other. let as rigid gty: generic ty : env ty = let extras = List.map gty.type params ~f: fun id - id, TypeVarBind in extras, gty.ty For the unify trace from earlier to actually reject the invalid program, we need to update unify to handle TypeVarBind . We generalize lookup tycon into a lookup binding function that returns any binding, and the TyName arm becomes php | TyName tname - match lookup binding tname env with | TypeVarBind - match tv row with | NoRow - | - raise expected ty error "record" tname | TypeBind tc - ignore union rows env tv row ClosedRow tc.ty | VarBind - raise undefined error "type" tname Now let's look at how we modify ELet . php match ann with | Some ann - let extras, check ty = as rigid ann in check extras @ env check ty rhs | None - infer env rhs In the case where there is a generic annotation, we extend the environment with its type parameters extras , and type-check the right-hand-side. The annotation puts us back in checking mode, and the rigid type variables introduced by as rigid mean the check enforces the polymorphic annotation rather than falling back to inference. Now what if we want to have a generic function that doesn't need a type annotation? This is where generalization comes in. Generalization generalization Now that we've covered instantiation of generic types and checking generic annotations, it's time to get to the meat of Hindley-Milner--generalization. Simply put, generalization takes a type that's not generic and makes it generic by turning its unbound type variables into type parameters. So given a type like js let t = TyVar ref Unbound "?0" in TyArrow t, t generalization could turn it into something like { type params = "?0" ; ty = TyArrow TyName "?0", TyName "?0" } I say could turn into and not will turn into, because there is one crucial piece of information that plays a role in whether a type variable gets generalized--its scope. The rule is that a type variable on the right-hand-side of a let binding is only generalized if it was created in the right-hand-side of that let binding. So in other words, for an expression like js let x = RHS in BODY if the type variable's scope is within RHS, it can be generalized. Now before we talk about how to implement it, let's build up an intuition for why this is. When a type variable is generalized inside a let binding, it becomes distinct from type variables outside the let binding. This means if that type variable outside the let binding was meant to be resolved into a bool , that no longer applies to the generalized type variable. Let's work through the following example. php fun x - let y = x in y true true Already off the bat, we can tell that this program shouldn't type-check. We effectively have an identity function being applied to true , and the result is applied to true . And we know that Bool is not an arrow type, so it can't be applied to anything. We saw a similar contradiction in an earlier example. So what would happen in this example if we generalized every type variable on the right-hand-side of a let binding? If we trace the process of inference, it would look like this php 1. fun x - let y = x in y true true EApp 2. fun x - let y = x in y true EApp 3. fun x - let y = x in y ELam 4. ty param = ?0 5. env' = "x", forall . ?0 :: env 6. let y = x in y ELet 7. x EVar 8. inst forall . ?0 9. ?0 10. ty gen = gen ?0 11. env = "y", forall ?0. ?0 12. y EVar 13. inst forall ?0. ?0 14. ?1 15. ?0 - ?1 16. true EBool 17. ty res = ?2 18. ty arr = Bool - ?2 19. unify ?0 - ?1 Bool - ?2 20. ?2 21. true EBool 22. ty res = ?3 23. ty arr = Bool - ?3 24. unify ?2 Bool - ?3 25. ?3 On line 4, x is given the type variable ?0 . On line 6, it's bound to y . On line 10, y 's type is generalized. On line 13, it's instantiated to get the type variable ?1 . On line 15, we see the type of lambda ends up being ?0 - ?1 . On line 19, this type is unified with Bool - ?2 because of the inner application to true . On line 24, the result type ?2 is unified with Bool - ?3 because of the outer application to true . We end up with ?3 , an unbound type var, as the program's type. But this program should have produced a type error because Bool is applied to Bool The issue is the type of the lambda becoming ?0 - ?1 . After all, this is an identity function--the type of the lambda should be ?0 - ?0 . However, generalizing x 's type effectively separates it from ?0 , so while ?0 can continue to get unified with Bool , that information doesn't get propagated to ?1 . Because generalization happens at a let binding, we can't allow type variables that are mentioned outside of the let binding to be generalized. That outer type variable and the inner type variable once instantiated can end up unifying with different types and diverging, letting you make incorrect assumptions about that type. In the above example, if we knew that ?0 's scope escaped outside the let binding, we would not generalize it. The lambda's type would be ?0 - ?0 and we'd end up trying to unify Bool with an arrow type, leading to a type error. So if our rule is: only generalize type variables inside the scope of the right-hand-side of the let binding, how do we actually track the scope of a type variable? Since the scope corresponds to the right-hand-side of a let binding, the more nested a let binding is, the deeper its scope. This means we can treat the scope as a positive integer, where a deeper scope a.k.a a deeper let binding has a higher number. Turns out, we just need a single global integer corresponding to the current scope the type-checker is at--we'll call it current scope . When we enter a let binding, we increment its value via enter scope . When we exit the right-hand-side of the let binding, we decrement its value via leave scope . js The scope is an integer counter that holds the depth of the current let binding. Every unbound type variable contains the scope at which it was created. type scope = int Global state that stores the current scope. let current scope = ref 1 let enter scope = Int.incr current scope let leave scope = Int.decr current scope Okay we know the current scope, but now we need to associate each type variable with the scope it was created at. We need to modify our definition of tv type variable to store its scope, as well as modify our fresh unbound var function to construct a fresh type variable with the current scope. A type variable type tv = | Unbound of id row constraint scope Unbound type variable: Holds the type variable's unique name, any row constraint, and the scope at which it was created. | Link of ty Link type variable: Holds a reference to a type. Generate a fresh unbound type variable with a unique name, an optional row constraint, and the current scope. let fresh unbound var ? row=NoRow = let n = gensym counter in Int.incr gensym counter; let tvar = "?" ^ Int.to string n in TyVar ref Unbound tvar, row, current scope If the scope of a type variable is greater than the current scope , we know it is deeper contained inside , and it is safe to generalize. If we take another look at our previous example php fun x - let y = x in y true true with the updated generalization logic, we'll see php 1. fun x - let y = x in y true true EApp 2. fun x - let y = x in y true EApp 3. fun x - let y = x in y ELam 4. ty param = ?0, 1 scope is 1 5. env' = "x", forall . ?0 :: env 6. let y = x in y ELet scope is 2 7. x EVar 8. inst forall . ?0 9. ?0 10. ty gen = gen ?0 1 <= 2 11. env = "y", forall . ?0 12. y EVar 13. inst forall . ?0 14. ?0 15. ?0 - ?0 16. true EBool 17. ty res = ?1 18. ty arr = Bool - ?1 19. unify ?0 - ?0 Bool - ?1 20. Bool 21. true EBool 22. ty res = ?2 23. ty arr = Bool - ?2 24. unify Bool Bool - ?2 TYPE ERROR Note how the generalized type the type of y on line 11 does not have ?0 as a type parameter, since ?0 's scope 1 is not greater than current scope 2 . When the generalized type gets instantiated, it just returns ?0 , giving the lambda the type ?0 - ?0 . We see further down that this leads to unifying Bool with Bool - ?2 , which is a type error, as we expected. This leads us to ask another question. What happens when a type variable tv in an outer scope gets unified with a type ty containing type variables in an inner scope? Since we think of unification as equating two types, we should interpret this scenario as ty replacing all occurrences of tv . This means that all of the type variables inside of ty should have the scope of tv a.k.a the outer scope . In implementation terms, this is the minimum of the two scopes. So what we want is when unify ing a TyVar with another type, we traverse the other type for its type variables, and update their scope to be the minimum. If we take a look at our TyVar case in unify , we already do a traversal of the other type inside of occurs . We can take advantage of this and update the scope inside the occurs check. php | TyVar tv, ty | ty, TyVar tv - If either type is a type variable, ensure that the type variable does not occur in the type. Update the scopes while you're at it. occurs tv ty; Link the type variable to the type. tv := Link ty Then, after the occurs check when we Link to the target, the source type variable is automatically updated to point to the target. Let's look at how we'll modify the occurs check. We need to add an additional case. php | TyVar { contents = Unbound id, tgt row, tgt scope } as tgt - Recurse into the target's row constraint to lower scopes there too. row iter tgt row fun , ty - occurs src ty ; Grab src and tgt's scopes. let { contents = Unbound , , src scope } = src in Compute the minimum of their scopes the outermost scope . let min scope = min src scope tgt scope in Update the tgt's scope to be the minimum, preserving its row. tgt := Unbound id, tgt row, min scope Since Unbound carries row constraint as well as scope now, the destructure and update both have to include it. We also recurse into the row's types so their scopes get lowered too. Now the overall occurs check looks like Occurs check: check if a type variable src occurs in a type ty . If it does, raise an exception. Otherwise, update the scopes of the type variables in ty to be the minimum of its scope and the scope of src. let rec occurs src : tv ref ty : ty : unit = Follow all the links. If we see a type variable, it will only be Unbound. match force ty with | TyVar tgt when phys equal src tgt - src type variable occurs in ty. raise OccursCheck | TyVar { contents = Unbound id, tgt row, tgt scope } as tgt - row iter tgt row fun , ty - occurs src ty ; let { contents = Unbound , , src scope } = src in let min scope = min src scope tgt scope in tgt := Unbound id, tgt row, min scope | TyArrow from, dst - occurs src from; occurs src dst; | - To fully ensure that the scope of a type variable gets updated to be the outermost one, we also need to update the TyVar-TyVar arm in unify that unions row constraints. That arm doesn't go through the occurs check, so we set the min scope there directly: php | TyVar other when not phys equal tv other - let Unbound id, other row, other scope = other in row iter other row fun , ty - occurs tv ty ; let min scope = min src scope other scope in let row = union rows env tv row other row in other := Unbound id, row, min scope The change is just pulling out other scope , taking the minimum with src scope , and stamping it on the updated other . Now let's actually look into how generalization is implemented. gen will be a function that accepts a ty and returns a generic ty . js let gen ty: ty : generic ty = let type params = Hash set.create module String in We want to walk over the type to find all of its type variables, and grab the id s of the ones whose scope is greater than the current scope . We keep track of those ids in a Hash set called type params . Those will be the type parameters in our generalized type. We create a helper gen' to recur down the type and return the generalized type. The first case is the only interesting one the rest are just recurring over the ty . If the scope of the Unbound type variable is greater than current scope , we add the type variable's id to the type params hash set and return up a TyName with that id to reference that type parameter. Remember when inst antiation comes around, it will look for TyName s that correspond to those type parameters. We also mutate the tvar to Link to the generalized TyName , so any later code that walks the typed AST doesn't see it as still Unbound. js let rec gen' ty = match force ty with | TyVar { contents = Unbound id, , scope } as tv when scope current scope - Hash set.add type params id; tv := Link TyName id ; TyName id | TyArrow from, dst - TyArrow gen' from, gen' dst | ty - ty in We ignore the row constraint for now and come back to it when we handle row polymorphism. Finally, we call gen' on the input ty , get a sorted list of type parameters from the hash set, and return up our generic ty . js let ty = gen' ty in let type params = Hash set.to list type params | List.sort ~compare in { type params; ty } Overall, our gen implementation looks as follows: js let gen ty: ty : generic ty = let type params = Hash set.create module String in let rec gen' ty = match force ty with | TyVar { contents = Unbound id, , scope } as tv when scope current scope - Hash set.add type params id; tv := Link TyName id ; TyName id | TyArrow from, dst - TyArrow gen' from, gen' dst | ty - ty in let ty = gen' ty in let type params = Hash set.to list type params | List.sort ~compare in { type params; ty } Since we've finished writing the generalization procedure, let's update our type inference logic in infer . Most of our cases will actually not be affected. Just our ELam , ELet , and ELetRec cases. You might wonder why ELam is affected, since we only want to generalize at let bindings. This is correct. We don't want to generalize in ELam . However, the bindings in our environment have generic ty . In ELam , when we add the param to the environment with a fresh type variable, we need to wrap its type inside a generic ty , without actually generalizing it. Let's make a function dont generalize for this purpose. The environment stores generic types, but sometimes, we need to associate a non-generalized type to a variable. This function wraps a type into a generic type. let dont generalize ty : generic ty = { type params = ; ty } So now, our ELam case has to add the binding param, VarBind dont generalize ty param instead of param, VarBind ty param . All in all, it should look like php | ELam param, body - Instantiate a fresh type variable for the lambda parameter, and extend the environment with the param and its type. let ty param = fresh unbound var in let env' = param, VarBind dont generalize ty param :: env in Typecheck the body of the lambda with the extended environment. let body = infer env' body in Return a synthesized arrow type from the parameter to the body. TELam param, body, TyArrow ty param, typ body Next, our ELet case will be the first interesting one. As mentioned before, we want to enter scope at its beginning, and leave scope after inferring the right-hand-side of the binding. The beginning of the case should now look like php | ELet id, ann, rhs , body - enter scope ; let rhs = match ann with | Some ann - let extras, check ty = as rigid ann in check extras @ env check ty rhs | None - infer env rhs in leave scope ; ... On top of this change, we want to generalize the type of the right-hand-side when there's no annotation. If there is an annotation, we already have the polymorphic type we want, so we use the annotation directly. php let ty gen = match ann with | Some ann - ann | None - gen typ rhs in That's the type we add to the environment for the binding. js let env = id, VarBind ty gen :: env in And the rest is kept as usual. Overall, the ELet case should look like php | ELet id, ann, rhs , body - enter scope ; let rhs = match ann with | Some ann - let extras, check ty = as rigid ann in check extras @ env check ty rhs | None - infer env rhs in leave scope ; let ty gen = match ann with | Some ann - ann | None - gen typ rhs in let env = id, VarBind ty gen :: env in let body = infer env body in TELet id, ann, rhs , body, typ body Try let generalization try-let-generalization Here's a tool to visualize the process of let generalization. Pick the naive rule or the scope-checked one, then step through to see how the trace differs between them. The ELetRec case is slightly more complicated. To type-check recursive let bindings, we want to delay generalization until after each let binding is inferred. This means that mutually recursive bindings will not be referencing generic versions of each other. Why is this? Turns out that referencing generic versions of each other while fully inferring their types is undecidable. Here is an example of polymorphic recursion from the ocaml docs https://v2.ocaml.org/manual/polymorphism.html s%3Apolymorphic-recursion . js type 'a nested = | List of 'a list | Nested of 'a list nested let rec depth = function | List - 1 | Nested n - 1 + depth n Looks like a fairly simple function, but the issue here is that the inner call to depth n ends up trying to unify 'a nested with 'a list nested , which is not satisfiable. The type-checker doesn't realize that the 'a nested depth was initially called on is different from the 'a list nested that's the element type. This can be solved by providing an explicit annotation to depth , like forall 'a. 'a nested - int . However, there are other issues related to polymorphic recursion in that it can't be monomorphized, and leads to inefficient implementation. In practice, not having polymorphic recursion is not an issue. Most of the recursive functions you'll ever want to define can be written and inferred in this setting. Aside The undecidability of type inference for polymorphic recursion was shown by Fritz Henglein in the paper "Type Inference with Polymorphic Recursion". They show that semi-unification reduces to type inference for polymorphic recursion, which implies it's undecidable. We still want to enter scope at the beginning. After that, we run as rigid on each declaration's annotation if it has one , storing the result in a list called prepared so we can reuse it across the next few passes. php | ELetRec decls, body - enter scope ; let prepared = List.map decls ~f: fun id, ann, rhs - match ann with | Some ann - let extras, check ty = as rigid ann in id, Some ann, rhs, extras, check ty | None - id, None, rhs, , fresh unbound var in When we map over each prepared declaration to add its binding to the environment, since we aren't generalizing until later, we just want to add the non-generalized versions by wrapping each check ty in dont generalize . This time, the extended environment is set to a variable named env with decls instead of env , because we want to keep the old env around so we can add the generalized bindings. php let env decls = List.map prepared ~f: fun id, , , , check ty - id, VarBind dont generalize check ty in let env with decls = env decls @ env in When we check the right-hand-side of the declarations using the types in the extended environment env with decls , we add the rigid extras to it and check against check ty . After all of the right-hand-side expressions in the recursive let binding have been inferred, then we can leave scope . This list of declarations needs to be a tlet decl list , since that's what TELetRec expects. js let tdecls : tlet decl list = List.map prepared ~f: fun id, ann, rhs, extras, check ty - let trhs = check extras @ env with decls check ty rhs in id, ann, trhs in leave scope ; Now we generalize the types of all the bindings. As with ELet , if there's an annotation we use it directly, otherwise we call gen on the inferred type. php let generalized bindings = List.map tdecls ~f: fun id, ann, rhs - let ty gen = match ann with | Some ann - ann | None - gen typ rhs in id, VarBind ty gen in Finally, we add it to the original env so we can use it to infer the body of the recursive let binding. js let env body = generalized bindings @ env in let body = infer env body body in TELetRec tdecls, body, typ body Overall, our updated implementation of ELetRec looks like php | ELetRec decls, body - enter scope ; let prepared = List.map decls ~f: fun id, ann, rhs - match ann with | Some ann - let extras, check ty = as rigid ann in id, Some ann, rhs, extras, check ty | None - id, None, rhs, , fresh unbound var in let env decls = List.map prepared ~f: fun id, , , , check ty - id, VarBind dont generalize check ty in let env with decls = env decls @ env in let tdecls : tlet decl list = List.map prepared ~f: fun id, ann, rhs, extras, check ty - let trhs = check extras @ env with decls check ty rhs in id, ann, trhs in leave scope ; let generalized bindings = List.map tdecls ~f: fun id, ann, rhs - let ty gen = match ann with | Some ann - ann | None - gen typ rhs in id, VarBind ty gen in let env body = generalized bindings @ env in let body = infer env body body in TELetRec tdecls, body, typ body Aside Here's our typing rule for ELet . FV A and FV Γ are the sets of type variables that appear free in A and Γ respectively. We write vars for FV A \ FV Γ , the type variables free in A but not in Γ . This rule basically says that if rhs has the type A in Γ , and Γ extended with x having the type ∀ vars. A lets us give the body the type B , then let x = rhs in body has type B . And here's our typing rule for ELetRec . Here, we have the same decls , A x , rhs x , and Γ rec as in the original T-LetRec rule. vars x is the set of type variables we generalize for the binding x . This rule basically says that if each rhs x has the type A x in Γ rec , and Γ extended with each x having the type ∀ vars x. A x lets us give the body the type B , then let rec { x = rhs x | x ∈ decls } in body has type B . Note that when the rhs is inferred, x is not polymorphic i.e. it's a monotype , so in our formulation of T-LetRec, polymorphic recursion isn't supported. The original Damas-Milner formulation factors generalization out as its own rule: This says that if e has the type A in Γ , and a is any type variable not free in Γ , then e can be given the type ∀a. A . With T-Gen-DM in place, the simpler versions of T-Let and T-LetRec don't need to generalize themselves. They assume A is already polymorphic where needed, and just thread it through. Chaining applications of T-Gen-DM for each variable in FV A \ FV Γ gives us the same generalization present in our T-Let and T-LetRec rules. Woo That was a doozy. But we got through it now. How about we take a look at some examples to celebrate? You can find and run these examples in lib/six.ml lib/six.ml . Examples examples-6 php typecheck source {| type A = {} let a : A = {} in let f = fun x - x in let = f a in f true |} Output: bool php typecheck source {| let rec fix = fun f - fun x - f fix f x in fix fun f - fun arg - if arg then f false else true |} Output: bool - bool js typecheck source {| type A = {} let a : A = {} in let f : forall 'a. 'a - bool = fun x - true in f a |} Output: bool php typecheck source {| type A = {} let f : forall 'a. 'a - A = fun x - true in f true |} Output: TypeError "expression does not have type 'a - A" php typecheck source " fun x - let y = x in y true true" Output: UnificationFailure "failed to unify type bool with bool - ?2" Row polymorphism row-polymorphism Currently, we are able to infer the types of expressions involving records, as long as they ultimately unify to some concrete type. However, one of the beautiful things about let generalization in Hindley-Milner is that we can define a function without a type signature that can operate on values of different types. What if we could apply that polymorphism to records? For example, given the records php type Foo = { x : bool } type Bar = { x : bool - bool } let r1 : Foo = { x = true } in let r2 : Bar = { x = fun y - y } in and the function php let f = fun r - r.x in We'd like to be able to invoke f on both records, that is f r1 and f r2 . There's no reason why r.x can't operate on both records, since they both have fields named x . Similarly with { r with x = true } , the only requirement on r is that it contain a field x whose type is bool . How do we encode this in our type system? Recall when inferring the type of record projection, we give the record a fresh unbound type variable with an OpenRow constraint. We expressed to the type-checker "we don't know what record this is but we know it should contain a field named x ." So at the expression level, that constraint is already attached to the Unbound type variable for r . The problem is what happens at generalization. When f is normally generalized, the OpenRow constraint isn't preserved, so you end up with forall 'a 'b. 'a - 'b . We need some way of encoding that 'a is a record with a field x : 'b . Here's the syntax for that: php forall 'a 'b. 'a :: { x : 'b, ... } = 'a - 'b The piece between :: and = is a row constraint, and it corresponds directly to the OpenRow the expression-level inference produced for r . So row polymorphism is really about carrying that constraint through gen , inst , and unify . The expression-level inference doesn't have to change at all. Aside Our approach borrows ideas from Atsushi Ohori's A Polymorphic Record Calculus and Its Compilation https://dl.acm.org/doi/10.1145/218570.218572 , including the :: syntax for kind-based constraints on type variables. There are many other approaches to row polymorphism. Mitchell Wand's original row variables and Didier Rémy's presence/absence type system handle simple rows where labels must be unique. Daan Leijen's Extensible records with scoped labels https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/scopedlabels.pdf lifts that restriction with scoped rows. More recent work by Morris and McKinna in Abstracting Extensible Data Types: Or, Rows by Any Other Name https://dl.acm.org/doi/10.1145/3290325 introduces a system called Rose that abstracts over rows via qualified types and captures both simple and scoped rows. Its successor, Generic Programming with Extensible Data Types https://dl.acm.org/doi/10.1145/3607843 by Hubers and Morris, extends Rose with first-class labels and generic programming over rows, enabling polymorphic equality on extensible records and variants. Okay so given that type signature, it's clear we need to update generic ty and TypeVarBind to carry row constraints. Then we need to update gen , inst , and unify accordingly. type generic ty = { type params : id row constraint list; ty : ty; } Similarly, we want type variables sitting in our environment to hold onto those row constraints as well. type bind = ... | TypeVarBind of row constraint And correspondingly, we have to update the producers and consumers of generic ty . Let's start with the simplest: as rigid . js let as rigid gty: generic ty : env ty = let extras = List.map gty.type params ~f: fun id, row - id, TypeVarBind row in extras, gty.ty Next, let's update gen . We're going to create a small helper to map over the fields of a row constraint. php let map row ~f row = match row with | NoRow - NoRow | OpenRow flds - OpenRow List.map flds ~f: fun id, ty - id, f ty | ClosedRow flds - ClosedRow List.map flds ~f: fun id, ty - id, f ty Now gen just needs to map over the row constraint to generalize unbound type variables present in the row constraint. | TyVar { contents = Unbound id, row, scope } as tv when scope current scope - Hashtbl.set type params ~key:id ~data: map row ~f:gen' row ; We also change type params from a Hash set to a Hashtbl so we can map a type variable to its row constraint. Overall, our gen implementation looks like js let gen ty: ty : generic ty = let type params : id, row constraint Hashtbl.t = Hashtbl.create module String in let rec gen' ty = match force ty with | TyVar { contents = Unbound id, row, scope } as tv when scope current scope - Hashtbl.set type params ~key:id ~data: map row ~f:gen' row ; tv := Link TyName id ; TyName id | TyArrow from, dst - TyArrow gen' from, gen' dst | ty - ty in let ty = gen' ty in let type params = Hashtbl.to alist type params | List.sort ~compare: fun a, b, - String.compare a b in { type params; ty } Similarly, we update inst . It's mostly the same as before: create fresh type variables for each type parameter, then walk the type body replacing each TyName with its corresponding type variable. However, this time, we need to also preserve whatever row constraint the type parameter had, recursing over the row to instantiate its type variables as well. Overall, our inst implementation looks like js let inst gty: generic ty : ty = let tbl = Hashtbl.create module String in List.iter gty.type params ~f: fun pid, - Hashtbl.set tbl ~key:pid ~data: fresh unbound var ; let rec inst' ty = match force ty with | TyName id as ty - match Hashtbl.find tbl id with | Some tv - tv | None - ty | TyArrow from, dst - TyArrow inst' from, inst' dst | ty - ty in Attach the instantiated row constraint to each fresh type variable in the table. List.iter gty.type params ~f: fun pid, row - match row with | NoRow - | - match Hashtbl.find exn tbl pid with | TyVar tv - let Unbound id, , scope = tv in tv := Unbound id, map row ~f:inst' row, scope | - failwith "unreachable: tbl always holds TyVars" ; inst' gty.ty We now need to update unify to handle type variables that carry row constraints, like those in a type annotation that as rigid puts in env as rigid TyNames. We need to ensure that fields in a type variable's row constraint exist in the rigid type's row constraint. We'll pull this into a helper called check rigid subset . If the type variable has no row constraint, it's trivially a subset of anything else. and check rigid subset env tname tv row rigid row = match tv row, rigid row with | NoRow, - ... If the type variable has a row but the rigid type doesn't, then the rigid type isn't record-shaped, so we throw an error. php | , NoRow - raise expected ty error "record" tname ... If the type variable has an OpenRow, we check if each of its fields exists in the rigid type's row by calling fld exists , which if you recall tries to unify the field's type. php | OpenRow flds, OpenRow rigid flds | OpenRow flds, ClosedRow rigid flds - List.iter flds ~f: fun id, ty - if not fld exists env rigid flds id ty then raise row mismatch tv row rigid row ... The catch-all covers when the type variable has a ClosedRow, which means it's a record literal that hasn't found its nominal type yet. A rigid type variable isn't a nominal type so they can't be bound. php | - raise row mismatch tv row rigid row Overall, check rigid subset looks like Check that tv row's fields are contained within rigid row. and check rigid subset env tname tv row rigid row = match tv row, rigid row with | NoRow, - | , NoRow - raise expected ty error "record" tname | OpenRow flds, OpenRow rigid flds | OpenRow flds, ClosedRow rigid flds - List.iter flds ~f: fun id, ty - if not fld exists env rigid flds id ty then raise row mismatch tv row rigid row | - raise row mismatch tv row rigid row Now the TypeVarBind case just becomes a call to check rigid subset . php | TyVar tv, ty | ty, TyVar tv - let Unbound , tv row, = tv in match ty with | TyName tname - match lookup binding tname env with | TypeVarBind rigid row - check rigid subset env tname tv row rigid row ... ... Aside Here are the typing rules for projection and with-expressions on row-polymorphic type variables. They mirror T-Proj and T-With from the section on Type declarations type-declarations , but get their fields from TypeVarBind instead of TypeBind . We update the T-Let rule to hold row constraints in the quantified type, where the row constraint for type variable a is denoted by R a . T-LetRec is similarly updated to carry row constraints in polymorphic types, but for each binding. Now let's look at some examples. You can find and run these examples in lib/seven.ml lib/seven.ml . Examples examples-7 In this example, 'r is a rigid type variable in the environment with an OpenRow constraint { x : bool, ... } . The body's r.x creates an OpenRow constraint { x : ? } on r 's type variable. check rigid subset confirms r 's row is contained in 'r 's row. js typecheck source {| type Foo = { x : bool, y : bool } let get x : forall 'r. 'r :: { x : bool, ... } = 'r - bool = fun r - r.x in let foo : Foo = { x = true, y = false } in get x foo |} Output: bool In this example, gen gives f a row-polymorphic type, a function whose input can be any record with an x field. Each application instantiates f 's type to a fresh type variable with an OpenRow constraint, which is unified with the argument. php typecheck source {| type Foo = { x : bool } type Bar = { x : bool - bool } let r1 : Foo = { x = true } in let r2 : Bar = { x = fun y - y } in let f = fun r - r.x in let = f r1 in f r2 |} Output: bool - bool In this example, get x 's type is instantiated to a fresh type variable with the OpenRow constraint { x : bool, ... } . That type variable is unified with Foo , but when unify tries to union their fields together, it finds that Foo doesn't have an x field. js typecheck source {| type Foo = { y : bool } let get x : forall 'r. 'r :: { x : bool, ... } = 'r - bool = fun r - r.x in let foo : Foo = { y = true } in get x foo |} Output: RowMismatch "{x: bool, ...} and {y: bool}" That's row polymorphism We can write functions that are polymorphic over the record types they operate on. Note that we didn't have to touch infer at all. All of our changes happened with generic ty , gen , inst , unify , plus some new helpers. This makes sense given that nothing about our expression language has changed. We just want to make our functions more generic. Generic type declarations generic-type-declarations You'll notice in our examples above, the type declarations are not generic. However, in languages like Java or ML, you have access to types like List that are instantiated with some type argument. Similarly to row polymorphism, we won't need to change anything about our expression-level inference. All of the work happens at the level of gen , inst , unify , and occurs . The first thing we'll want to do is modify our definition of tycon to contain type parameters. type tycon = { name : id; type params : id list; ty : record ty; } This allows us to write definitions like type Box<T = { x: T } where Box is a type constructor with a single type parameter. We need some way to represent a concrete type like Box<bool , which is the result of type application . We will modify our ty definition to add a TyApp variant. type ty = ... | TyApp of ty list Type application: head :: args, e.g. TyApp TyName "box"; TyBool A Box<Bool would be represented as TyApp TyName "Box"; TyBool . Next, we need to update our gen , inst , and occurs implementations to handle TyApp . They all follow the same pattern of recursively mapping over the TyApp 's list. Here's gen : php let rec gen' ty = match force ty with ... | TyApp app - TyApp List.map app ~f:gen' ... Here's inst : php let rec inst' ty = match force ty with ... | TyApp app - TyApp List.map app ~f:inst' ... And here's occurs : js let rec occurs src : tv ref ty : ty : unit = match force ty with ... | TyApp app - List.iter app ~f: occurs src ... We now want to update unify to handle type applications. Conceptually, this is divided into two cases. The first is the case where you have two TyApp s and want to unify them. This is just a matter of checking that their type argument lists unify. That is, they are the same length and that each type argument of the first list unifies with the corresponding type argument of the second list. and unify env t1 : ty t2 : ty : unit = ... | TyApp app1, TyApp app2 when List.length app1 = List.length app2 - List.iter2 exn app1 app2 ~f: unify env ... The second case is where a type variable gets unified with a reference to some pre-declared type constructor that is possibly applied to some arguments. This case takes effect in unify where one of the two types is a TyVar . php match t1, t2 with ... | TyVar tv, ty | ty, TyVar tv - ... This case is split so we can handle when the other ty is either TyName just a type constructor's name or TyApp a type constructor applied to type arguments . For example, this would be the first case, where we'd unify Foo with ClosedRow { x: bool } . js type Foo = { x: bool } let foo : Foo = { x = true } in foo For Foo , there's nothing to apply. Its fields { x: bool } are already what we want to unify against. And this would be the second case, where we'd unify Box bool with ClosedRow { x: bool } . js type Box 'a = { x: 'a } let box : Box bool = { x = true } in box However, here we want to actually apply the type. That is, we want to substitute bool into the argument for Box to get a { x: bool } we can actually unify against. We define a helper apply tyapp to do this for us. js let apply tyapp env ty : ty : record ty = match force ty with ... If it's a TyName , there's nothing to apply. We just look the binding up in the environment, expecting a TypeBind holding a type constructor. Before we return its underlying record fields, we validate that the type constructor's argument list is empty, since we don't want someone to be referring to a type like Box in an annotation without fully applying it. php | TyName name - match lookup binding name env with | TypeBind tc when List.is empty tc.type params - tc.ty | TypeBind - raise cannot apply name | TypeVarBind | VarBind - raise undefined error "type" name If it's a TyApp , we still look up the binding, but now we have to substitute all the type arguments like bool in Box bool for the type parameters like 'a in Box 'a wherever they show up in the underlying record type so { x : bool } instead of { x : 'a } . If you recall back in the Instantiation instantiation section, we also perform substitution on types. Turns out, if we create a hash table mapping from the type parameters to their corresponding type arguments, we can use the same exact logic for substitution here. Let's first avoid some duplication by extracting out the substitution logic in a helper inst now calls substitute instead of inst' . js let rec substitute tbl : id, ty Hashtbl.t ty : ty : ty = match force ty with | TyName id as ty - match Hashtbl.find tbl id with | Some t - t | None - ty | TyArrow from, dst - TyArrow substitute tbl from, substitute tbl dst | TyApp app - TyApp List.map app ~f: substitute tbl | ty - ty And our type application logic just maps over the record fields of a type constructor, and substitutes each field's type using our table, returning the resultant record. php | TyApp TyName name :: args - match lookup binding name env with | TypeBind tc - match List.zip tc.type params args with | Ok pairs - let tbl = Hashtbl.of alist exn module String pairs in List.map tc.ty ~f: fun id, t - id, substitute tbl t | Unequal lengths - raise cannot apply name | TypeVarBind | VarBind - raise undefined error "type" name Finally, if we don't see a TyName or TyApp , we throw an error. php | - failwith "apply tyapp: expected TyName or TyApp" Overall, our apply tyapp function looks like js let apply tyapp env ty : ty : record ty = match force ty with | TyName name - match lookup binding name env with | TypeBind tc when List.is empty tc.type params - tc.ty | TypeBind - raise cannot apply name | TypeVarBind | VarBind - raise undefined error "type" name | TyApp TyName name :: args - match lookup binding name env with | TypeBind tc - match List.zip tc.type params args with | Ok pairs - let tbl = Hashtbl.of alist exn module String pairs in List.map tc.ty ~f: fun id, t - id, substitute tbl t | Unequal lengths - raise cannot apply name | TypeVarBind | VarBind - raise undefined error "type" name | - failwith "apply tyapp: expected TyName or TyApp" That might've seemed like a long detour but let's reorient ourselves. We're back to updating unify under the TyVar branch. We want to handle the cases where the other type is a TyName or TyApp corresponding to some type constructor. Here's how we handle these cases: php match t1, t2 with ... | TyVar tv, ty | ty, TyVar tv - let Unbound , tv row, src scope = tv in match ty with | TyName tname - match lookup binding tname env with ... | TypeBind - let tycon row = ClosedRow apply tyapp env ty in ignore union rows env tv row tycon row | TyApp - let tycon row = ClosedRow apply tyapp env ty in ignore union rows env tv row tycon row We apply the type to get its underlying record type and union its row constraints with those of our type variable that we're unifying. Aside We update our formation rules for type constructors by updating TypeBind to carry a list of type parameters. We add T-Record-App, T-Proj-App, and T-With-App to mirror T-Record, T-Proj, and T-With from the section on Type declarations type-declarations , but they substitute the type arguments into the tycon's body. We write T params ↦ args for T with each parameter in params replaced by the corresponding argument in args . And so ends our process of typechecking generic type declarations Let's look at some examples. You can find and run these examples in lib/eight.ml lib/eight.ml . Examples examples-8 Here's the box bool example from earlier. { x = true } is inferred as a ClosedRow { x : bool } that's checked against the annotation. apply tyapp takes box and substitutes bool for 'a in its body, giving us { x : bool } , which matches that closed row constraint. js typecheck source {| type box 'a = { x : 'a } let r : box bool = { x = true } in r.x |} Output: bool Here's an identity function of the type forall 'a. box 'a - box 'a . It gets instantiated to box ?0 - box ?0 , so when it's applied to r , box ?0 gets unified with box bool . This will hit the TyApp, TyApp case of our unify . js typecheck source {| type box 'a = { x : 'a } let identity : forall 'a. box 'a - box 'a = fun b - b in identity let r : box bool = { x = true } in r |} Output: box bool Here's a case where the literal's fields don't match the type constructor's. box requires x and y , but the literal only provides x . Going through the same route as before in apply tyapp , we find that { x : bool, y : bool } doesn't unify with ClosedRow { x : bool } , so we raise a RowMismatch . js typecheck source {| type box 'a = { x : 'a, y : bool } let r : box bool = { x = true } in r.x |} Output: RowMismatch "{x: bool} and {x: bool, y: bool}" Side effects side-effects Up until now, this language has been pure. You would think adding features like mutability and other side effects would not be a problem for a polymorphic type system like ours. However, there are gotchas. Let's say we added mutability to our language with a Ref 'a type. For example, Ref int corresponds to a memory location containing an int value. A Ref 'a can be built with a ref function, whose type is forall 'a. 'a - Ref 'a . You can retrieve the value at a Ref 'a via deref , whose type is forall 'a. Ref 'a - 'a . A shorthand operator for this is r , where r is the name of the reference. Finally, you can update the value at an existing memory location via update , whose type is forall 'a. Ref 'a - 'a - Unit Unit is just an empty record type . A shorthand syntax for this operation is r = v , where r is the name of the reference and v is the value being stored. So for example, js let r = ref 0 in r = r + 1; r this program would create a reference to a memory location containing an integer 0 , increment its contents to be one higher, and then return that value. So far so good. Now let's see what happens when we try to combine references with polymorphism. php type A = {} let r = ref fun x - true in r = fun x - if x then false else true; let a : A = {} in r a In this example, we create a reference to a lambda and then generalize it. r would have the generic type forall 'a. Ref 'a - bool . The third line instantiates the generic type to be Ref ?0 - bool and unifies ?0 - bool with the right-hand-side, whose type is bool - bool . All well and good. Now comes a problem. The last line again instantiates the generic type to get Ref ?1 - bool , dereferences it, and applies the lambda to a . The type-checker accepts this program. However, if we actually run this, the third line stores a lambda that accepts a bool ean condition and does if condition then ... to it. And the fifth line invokes that lambda on a value of type A . But A is not a bool What we learn from this example is that by generalizing a variable that is mutable, each instantiation gets to ignore changes to the type that other updates made to that memory location. We don't want that, because it means our program is not type-safe In other words, the evaluator of this language would reach an invalid state at runtime when it tries to do if a then ... , since A is not bool . What can we do about this? The immediate answer is to not generalize expressions like ref <exp , so we just end up with r 's type as Ref ?0 - bool . Then when the third line updates the location to hold bool - bool , that information gets carried into the last line, where we try to unify bool - bool with A - ?1 and fail. Well our intuition is mostly correct, but turns out we need to ensure that expressions we generalize don't contain ref <exp anywhere in their body. In our case, we can safely generalize any expression that is a constant EBool , variable EVar , lambda ELam , or a record literal ERecord whose elements are all generalizable. Everything else, like a function application, if expression, record projection, or let binding, we won't generalize. This is called the syntactic value restriction. It is the criterion Standard ML uses to handle mutability. We are basically ensuring that we only generalize values , but take a conservative approach and define value as any constant, variable, lambda, or record literal whose elements are all values. There are other approaches here, including OCaml's that does a deeper syntactic check to allow nested let bindings, record projection, some lambda applications, etc... Other approaches include changing our evaluation model from eager to lazy, analyzing the bodies of functions being applied to see if there are observable side effects, using an effect system to track effects of expressions, etc... That last one which Koka employs is kind of the ultimate solution to the problem, because we get precise tracking at the type-level for expressions that don't perform side effects and can be generalized. However, discussing effect systems is outside the scope of this article, and restricting generalization to syntactic values turns out to not be a problem in practice. Aside Stephen Dolan recently took a different approach in Rethinking the Value Restriction https://www.youtube.com/watch?v=C1g PO xcI8 that supports full rank-1 types in ML, restricts generalization to lambda abstractions, and lazily instantiates foralls only when forced to by application or projection. There is some nuance around covariance annotations and curried functions, but consider taking a look at this talk Let's take a look at how we can modify infer to implement the value restriction. We'll start with is value , a helper that determines if a typed expression is syntactically a value. js let rec is value x: texp : bool = match x with | TEBool | TEVar | TELam - true | TERecord rec lit, - List.for all rec lit ~f: fun , fld - is value fld | TEWith | TEApp | TEIf | TEProj | TELet | TELetRec - false The only interesting case is TERecord , where we check that all of its fields are also values. Next, let's write generalize if value , a helper that wraps gen so we only generalize when the rhs is a value. Otherwise, we fall back to dont generalize . js let generalize if value rhs : generic ty = if is value rhs then gen typ rhs else dont generalize typ rhs Now in our ELet case, the None branch where we previously called gen typ rhs becomes: php | None - generalize if value rhs The ELetRec case gets the same treatment in the List.map that produces generalized bindings . The None branch where we previously called gen typ rhs becomes: php | None - generalize if value rhs Putting this all together, we have implemented the value restriction. If we added ref , deref , and update built-ins, our language would correctly handle mutability. Aside Given the is value predicate we defined in this section, the typing rules for let and let-rec are updated to generalize only when the rhs is a value. Let's take a look at some examples. You can find and run these examples in lib/nine.ml lib/nine.ml . Examples examples-9 We can simulate the example from before with our type-checker. We add definitions and signatures for Ref , ref , deref , and update . We can't really implement update without an actual memory store, so we just return an empty Unit record. Because of the value restriction, r doesn't get generalized, and so update knows the type in the ref is just bool - bool . When we try to apply the dereferenced value to a Unit , it now fails to typecheck as expected. typecheck source {| type Ref 'a = { value : 'a } type Unit = {} let ref : forall 'a. 'a - Ref 'a = fun x - { value = x } in let deref : forall 'a. Ref 'a - 'a = fun r - r.value in let update : forall 'a. Ref 'a - 'a - Unit = fun r - fun x - {} in let r = ref fun x - x in let = update r fun x - if x then false else true in let u : Unit = {} in deref r u |} Output: UnificationFailure "failed to unify type bool with Unit" And here's how it looks being used successfully. typecheck source {| type Ref 'a = { value : 'a } type Unit = {} let ref : forall 'a. 'a - Ref 'a = fun x - { value = x } in let deref : forall 'a. Ref 'a - 'a = fun r - r.value in let update : forall 'a. Ref 'a - 'a - Unit = fun r - fun x - {} in let r = ref fun x - x in let = update r fun x - if x then false else true in update r fun x - false |} Output: Unit Conclusion conclusion The features covered in this article already give you a very sound and flexible system to program in, with generics, row polymorphism, side effects, and annotation-less type safety. As mentioned, see the companion repository https://github.com/smasher164/hm tut https://github.com/smasher164/hm tut for the source corresponding to each section. In the next post, we'll cover how to implement typeclasses/traits and their various extensions. Acknowledgements acknowledgements I'd like to thank Ashley Chekhova, Russell Johnston, and others for their helpful feedback.