🌐 한국어로 읽기

Background for chapter 09.

Hindley-Milner, gently

This is not a tutorial on Hindley-Milner in general — textbook HM comes with generalization, an occurs check, and let-polymorphism baked in. This describes the specific checker MicroHs actually shipped first, src/MicroHs/TypeCheck.hs as of cc57346e ("First version with type checking.", 2023-08-06). Every claim below is checked against that file, at that commit, or against a program actually run through the cc57346e build.

Types are terms

The hook, and the thing every other section depends on: MicroHs does not have a separate type-syntax AST. 33b009fa ("Use Expr for EType.", 2023-07-21) deletes the three-constructor EType that had existed since chapter 08's db418344 (TVar/TConstr/TUVar) and replaces it with a type synonym for the same Expr that already represents terms (33b009fa:src/MicroHs/Parse.hs lines 99–111, quoted whole):

-- Expr restricted to
--  * after desugaring: EApp and EVar
--  * before desugaring: EApp, EVar, ETuple, EList
type EType = Expr

validType :: Expr -> Bool
validType ae =
  case ae of
    EVar _ -> True
    EApp f a -> validType f && validType a
    EList es -> length es <= 1 && all validType (take 1 es)
    ETuple es -> all validType es
    _ -> False

A type is just an Expr that satisfies validType — a type variable and a type constructor are both EVar, a type application (Maybe Int, [a], a -> b) is EApp, and there's no separate parser production for types at all: pType runs the ordinary expression parser and checks validType on what comes back (33b009fa:src/MicroHs/Parse.hs lines 450–454). This carries all the way into the checker — a metavariable (textbook HM's α, β, ...) is one more constructor on the same Expr type (cc57346e:src/MicroHs/Parse.hs lines 56–78, quoted in part, ... marking constructors omitted from the middle):

data Expr
  = EVar Ident
  | EApp Expr Expr
  ...
  | EBad
  -- Only while type checking
  | EUVar Int
  -- Constructors after type checking
  | ECon ConTyInfo Ident
  --Xderiving (Show, Eq)

There is no Type module and not even a separate Kind type — type EKind = EType (cc57346e:src/MicroHs/Parse.hs line 133). Terms, types, and kinds are one recursive datatype throughout.

Metavariables and substitution, as implemented

An unknown type is EUVar Int, just an integer tag. The substitution that resolves those tags is a single IM.IntMap EType in the checker's own state (cc57346e:src/MicroHs/TypeCheck.hs line 132):

data TCState = TC IdentModule Int TypeTable ValueTable (IM.IntMap EType)

The Int next to it is a fresh-name counter; newUVar bumps it and returns EUVar n (cc57346e:src/MicroHs/TypeCheck.hs lines 338–342). Recording a solution is a plain map insert, addUVar (cc57346e:src/MicroHs/TypeCheck.hs lines 254–262, quoted whole):

addUVar :: Int -> EType -> T ()
addUVar i t = T.do
  let
    add = T.do
      TC mn n tenv venv sub <- get
      put (TC mn n tenv venv (IM.insert i t sub))
  case t of
    EUVar j -> if i == j then T.return () else add
    _ -> add

The one check here is i == j — refuse to insert i ↦ EUVar i. That is the entire safety net; there is no deeper occurs check, and "What this checker leaves out" below shows what that costs. Reading a solution back out chases the map recursively (derefUVar, cc57346e:src/MicroHs/TypeCheck.hs lines 291–300, quoted whole):

derefUVar :: EType -> T EType
derefUVar at =
  case at of
    EApp f a -> EApp <$> expandType f <*> expandType a
    EUVar i -> T.do
      sub <- gets uvarSubst
      case IM.lookup i sub of
        Nothing -> T.return at
        Just t -> derefUVar t
    _ -> T.return at

expandType (lines 270–273) is derefUVar followed by expandSyn, which does the same kind of lookup against a different map — type synonyms. And replacing a named type variable (what forall-instantiation needs) is separate again: subst, a plain syntactic walk (cc57346e:src/MicroHs/Parse.hs lines 759–768, quoted whole):

subst :: [(Ident, Expr)] -> Expr -> Expr
subst s =
  let
    sub ae =
      case ae of
        EVar i -> fromMaybe ae $ lookupBy eqIdent i s
        EApp f a -> EApp (sub f) (sub a)
        EUVar _ -> ae
        _ -> error "subst unimplemented"
  in sub

Three mechanisms, three pieces of state, all on the one Expr type.

Unification, traced by hand

unify/unifyR (cc57346e:src/MicroHs/TypeCheck.hs lines 302–330, quoted whole) is the whole algorithm — dereference both sides, then compare structurally:

unify :: HasCallStack => EType -> EType -> T ()
unify a b = T.do
  aa <- expandType a
  bb <- expandType b
  unifyR aa bb
  
unifyR :: HasCallStack => EType -> EType -> T ()
unifyR a b = T.do
  venv <- gets valueTable
  tenv <- gets typeTable
  let bad = error $ "Cannot unify " ++ showExpr a ++ " and " ++ showExpr b ++ "\n" ++
                    show a ++ " - " ++ show b ++ "\n" ++
                    show tenv ++ "\n" ++
                    show venv
  case a of
    EVar ia ->
      case b of
        EVar ib  -> if eqIdent ia ib then T.return () else bad
        EApp _ _ -> bad
        EUVar i  -> addUVar i a
        _        -> impossible
    EApp fa xa ->
      case b of
        EVar _     -> bad
        EApp fb xb -> T.do { unify fa fb; unify xa xb }
        EUVar i    -> addUVar i a
        _          -> impossible
    EUVar i -> addUVar i b
    _ -> impossible

Four cases, because a desugared EType only contains EVar/EApp/EUVar: two constructor names must match exactly by identifier; two applications unify head and argument separately (this is how a -> b against Int -> Char splits in two, since tArrow a r = EApp (EApp (EVar "Primitives.->") a) r); a metavariable on either side just records a binding.

Trace 1 — the call const 5 'x', where const :: forall a b . a -> b -> a has been freshened at the use site to EUVar 2 -> EUVar 3 -> EUVar 2 (see tInst below) — the application's result metavariable τ (EUVar 1) is allocated before tInst freshens the scheme, so it carries the lowest fresh number, not the highest. Checking the application unifies the freshened scheme against Int -> (Char -> τ): unify (EUVar 2) Int → addUVar 2 Int; unify (EUVar 3) Char → addUVar 3 Char; unify (EUVar 1) (EUVar 2) → unify runs expandType on both sides first, and 2 ↦ Int is already in the map, so the binding recorded is addUVar 1 Int directly — no two-hop chase. Dereferencing τ afterward reads 1 ↦ Int — the call's result type is Int.

Trace 2 — a failing unification, run for real: bad2 :: forall a b . a -> b -> a; bad2 x y = x + 1 fails with Cannot unify a and Primitives.Int, because inside bad2's own body the signature's a is a literal, un-instantiated EVar name (why: next section) — unifyR's EVar/EVar case runs with ia = "a", ib = "Primitives.Int", eqIdent is false, and bad fires. No metavariable involved at all.

forall, instantiation, and rigid type variables

f7db30f1 ("Add lots of type signatues and forall.", 2023-07-23) adds forall across the standard library — 9 files, 134 insertions, 74 deletions, all under lib/ plus the Makefile. Most touched functions already had a signature; what's new is the quantifier (f7db30f1:lib/Data/Function.hs, quoted in part: . and id omitted after the first ..., flip omitted after the second, uncurry omitted after fix — each of those four just gains a forall the same way ($) does):

-($) :: (a -> b) -> a -> b
+($) :: forall a b . (a -> b) -> a -> b
...
-const :: a -> b -> a
+const :: forall a b . a -> b -> a
...
+fix :: forall a . (a -> a) -> a
 fix = primFix

Why the quantifier matters is mechanical. ETypeScheme [Ident] EType carries an explicit list of bound names (cc57346e:src/MicroHs/Parse.hs line 130), and the parser only populates it when it sees the keyword (cc57346e:src/MicroHs/Parse.hs lines 484–488, quoted whole):

pTypeScheme :: P ETypeScheme
pTypeScheme = P.do
  vs <- (pKeyword "forall" *> esome pLIdent <* pSym '.') <|< pure []
  t <- pType
  pure $ ETypeScheme vs t

Checking a signature (tcTypeScheme, lines 485–488 of TypeCheck.hs) brings exactly the names in vs into scope; a name never quantified is simply not in scope. Confirmed by deleting the quantifier from const's signature in the cc57346e worktree (const :: a -> b -> a, no forall) and compiling a program that uses it:

mhs: undefined variable a
CallStack (from HasCallStack):
  error, called at src/MicroHs/TypeCheck.hs:354:16 in main:MicroHs.TypeCheck

— the checker fails on const's signature, never reaching its body. Without forall a polymorphic-looking signature is ill-formed, which is why f7db30f1 had to sweep the library two weeks before cc57346e could accept any of it.

What makes a definition polymorphic, then, given that there is no generalization step anywhere in this file? tInst freshens a scheme's bound names to new metavariables only at a use site — every EVar reference goes through tLookupInst (cc57346e:src/MicroHs/TypeCheck.hs lines 364–371, quoted whole):

tInst :: ETypeScheme -> T EType
tInst as =
  case as of
    ETypeScheme vs t ->
      if null vs then T.return t
      else T.do
        us <- mapM (const newUVar) (replicate (length vs) ())
        T.return (subst (zip vs us) t)

But when the checker verifies the definition itself, tcDefValue (lines 526–536) checks the body against the declared type verbatim — still containing the literal identifiers a/b, not fresh metavariables. Since unifyR's EVar/EVar case demands identical names, a behaves as a rigid, opaque constant for that one definition's check — exactly what the bad2 failure above shows. Two consequences: (1) polymorphism = rigid check at the definition plus fresh instantiation at every call site (verified: one program calling const 5 'x' and const "hi" 42 compiles and prints 5 then "hi"); (2) with no generalization, every top-level binding needs an explicit signature to be checked at all — the next section shows what a missing one costs.

What this checker leaves out

Checked directly against the file, not assumed from familiarity with "real" Hindley-Milner:

• No occurs check. addUVar's only guard is i ↦ EUVar i itself; it never checks whether t contains EUVar i nested deeper. \x -> x x unifies x's metavariable with x's-metavariable -> τ, a cycle addUVar happily records — no "infinite type" error. Run for real (cc57346e build, ulimit -v 2000000): a program with that lambda in an unused let dies with mhs: out of memory, derefUVar chasing the substitution's own cycle. (Unbounded, the same run consumed tens of gigabytes of host RAM before being killed — genuine non-termination, not a hypothetical.)
• No let-polymorphism for local bindings. tcBinds gives each local binding one fresh metavariable in an empty scheme, ETypeScheme [] (cc57346e:src/MicroHs/TypeCheck.hs line 708), so tInst on it is the null vs case — no freshening, ever. A local function used at two different types — textbook let-generalization's whole reason to exist — is a hard "Cannot unify" error here.
• Mutual recursion is an open gap, by the code's own admission. tcBinds carries -- XXX No mutual recursion yet (line 703). Tested at cc57346e: a single self-recursive local function works (let countdown n = if n == 0 then 0 else countdown (n - 1) runs to 0), but two local functions calling each other fail — one stage after type checking, at name resolution: mhs: undefined: isOdd, from src/MicroHs/Main.hs's linking pass.
• No type classes. grep -in "class" over Parse.hs and TypeCheck.hs at cc57346e returns nothing — no AST case, no dictionaries. do-notation still resolves (>>=)/(>>) by explicit module qualifier (chapter 03), not a Monad constraint.
• Kinds exist, but only just. EKind is EType again, checked against the single sentinel kType = EVar "Type" (lines 228–229) — enough to reject an arity mismatch like data Foo a = Foo (a Int), but every type variable has kind Type and there is no * -> *-and- beyond machinery.

Worked example: const

lib/Data/Function.hs (cc57346e):

const :: forall a b . a -> b -> a
const x _ = x

Hand-inferring the way tcDefValue does — walking ELam "x" (ELam "_" (EVar "x")) against the declared a -> b -> a, with a/b in scope as rigid names:

1. Outer ELam "x" e, expected a -> (b -> a). A fresh metavariable τ₁ stands for x's type; the body is checked with no expected type (ELam's case recurses with Nothing, unifying afterward), with x : τ₁ in the environment.
2. Inner ELam "_" (EVar "x"): fresh τ₂ for _; the body looks up x and returns τ₁. The inner lambda's type is τ₂ -> τ₁.
3. The outer lambda's constructed type, τ₁ -> (τ₂ -> τ₁), is unified against a -> (b -> a): τ₁ ↦ a, τ₂ ↦ b, and the return-position unify τ₁ a resolves to unifyR (EVar "a") (EVar "a") — succeeds by eqIdent.

Every metavariable resolves to the signature's own a/b, no contradiction — the body checks against forall a b . a -> b -> a, matching the source. Against the real checker (cc57346e worktree, -ilib on the actual lib/ tree):

$ cat > ConstDemo.hs <<'EOF'
module ConstDemo(module ConstDemo) where
import Prelude

main :: IO ()
main = do
  putStrLn (showInt (const 5 'x'))
  putStrLn (const "hi" 42)
EOF
$ nix develop $MICROHS -c ./bin/mhs -ilib ConstDemo
$ nix develop $MICROHS -c ./bin/eval
5
hi

const 5 'x' instantiates a ↦ Int, b ↦ Char; const "hi" 42 instantiates a ↦ [Char], b ↦ Int — two independent instantiations of the one rigid-checked definition, exactly as tInst predicts.