In earlier days Lisp didn't have a type system, as time pass, people start to want to (or need to) express program more precisely since cooperation and robustness. Then people start working for their needs. To express a list, introduce parametric polymorphism. parametric polymorphism sounds scared but doesn't, let's view an example:

(: list-length (All (A) (-> (Listof A) Integer)))

This syntax bind list-length to a type (All (A) (-> (Listof A) Integer)), or we would write list-length : (All (A) (-> (Listof A) Integer))you can see Racket use prefix operator, very Lisp style, not surprise XD. The syntax is not the most important thing, but it shows a very common thing in many different languages, to help you get what is parametric polymorphism. Now imagine, every time call list-length, must provide A as an argument: (list-length Number lst). People would get tired and say: I hate the static type system, it seems no surprise. That's the reason for type inference. With type inference, if lst : (Listof Number), A is Number, get type without type! The idea is so frustrating and makes people crazy to think about: Can we have a system, get all the type without type? The result is the HM type system.

(define id
  (lambda (x) x))

(: id-str (-> str str))
(define id-str (lambda (x) x))
(: id-int (-> int int))
(define id-int (lambda (x) x))
(: id-bool (-> bool bool))
(define id-bool (lambda (x) x))
(: id-int-to-int (-> (-> int int) (-> int int)))
(define id-int-to-int (lambda (x) x))

(: id (All (A) (-> A A)))
(define id
  (lambda (x) x))

This section helps you get a project would be modified in the following part:

raco pkg new hindley-milner
cd hindley-milner
raco pkg install --auto

I would show a small enough language can cooperate with HM type system and big enough to convince you this is useful. Here is the whole shape of the data up front, then the rest of the article explains why each piece has to be there.

Definition of language (create lang.rkt):

#lang typed/racket

(provide expr expr:int expr:bool expr:string expr:list expr:variable expr:lambda expr:application expr:let)

(struct expr [] #:transparent)
(struct expr:int expr [(v : Integer)] #:transparent)
(struct expr:bool expr [(v : Boolean)] #:transparent)
(struct expr:string expr [(v : String)] #:transparent)
(struct expr:list expr [(elems : (Listof expr))] #:transparent)
(struct expr:variable expr [(name : String)] #:transparent)
(struct expr:lambda expr
  [(param : (Listof String))
   (body : expr)]
  #:transparent)
(struct expr:application expr
  [(func : expr)
   (args : (Listof expr))]
  #:transparent)
(struct expr:let expr
  [(bindings : (Listof (Pair String expr)))
   (expr : expr)]
  #:transparent)

Definition of types (create typ.rkt):

#lang typed/racket

(provide typ typ:builtin typ:freevar typ:constructor typ:arrow typ:scheme
         set-typ:freevar-subst!)

(struct typ [] #:transparent)
;;; A freevar is a mutable ref cell. `subst` is what it has been solved to,
;;; `#f` means it is still open.
(struct typ:freevar typ
  [(index : Integer)
   (subst : (Option typ))]
  #:transparent
  #:mutable)
(struct typ:constructor typ
  [(name : String)
   (arg : (Listof typ))]
  #:transparent)
(struct typ:arrow typ
  [(from : typ)
   (to : typ)]
  #:transparent)
;;; A type scheme: forall vars . body
(struct typ:scheme typ
  [(vars : (Listof typ))
   (body : typ)]
  #:transparent)

(: typ:builtin (-> String typ:constructor))
(define (typ:builtin name)
  (typ:constructor name '()))

Four shapes of type. typ:constructor covers int, bool, string and list A alike, so typ:builtin is just the zero-argument case of it. typ:arrow is the function type. typ:freevar is the placeholder we hand out when a type is not known yet, and typ:scheme is what makes a binding polymorphic. The last two are the whole story of this article, and they are two different mechanisms, not one.

One helper before anything else, because the error messages need it (create pretty-print.rkt):

#lang typed/racket

(require "typ.rkt")

(provide pretty-print-typ)

(: pretty-print-typ (-> typ String))
(define (pretty-print-typ t)
  (match t
    ([typ:freevar idx subst]
     (if subst
         (pretty-print-typ subst)
         (format "?~a" idx)))
    ([typ:constructor name typ-args]
     (if (empty? typ-args)
         (format "~a" name)
         (let ([j (string-join (map
                                (lambda ([typ-arg : typ])
                                  (pretty-print-typ typ-arg))
                                typ-args) " ")])
           (if (string=? name "pair")
               (format "(~a)" j)
               (format "(~a ~a)" name j)))))
    ([typ:scheme vars body]
     (format "(forall (~a) ~a)"
             (string-join (map (lambda ([v : typ]) (pretty-print-typ v)) vars) " ")
             (pretty-print-typ body)))
    ([typ:arrow from to]
     (format "~a -> ~a" (pretty-print-typ from)
             (pretty-print-typ to)))))

Notice the typ:freevar case already follows subst when the cell has been solved.

Two pieces of state, and everything from here to the end of the inference goes into this one file, in the order it appears. Environment maps variable names to types and forms a chain of scopes, and Context carries the environment plus the counter that hands out fresh freevars (create semantic.rkt):

#lang typed/racket

(provide type/infer Context Context/new)

(require "lang.rkt"
         "typ.rkt"
         "pretty-print.rkt")

(struct Env
  [(parent : (Option Env))
   (type-env : (Mutable-HashTable String typ))]
  #:transparent
  #:mutable)
(: Env/new (->* () ((Option Env)) Env))
(define (Env/new [parent #f])
  (Env parent (make-hash '())))
;;; Env/lookup take variable name such as `x` to get a type from env
(: Env/lookup (-> Env String typ))
(define (Env/lookup env var-name)
  (: lookup-parent (-> typ))
  (define lookup-parent (lambda ()
                          (: parent (Option Env))
                          (define parent (Env-parent env))
                          (if parent
                              ; dispatch to parent if we have one
                              (Env/lookup parent var-name)
                              ; really fail if we have no parent environment
                              (raise (format "no variable named: `~a`" var-name)))))
  (let ([typ-env : (Mutable-HashTable String typ) (Env-type-env env)])
    (hash-ref typ-env var-name lookup-parent)))

(: Env/bind-var (-> Env String typ Void))
(define (Env/bind-var env var-name typ)
  (let ([env (Env-type-env env)])
    (if (hash-has-key? env var-name)
        (raise (format "redefined: `~a`" var-name))
        (hash-set! env var-name typ))))

(struct Context
  [(freevar-counter : Integer)
   (type-env : Env)]
  #:transparent
  #:mutable)
(: Context/new (-> Context))
(define (Context/new)
  (Context 0 (Env/new)))
(: Context/new-freevar! (-> Context typ))
(define (Context/new-freevar! ctx)
  (let ([cur-count (Context-freevar-counter ctx)])
    (set-Context-freevar-counter! ctx (+ 1 (Context-freevar-counter ctx)))
    (typ:freevar cur-count #f)))

Inference needs exactly two tools. This one answers these two types must be the same, what does that force?; the next one answers this binding can be used at many types, how?. We build both before walking the language, then the walk is short.

Solving a freevar is writing into its cell:

(: subst! (-> typ typ Void))
(define (subst! v t)
  (match v
    ([typ:freevar _ _] (set-typ:freevar-subst! v t))
    (_ (void))))

And because the cell remembers, nothing may look at a freevar directly. Every comparison has to force it first, following the chain until it reaches something that is not a solved freevar:

(: force (-> typ typ))
(define (force t)
  (match t
    ([typ:freevar _ s] (if s (force s) t))
    (_ t)))

So occurs, unify and free-vars below all force on the way in.

Occurs check makes unification fail when we are about to solve V to a type T that contains V itself. Without it we would accept

(= ?0 (list ?0))

and ?0 would stand for (list (list (list ...))), an infinite type. So we check whether v occurs in t, forcing on the way in:

(: occurs (-> typ typ Boolean))
(define (occurs v* t*)
  (define v (force v*))
  (define t (force t*))
  (match (cons v t)
    ; same freevar means `v` occurs in `t`, then should be rejected
    ([cons v (typ:freevar _ _)] (eqv? v t))
    ; arrow and constructor both just keep check on type parameters
    ([cons v (typ:arrow t1 t2)] (or (occurs v t1) (occurs v t2)))
    ([cons v (typ:constructor _ type-params)]
     (foldl (lambda ([t : typ] [pre-bool : Boolean])
              (or pre-bool (occurs v t)))
            #f
            type-params))
    ; rest is fine
    (_ #f)))

occurs only reports; unify below is what raises on a positive result, and that is how (lambda (x) (x x)) gets rejected.

Now unify itself:

(: unify (-> typ typ Void))
(define (unify t1* t2*)
  (define t1 (force t1*))
  (define t2 (force t2*))
  (match (cons t1 t2)
    ([cons (typ:constructor a al) (typ:constructor b bl)]
     #:when (string=? a b)
     (for-each (lambda ((ae : typ) (be : typ))
                 (unify ae be))
               al bl))
    ([cons (typ:arrow p1 r1) (typ:arrow p2 r2)]
     (unify p1 p2)
     (unify r1 r2))
    ;;; freevar type is the only interesting case in `unify`
    ((and
      [cons _ (typ:freevar _ _)]
      [cons t v])
     (cond
       ;;; already the same cell: nothing to solve, and writing here would make
       ;;; the cell point at itself, which `force` would then loop on
       ([eqv? v t] (void))
       ([occurs v t]
        (raise (format "occurs check failed: ~a in ~a"
                       (pretty-print-typ v) (pretty-print-typ t))))
       (else (subst! v t)))
     (void))
    ([cons (typ:freevar _ _) t2] (unify t2 t1))
    (_ (raise (format "cannot unify type ~a and ~a"
                      (pretty-print-typ t1) (pretty-print-typ t2))))))

Two constructors unify when the names match and their arguments unify pairwise. Two arrows unify componentwise --- in fact we could drop typ:arrow and encode it as a constructor named "->", all type constructors unify the same way. When one side is a freevar we solve it, after the occurs check. When only the left side is a freevar we flip and reuse the same case. Anything else is a type error.

Binding a variable to its inferred type does not make it polymorphic. (lambda (a) a) infers to (?0) -> ?0, and ?0 is one cell. If id is bound to that type and looked up twice, both uses get the same cell, so the first use decides it forever.

Polymorphism needs the sharing to be broken. Two operations do it.

First, the freevars a type still has open. Force on the way in, so a cell already solved to int contributes nothing:

(: free-vars (-> typ (Listof typ)))
(define (free-vars t)
  (match (force t)
    ([typ:freevar _ _] (list (force t)))
    ([typ:arrow f to] (append (free-vars f) (free-vars to)))
    ([typ:constructor _ args]
     (append* (map (lambda ([a : typ]) (free-vars a)) args)))
    ;;; the ones bound by forall are not free
    ([typ:scheme vars body]
     (filter (lambda ([v : typ]) (not (memq v vars))) (free-vars body)))
    (_ '())))

(: env-free-vars (-> Env (Listof typ)))
(define (env-free-vars env)
  (append
   (append* (map (lambda ([t : typ]) (free-vars t))
                 (hash-values (Env-type-env env))))
   (let ([p (Env-parent env)])
     (if p (env-free-vars p) '()))))

memq and assq throughout: a freevar is a ref cell, so identity is the right comparison.

At the binding site, quantify the freevars of the type that do not also occur in the environment:

(: generalize (-> Env typ typ))
(define (generalize env t)
  (let* ([in-env (env-free-vars env)]
         [quantified (remove-duplicates
                      (filter (lambda ([v : typ]) (not (memq v in-env)))
                              (free-vars t)))])
    (if (empty? quantified)
        t
        (typ:scheme quantified t))))

Why exclude the environment's freevars? Consider

(lambda (x) (let ([y x]) ...))

x : ?0, and y gets ?0 as well. But ?0 is still reachable from the environment through x, and whoever calls this lambda will decide what it is. Quantifying it would make y usable at any type out of nothing, and

(lambda (x) (let ([y x]) '((y 1) (y "s"))))

would typecheck. It must not. So the rule is: quantify what belongs to this definition alone.

Note this also means generalize often quantifies nothing. If the body of a definition already pinned a variable down, there is no freevar left to quantify and the binding stays monomorphic, which is exactly right.

At every use site, replace each quantified variable with a brand new freevar and copy the type:

(: instantiate (-> Context typ typ))
(define (instantiate ctx t)
  (match t
    ([typ:scheme vars body]
     (let ([mapping : (Listof (Pairof typ typ))
                    (map (lambda ([v : typ]) (cons v (Context/new-freevar! ctx))) vars)])
       (copy/subst mapping body)))
    (_ t)))

(: copy/subst (-> (Listof (Pairof typ typ)) typ typ))
(define (copy/subst mapping t)
  (let ([t (force t)])
    (match t
      ([typ:freevar _ _]
       (let ([hit (assq t mapping)])
         (if hit (cdr hit) t)))
      ([typ:arrow f to]
       (typ:arrow (copy/subst mapping f) (copy/subst mapping to)))
      ([typ:constructor name args]
       (typ:constructor name (map (lambda ([a : typ]) (copy/subst mapping a)) args)))
      (_ t))))

The copy is the point. The scheme stays untouched in the environment so the next use can copy it again, and the two uses end up with two unrelated cells.

With both tools in hand the inference itself is a walk over the syntax, one clause at a time. It also shows how to get the ideas behind the rules, not just remember a snapshot.

Monomorphism, which means obviously and decidable, and it would be a good start:

([expr:int _] (typ:builtin "int"))
([expr:bool _] (typ:builtin "bool"))
([expr:string _] (typ:builtin "string"))

You can see why I say they are obviously even you never use static type, because this type is builtin in most language, inference their types is just by definition. 1 is int, #t is bool, "hello" is string. However, there has a common builtin type is not monomorphism, for example: list.

list A is a type when A is a type, so to infer the type of a list we also have to infer the type of its elements and check the rest follow the first one. The edge case is the empty list: no element to look at, so we hand out a fresh freevar as the placeholder.

([expr:list elems]
 (typ:constructor "list"
                  (list (if (empty? elems)
                            (Context/new-freevar! ctx)
                            ; use first element type as type of all elements
                            (let ([elem-typ (type/infer (car elems) ctx)])
                              ; check all elements follow first element type
                              (for-each (lambda ([elem : expr]) (unify elem-typ (type/infer elem ctx)))
                                        (cdr elems))
                              elem-typ)))))

This is where the first freevar of a program usually comes from, and where unify first gets used.

A variable's type comes out of the environment --- and if what we find is a scheme, this is the use site, so instantiate it:

([expr:variable name] (instantiate ctx (Env/lookup (Context-type-env ctx) name)))

instantiate returns anything that is not a scheme unchanged, so lambda parameters and other monomorphic bindings just pass through.

Lambda in the HM system has no annotation on its parameters, so each parameter is bound to a fresh freevar in a new environment. Since multiple parameters are valid in this language, I use a type constructor named pair to group them rather than extending the type definition. Then infer the body under that environment and produce the arrow type:

([expr:lambda params body]
 (let* ([outer-env : Env (Context-type-env ctx)]
        [lambda-env : Env (Env/new outer-env)]
        [param-types (typ:constructor
                      "pair"
                      (map (lambda ([param-name : String])
                             (let ([r (Context/new-freevar! ctx)])
                               (Env/bind-var lambda-env param-name r)
                               r)) params))])
   (set-Context-type-env! ctx lambda-env)
   (let ([body-typ (type/infer body ctx)])
     (set-Context-type-env! ctx outer-env)
     (typ:arrow param-types body-typ))))

The environment is saved and put back around the body. Context holds one mutable environment, so without the restore the parameter would stay visible to whatever is inferred next --- in ((lambda (x) x) x) the second x would resolve to the parameter instead of failing as an unbound variable.

A lambda parameter is never generalized. That is not an omission, it is the definition of the system: a parameter is one type decided by the caller, so it gets one cell. Which is precisely why let has to be its own case.

let is the binding form that generalizes. Infer the right hand side, generalize it against the current environment, then bind the resulting scheme:

([expr:let bindings exp]
 (let* ([outer-env : Env (Context-type-env ctx)]
        [let-env : Env (Env/new outer-env)])
   (for-each (lambda ([bind : (Pairof String expr)])
               (match bind
                 ([cons name init]
                  (Env/bind-var let-env name
                                (generalize outer-env (type/infer init ctx))))))
             bindings)
   (set-Context-type-env! ctx let-env)
   (let ([body-typ (type/infer exp ctx)])
     (set-Context-type-env! ctx outer-env)
     body-typ)))

This single call to generalize is the whole difference between let and lambda, and it is what "let polymorphism" names. It is also what keeps inference decidable: quantification only ever happens at a binding whose right hand side we have already inferred, never at an unknown parameter.

Application needs a few steps:

1. For application (func args ...), infer the type of func.
2. Infer the type of every argument.
3. Assume the return type is a fresh freevar.
4. Unify the function's type with (args ...) -> freevar.
5. Return that freevar as the result.

([expr:application fn args]
 (let ([fn-typ (type/infer fn ctx)]
       [args-typ (map (lambda ((arg : expr)) (type/infer arg ctx)) args)]
       [fresh (Context/new-freevar! ctx)])
   (unify fn-typ (typ:arrow (typ:constructor "pair" args-typ) fresh))
   fresh))

We never check "is this an arrow type" ourselves --- unify does it, and it also solves the argument and result types on the way. If func turns out to be int, the constructor case fails and we get a type error for free.

Put together:

(: type/infer (->* (expr) (Context) typ))
(define (type/infer exp [ctx (Context/new)])
  (match exp
    ([expr:int _] (typ:builtin "int"))
    ([expr:bool _] (typ:builtin "bool"))
    ([expr:string _] (typ:builtin "string"))
    ([expr:list elems]
     (typ:constructor "list"
                      (list (if (empty? elems)
                                (Context/new-freevar! ctx)
                                (let ([elem-typ (type/infer (car elems) ctx)])
                                  (for-each (lambda ([elem : expr]) (unify elem-typ (type/infer elem ctx)))
                                            (cdr elems))
                                  elem-typ)))))
    ([expr:variable name] (instantiate ctx (Env/lookup (Context-type-env ctx) name)))
    ([expr:lambda params body]
     (let* ([outer-env : Env (Context-type-env ctx)]
            [lambda-env : Env (Env/new outer-env)]
            [param-types (typ:constructor
                          "pair"
                          (map (lambda ([param-name : String])
                                 (let ([r (Context/new-freevar! ctx)])
                                   (Env/bind-var lambda-env param-name r)
                                   r)) params))])
       (set-Context-type-env! ctx lambda-env)
       (let ([body-typ (type/infer body ctx)])
         (set-Context-type-env! ctx outer-env)
         (typ:arrow param-types body-typ))))
    ([expr:let bindings exp]
     (let* ([outer-env : Env (Context-type-env ctx)]
            [let-env : Env (Env/new outer-env)])
       (for-each (lambda ([bind : (Pairof String expr)])
                   (match bind
                     ([cons name init]
                      (Env/bind-var let-env name
                                    (generalize outer-env (type/infer init ctx))))))
                 bindings)
       (set-Context-type-env! ctx let-env)
       (let ([body-typ (type/infer exp ctx)])
         (set-Context-type-env! ctx outer-env)
         body-typ)))
    ([expr:application fn args]
     (let ([fn-typ (type/infer fn ctx)]
           [args-typ (map (lambda ((arg : expr)) (type/infer arg ctx)) args)]
           [fresh (Context/new-freevar! ctx)])
       (unify fn-typ (typ:arrow (typ:constructor "pair" args-typ) fresh))
       fresh))))

Polymorphic use across two sites, which is the whole point:

(let ([id (lambda (a) a)]) (let ([x (id 1)]) (id "s")))   =>  string
(let ([id (lambda (a) a)]) id)                            =>  (?1) -> ?1
(let ([id (lambda (a) a)]) '((id 1) (id 2)))              =>  (list int)

The second line is worth a look: the printed variable is ?1, not the ?0 the definition created. That is instantiate handing out a copy.

And the things that must still be rejected:

(lambda (x) (x x))                                 =>  occurs check failed: ?0 in (?0) -> ?1
((lambda (x) (x 1)) 2)                             =>  cannot unify type (int) -> ?1 and int
(let ([f (lambda (a) '(a 1))]) (f "s"))            =>  cannot unify type int and string
(lambda (x) (let ([y x]) '((y 1) (y "s"))))        =>  cannot unify type int and string

The third one is the check on generalize being conservative: the body of f already unified a with int, so there is no free variable left to quantify and f is honestly (int) -> (list int). The fourth is the check on it not over-quantifying.

Damas-Milner's grammar is stratified:

$\sigma$ only ever appears in the environment, as the type of a let-bound variable. $\forall$ is not a type constructor: you cannot write $(\forall \alpha . \; \alpha \to \alpha) \to \text{int}$, because $\forall$ does not fit into $\tau$. So HM's $\forall \alpha . \; \tau$ really is a schema in the original sense of the word --- the same sense as an axiom schema, a template that generates types. instantiate applies the template. It does not eliminate a quantifier, because there is no quantifier there to eliminate.

System F's $\forall \alpha . \; \tau$ is a different object entirely: it lives inside $\tau$, it is a first-class type, and $\Lambda$ is a real abstraction. A dependent $\Pi (A : \text{Type}) . \; A \to A$ likewise. The notation is similar and the reading out loud is similar; the syntactic status is not.

The difference shows up the moment polymorphism has to cross an arrow. Ask for a parameter that is used at two types:

(lambda (f) '((f 1) (f "s")))

This fails with cannot unify type int and string. f is a lambda parameter, and a lambda parameter is bound to one freevar, so the two uses fight over the same cell. Nothing here is a scheme, so there is nothing to instantiate.

The next one is the interesting case, because a scheme really is involved:

(let ([id (lambda (a) a)])
  ((lambda (g) '((g 1) (g "s")))
   id))

Same error. id is a scheme sitting in the environment. But the moment it is passed as an argument it is instantiated to a monotype at the lookup, and g, being a lambda parameter again, could only ever hold a monotype anyway. Polymorphism cannot cross an arrow. That is what rank-1 (or prenex) means, and it is a direct consequence of $\sigma$ not fitting into $\tau$ --- not a shortcut in this implementation.

Is the restriction necessary? It is the price of the inference. With a first-class $\forall$ you need neither a separate category of schemes nor generalize at all: each application site elaborates its own metavariables, so the freshness comes from the site rather than from copying a template. What you give up is that you have to write the polymorphic type down --- typability for System F is undecidableReferenceTypability and type checking in the second-order λ-calculus are equivalent and undecidable1994 · J. B. Wells · 10.1109/lics.1994.316068, so there is no version of this article that infers a first-class $\forall$ for you. HM's stratification is exactly the trade that buys decidable inference.

After we build up a type system, we definitely want to see it work as a language, and make a new language in Racket is crazy easy.

To handle the whole module we overwrite #%module-begin, and we also want #%top-interaction for the REPL (modify main.rkt, which raco pkg new already made):

#lang racket

(require (for-syntax syntax/parse)
         racket/syntax
         syntax/stx)
(require "lang.rkt"
         "semantic.rkt"
         "pretty-print.rkt")

(provide (except-out (all-from-out racket) #%module-begin #%top-interaction)
         (rename-out [module-begin #%module-begin]
                     [top-interaction #%top-interaction]))

(define-syntax (parse stx)
  (define-syntax-class bind
    (pattern (bind-name:id bind-expr)
             #:with bind
             #'(cons (symbol->string 'bind-name) (parse bind-expr))))
  (syntax-parse stx
    [(_ ((~literal let) (binding*:bind ...) body))
     #'(expr:let (list binding*.bind ...) (parse body))]
    [(_ ((~literal lambda) (ps* ...) body))
     #'(expr:lambda (list (symbol->string 'ps*) ...) (parse body))]
    [(_ ((~literal quote) (elem* ...)))
     #'(expr:list (list (parse elem*) ...))]
    [(_ (f arg* ...))
     #'(expr:application (parse f) (list (parse arg*) ...))]
    [(_ v:id) #'(expr:variable (symbol->string 'v))]
    [(_ s:string) #'(expr:string (#%datum . s))]
    [(_ b:boolean) #'(expr:bool (#%datum . b))]
    [(_ i:exact-integer) #'(expr:int (#%datum . i))]))

(define-syntax-rule (module-begin EXPR ...)
  (#%module-begin
   (define all-form (list (parse EXPR) ...))
   (for-each (lambda (form)
               (printf "type:- ~a~n" (pretty-print-typ (type/infer form))))
             all-form)))

(define-syntax-rule (top-interaction . exp)
  (pretty-print-typ (type/infer (parse exp))))

(module reader syntax/module-reader
  hindley-milner)

parse is just mapping S expression onto the expressions defined in lang.rkt. Each clause matches on the shape of the form, and ~literal is what makes let and lambda keywords rather than variables. Note every pattern starts with (_ ...): the macro's own name is the first element of the syntax object.

With the reader submodule in place, #lang hindley-milner is a working language:

#lang hindley-milner

(let ([id (lambda (a) a)])
  (let ([x (id 1)])
    (id "s")))

(lambda (a) a)

(let ([id (lambda (a) a)]) '((id 1) (id 2)))

prints

type:- string
type:- (?0) -> ?0
type:- (list int)

and the REPL gives you a type per input:

> (let ([id (lambda (a) a)]) (id "s"))
"string"

So the system is two mechanisms, not one. unify with a forced mutable ref solves the monotypes, and generalize/instantiate makes a let binding usable at several of them by handing out copies. The first half you would also want in a plain STLC with inference; the second half is what makes it Hindley-Milner, and what makes the inference decidable at the price of $\forall$ being prenex.

I hope detailed implementation and examples show why we need the HM system, and how to make one, and where we would need it. Have a nice day, and it's time for cookies!