Function Types and Polymorphism

In the previous chapter, Bridger’s checker gave every function one fixed type. It rejects this program, which would run without error. id is a lambda that returns whatever it is given, and main calls it twice:

fn main() {
    let id = |x| x;
    println(id(1));
    println(id("one"));    // type mismatch: expected Int, found String
}

If both calls passed integers, as id(1) and id(2), the program would type-check and print 1 and 2. Part V’s compose, written at Int because Int was the only type its signature could name, has the same limit:

fn compose(f: fn(Int) -> Int, g: fn(Int) -> Int) -> fn(Int) -> Int =
    |x: Int| f(g(x));

fn main() {
    let len_plus = compose(|n| n + 1, |s: String| len(s));
    println(len_plus("four"));     // type mismatch: expected Int, found String
}

len is the prelude function that returns the length of a string or list. Neither id nor compose looks at the values it passes along, and each would run without error on the arguments the checker rejects.

The programs raise these questions:

• What type does id have? $\text{fn}(\text{Int})\to \text{Int}$ describes the first call and $\text{fn}(\text{String})\to \text{String}$ the second, but the lambda is checked only once.
• What would a signature for compose have to say? It works whenever g’s result is what f accepts, whatever the three types involved are.
• Where can a type differ from one use to the next? A checker that let every name take a new type at every use would accept id, but it would also accept a reference cell read at a type other than the one written into it.

Bridger answers all three with its function signatures, drawing on work on the types of polymorphic functions that began in the 1960s.

Many types for one function

Christopher Strachey’s lecture notes “Fundamental Concepts in Programming Languages”, given in Copenhagen in 1967 and published in 2000, sorted functions that accept arguments of more than one type into kinds: “There seem to be two main classes, which can be called ad hoc polymorphism and parametric polymorphism.” An ad hoc polymorphic function, such as an arithmetic operator, behaves differently at each type it accepts, and no one rule relates the type of its result to the types of its arguments. A parametric one behaves the same way at every type. Strachey’s example was a function Map that applies a function f to each member of a list, whose type “could be written (α ⇒ β, α list) ⇒ β list where α and β stand for any types.” He left the problem of designing a language with such functions to others.

Languages took it up from two directions. In John Reynolds’s “Towards a Theory of Type Structure” (1974), types are passed to functions as parameters: the polymorphic identity function takes a type t and returns the identity function on t, and a program applies it to a type explicitly before applying the result to a value. CLU, described by Barbara Liskov and colleagues in “Abstraction Mechanisms in CLU” (1977), let a data abstraction take a type parameter. Its sorted_bag took the type of the items it collected as a parameter, and each use named that type, as in sorted_bag[string].

Robin Milner’s 1978 paper, whose unification algorithm the previous chapter described, took the other direction and wrote no types at all. Its first example is map, whose type $((\alpha \to \beta )\times \alpha \text{list})\to \beta \text{list}$ Milner calls its “generic type”. Each occurrence of map gets its own copy of that type, with types substituted for $\alpha$ and $\beta$, so in map(sqroot, map(length, tokl)) the two occurrences are used at two different types. The rule stops at function parameters: “we do not allow different bound occurrences of a λ-bound variable to have different type.” Luis Damas and Milner’s “Principal Type-Schemes for Functional Programs” (1982) proved that the type the algorithm finds for a declaration is its most general one: every other type the declaration could be given is an instance of it.

Bridger’s generics combine the two directions. Its signatures name their type parameters, as Reynolds’s and CLU’s did, and its calls supply them silently, by Milner’s instances.

Signatures and the top-level context

A Bridger program is a set of declarations, and every fn declares its full type: each parameter carries an annotation, and the result type follows -> (an omitted result type is ()). The grammar enforces it. fn f(x) -> Int = 1; is a parse error at the ), where the parser expects a : and a type.

Because each signature is written, the checker knows every function’s type before it has checked any body. It builds the top-level context ${\Gamma }_0$ from the signatures alone, and then checks each body in ${\Gamma }_0$ extended with that function’s parameters. A body may therefore call any function in the program, itself included, wherever in the file that function is declared:

fn is_even(n: Int) -> Bool = if n == 0 { true } else { is_odd(n - 1) };

fn main() {
    println(is_even(10));                               // true
}

fn is_odd(n: Int) -> Bool = if n == 0 { false } else { is_even(n - 1) };

${\Gamma }_0$ is the static counterpart of the program’s environment ${\rho }_0$, which holds every top-level function as a closure capturing ${\rho }_0$ itself. ${\Gamma }_0$ needs no such knot: it holds types, and a type does not refer back to the context it is found in.

The signatures also bound each declaration’s inference. The inference variables of the previous chapter are made and solved while a single body is checked, and all of them must be solved before the checker moves on. A use of is_odd inside is_even reads the written type from ${\Gamma }_0$ and never waits on is_odd’s body, so the bodies can be checked in any order, and a mistake inside one is reported against its own signature.

A global let is added to ${\Gamma }_0$ at its type annotation, or, if it has none, at the type its initializer synthesizes. The determination rule applies to it as to any declaration. let g = |x| x; at the top level is rejected at the lambda: nothing in the declaration fixes the type of x, and a call to g in main cannot fix it, because it belongs to a different declaration.

Type parameters

A signature can name types it does not fix. A declaration may list type parameters in angle brackets after its name, and use them in its parameter and result types:

fn id<T>(x: T) -> T = x;

fn main() {
    println(id(1));                                     // 1
    println(id("one"));                                 // one
}

id’s signature says that for any type T, id takes a T and returns a T. Its type is a type scheme, written

$$\forall T.\text{fn}(T)\to T$$

and read for all T, a function from T to T. The fn types of the previous chapter are schemes with nothing quantified. A function whose type is a scheme is polymorphic, and since the one definition works the same way at every type, this kind of polymorphism is called parametric.

Part V’s compose gets the type it was promised:

fn compose<A, B, C>(f: fn(B) -> C, g: fn(A) -> B) -> fn(A) -> C =
    |x| f(g(x));

fn main() {
    let len_plus = compose(|n| n + 1, |s: String| len(s));
    println(len_plus("four"));                          // 5
    let shout = compose(|s| s ++ "!", |n: Int| to_string(n));
    println(shout(3));                                  // 3!
}

The signature says what the definition requires: g’s result type B must be f’s parameter type, while A and C may be any types. The lambda in the body no longer needs its annotation, since $\text{Chk-Lam}$ checks it against the declared result type and gives x the type A.

Checking a generic body

Inside its own declaration a type parameter is a type the body knows nothing about. It is equal to itself and to nothing else, and no operation is defined on it:

fn bad<T>(x: T) -> T = x + 1;      // type mismatch: expected Int, found T

+ checks each operand against Int, and unification has no way to make T equal to Int. The caller chooses T, and the body has to work for every choice; treating T as Int would make bad an Int function whose signature claimed otherwise. The error is reported at x. A body that passes the check uses its T values only in ways that work for every type. It may return them, pass them to a function that takes a T, store them in a list or a reference cell, or put them in a tuple, as swap does:

fn swap<A, B>(p: (A, B)) -> (B, A) = (p.1, p.0);
// swap((1, "one")) is ("one", 1)

Comparing two T values is also an operation, and it is not defined on every type: Bridger has no == on functions. fn eq<T>(a: T, b: T) -> Bool = a == b; is rejected with type T admits no equality. A type parameter can carry a requirement, such as T: Eq, that admits such operations for the types that meet it; Part IX introduces requirements of that kind. The type parameters in this part carry none.

The checker gets its rule for a generic body from $\text{T-Fn}$. Each function’s scheme goes into ${\Gamma }_0$, and its body is checked with its type parameters standing as types of their own:

$$\frac{{\Gamma }_0=(f:\forall {\vec{T}}_f.\text{fn}({\vec{\tau }}_f)\to {\tau }_f{)}^{\ast }{\Gamma }_0,{\vec{x}}_f:{\vec{\tau }}_f,{\tau }_{ret}={\tau }_f⊢e_f:{\tau }_f\text{for each }f}{⊢(\text{fn}f⟨{\vec{T}}_f⟩({\vec{x}}_f:{\vec{\tau }}_f)\to {\tau }_f=e_f{)}^{\ast }\text{ok}}(\text{T-Fn})$$

${\vec{T}}_f$ is $f$’s list of type parameters. They appear in the second premise only inside ${\vec{\tau }}_f$ and ${\tau }_f$, where each $T$ is a base type distinct from every other type, and ${\Gamma }_0$’s scheme is the only place they are quantified. For a function with no type parameters the rule is Appendix D’s $\text{T-Fn}$.

Instantiation

At a use of a polymorphic function, the scheme’s type parameters are replaced by types. The declarative rule chooses them:

$$\frac{f:\forall T_1\dots T_n.\tau \in \Gamma }{\Gamma ⊢f:\tau [T_1\mapsto {\tau }_1,\dots ,T_n\mapsto {\tau }_n]}(\text{T-Inst})$$

$\tau [T_1\mapsto {\tau }_1,\dots ]$ is $\tau$ with each $T_i$ replaced by ${\tau }_i$, and the rule allows any ${\tau }_i$. id(1) is typed with $T\mapsto \text{Int}$ and id("one") with $T\mapsto \text{String}$, two uses of one rule with different choices.

$\text{T-Inst}$ leaves the choice unstated, as $\text{T-Lam}$ left the parameter types, and the checker resolves it the same way. At each use of a polymorphic name it replaces every type parameter by a fresh inference variable, and the rest of the expression solves them:

1. At id(1), id synthesizes $\text{fn}(\alpha )\to \alpha$ for a fresh $\alpha$.
2. $\text{Syn-App}$ checks 1 against $\alpha$, and unification solves $\alpha$ as Int. The call has type $\alpha$, which is Int.
3. At id("one"), id synthesizes $\text{fn}(\beta )\to \beta$ with another fresh variable, and "one" solves $\beta$ as String.

Each use has its own variables, so what one use solves cannot conflict with another. For len_plus, compose’s A, B, and C become $\alpha$, $\beta$, and $\gamma$. The first argument |n| n + 1 is checked against $\text{fn}(\beta )\to \gamma$, so n has type $\beta$, and n + 1 solves $\beta$ and $\gamma$ as Int. The second argument is then checked against $\text{fn}(\alpha )\to \beta$, which is now $\text{fn}(\alpha )\to \text{Int}$, and its parameter annotation solves $\alpha$ as String. The call has type $\text{fn}(\alpha )\to \gamma$, which is $\text{fn}(\text{String})\to \text{Int}$.

A polymorphic function is instantiated wherever its name is written, including where it is passed as a value. apply(id, 5), with apply from the previous chapter, instantiates id and checks it against $\text{fn}(\text{Int})\to \text{Int}$; map([1, 2, 3], id) and map(["a", "b"], id) instantiate it once each, at Int and at String. The instantiated type is an ordinary function type. A let that binds it binds that one type:

fn main() {
    let f = id;
    println(f(1));
    println(f("one"));     // type mismatch: expected Int, found String
}

id is written once, on the let’s right-hand side, so it is instantiated once, at $\text{fn}(\alpha )\to \alpha$, and f is bound to that type. f(1) solves $\alpha$ as Int, and f("one") then finds an Int parameter.

An instantiation’s variables follow the determination rule like any other. fn nothing<T>() -> [T] = []; called as len(nothing()) leaves its $\alpha$ unsolved, since nothing in the call says what the list holds, and the checker asks for an annotation; let xs: [Int] = nothing(); supplies one.

A let binds one type

The opening program fails for the same reason as let f = id;. $\text{T-Let}$ binds id to the type the lambda synthesized, $\text{fn}(\alpha )\to \alpha$, an ordinary function type containing the unsolved inference variable $\alpha$. Because it has no $\forall$, each use of id looks that type up and uses it as it stands, so both calls share the one $\alpha$. id(1) solves it as Int, and id("one") is checked against that. Two calls at Int agree with the solution, which is why the version with id(2) runs.

In Bridger the only schemes are the ones declarations write. A let, local or global, binds a type with nothing quantified, so every use of the name shares that one type. To use a function at two types, the program declares it at the top level with type parameters.

Generalization

ML, Milner’s language, handles the opening program differently. At a let, its checker turns the right-hand side’s unsolved variables into quantified ones, so let id = |x| x binds id to $\forall \alpha .\text{fn}(\alpha )\to \alpha$, and each use instantiates it afresh. This step is let-generalization, and with it the opening program type-checks. As a rule it reads

$$\frac{\Gamma ⊢e_1:{\tau }_1{\alpha }_1,\dots ,{\alpha }_n\text{ not free in }\Gamma \Gamma ,x:\forall {\alpha }_1\dots {\alpha }_n.{\tau }_1⊢\{rest\}:\tau }{\Gamma ⊢\{\text{let}x=e_1;rest\}:\tau }(\text{HM-Let})$$

with a side condition: only variables that appear nowhere in the context may be quantified. In this declarative rule the ${\alpha }_i$ are type variables that nothing in $\Gamma$ fixes; the algorithm finds them by taking the inference variables that remain unsolved after checking $e_1$ and do not appear in $\Gamma$. A variable that does appear there is shared with a binding outside the let, and the rest of the enclosing declaration may still solve it. In |y| { let k = |z| y; … } the type of k is $\text{fn}(\beta )\to \alpha$, where $\alpha$ is y’s type, so $\beta$ may be quantified and $\alpha$ may not: k ignores its argument, but what it returns is y, whose type is fixed once for the whole lambda.

$\text{HM-Let}$ gives each let the most general scheme its right-hand side has, and a whole program written without a single annotation can be typed. That is the system named for Hindley and Milner, and the design space below sets it beside the signatures Bridger asks for.

Bridger’s polymorphism

Bridger’s functions are polymorphic where a top-level declaration says so. A fn with type parameters has a scheme in ${\Gamma }_0$; inside its body the parameters are types of their own, equal only to themselves; at each use of its name, the checker instantiates the scheme with fresh inference variables and solves them as in the previous chapter. A let never generalizes, so the inference that local lets and lambdas get is the monomorphic inference of the previous chapter, and a type that varies from use to use is always one a signature wrote.

Nothing changes at run time. The evaluator has carried a tag on every value since Part II, and id’s body returns its argument whatever the tag, so the closure for id serves id(1) and id("one") alike. Type parameters exist only in the checker; the evaluator never sees them.

Building it

The declarations reach the checker as the AST of Part I gave them. A fn declaration carries its generics, its annotated parameters, its result type, and its body:

Fn(Generics, Vec<Param>, Ty, Box<Expr>),   // fn f<T: C>(x: T, …) -> T = e

struct Generics { params: Vec<TyParam> }   // <T, U: Show, …>; empty if absent

Inside a declaration’s signature and body, a type parameter T is the named type T, a TyKind::Named with no arguments. unify needs no new case for it: two named types agree when their names and arguments do, so T unifies with T and with nothing else, apart from an unsolved inference variable. Solving a variable as T is allowed: in let ys = []; ys ++ [x] with x : T, the empty list’s element type is solved as T. What cannot happen is the reverse: solving T itself as Int or any other type. Only inference variables are solved, and T is a named type. That is all it takes to make a type parameter mean “some type the body knows nothing about”, and it is where bad’s expected Int, found T comes from.

The provided driver builds ${\Gamma }_0$ and checks each body. It does not copy the top-level signatures into the Ctx it hands check_expr; a Ctx holds only the parameters and local bindings in scope. The program’s declarations are reached through the checker:

impl Checker {
    /// The declaration named `name`, if any.
    pub fn decl(&self, name: &str) -> Option<&Decl>;
}

So the variable arm of check_expr finds a name in one of two places. A name bound in the Ctx has the type bound there, an ordinary monotype, and is used as it is. A name not in the Ctx refers to a top-level declaration, and a fn declaration gives a type built from its signature; when the declaration has type parameters, the arm replaces each one throughout that type with a fresh inference variable from fresh_meta, a new set at every use. Ty::substitute, provided with the AST, replaces type parameters throughout a type, and Milestone M5 supplies the lookups for a global’s type and for the signatures of the prelude’s native functions. The call arm needs no change: by the time a call is checked, its callee’s type has no type parameters left in it, only variables the arguments solve. The variable arm and its instantiation are part of Milestone M5.

The design space

How much is written

ML programs carry almost no types. With let-generalization, the type of every top-level function is inferred, and Damas and Milner’s result guarantees that what is inferred is the most general type the function has. Haskell inherited the inference, and its programmers write top-level signatures by convention anyway, as documentation that the compiler checks. Bridger requires them. The cost is annotations that ML would infer. In return, every polymorphic function’s type is on the page where it is declared, each declaration is checked against its own signature, and an error inside one body is reported there, without ever being blamed on a use in another declaration.

Generalization and reference cells

Let-generalization meets trouble once a language has mutable references. Suppose let r = ref []; were generalized. ref [] has type $\text{ref}⟨[\alpha ]⟩$, and generalizing gives r the scheme $\forall \alpha .\text{ref}⟨[\alpha ]⟩$. Then r := [1] instantiates $\alpha$ as Int, while deref r ++ ["one"] instantiates it as String. Both are accepted, and the program concatenates a list of integers with a list of strings that the checker treated as one list type. The checker has accepted a program that goes wrong. The instances of a scheme are independent only when nothing is shared between the uses, but every use of r reads and writes the same cell. Standard ML’s repair is to generalize a let only when its right-hand side is a lambda, a constant, or a variable, the forms that cannot allocate a cell. Bridger never generalizes, and let r = ref []; binds $\text{ref}⟨[\alpha ]⟩$ with one $\alpha$, solved by its first use, so the problem does not arise.

Who chooses the type

In id(1), the caller chooses T. A function cannot ask for an argument that is itself polymorphic, one the body may use at several types:

fn both<T>(f: fn(T) -> T) -> (Int, String) = (f(1), f("one"));
// type mismatch: expected T, found Int

both wants an f that works at Int and at String, but T is the caller’s choice, and inside the body it is a type of its own, so f(1) is rejected at 1. A type system can allow the quantifier inside a parameter’s type, so that both takes an argument of type $\forall T.\text{fn}(T)\to T$. Reynolds’s system has such types, and so do the extensions of Haskell that admit them. The price is inference: for those types in general it is undecidable, as J. B. Wells proved in 1999, so a language with them asks for annotations wherever such a type is used. Bridger’s schemes, with every quantifier at the front of a top-level signature, need none beyond the signature.

How generic code runs

A polymorphic function must run on values of whatever types it is instantiated at, and implementations meet that requirement in two ways. The first is a uniform representation. Every value has the same shape in memory, typically a pointer, so a single compiled version of the function handles every instantiation. ML implementations do this, and so does Java, whose generics were added in 2004 and are checked by the compiler and then erased, leaving one class for every instantiation. The second is to compile a separate copy of the function for each instantiation the program uses, with the type parameters replaced by the actual types. C++ templates work this way, and so do Rust’s generics; each copy is specialized to its types, at the cost of a larger program. Bridger’s evaluator has a uniform representation by construction, since every runtime value is a tagged Value.

Further reading

Parametric polymorphism and inference: Milner’s “A Theory of Type Polymorphism in Programming” (1978) presents let-polymorphism with the algorithm 𝒲 and its soundness proof. Damas and Milner’s “Principal Type-Schemes for Functional Programs” (1982) states the inference system as rules and proves that every typable expression has a most general type. Pierce’s Types and Programming Languages (MIT Press, 2002) covers let-polymorphism in chapter 22 and explicit polymorphism, with quantifiers anywhere in a type, in chapter 23.

What a type says about its functions: Philip Wadler’s “Theorems for Free!” (1989) shows that a polymorphic function’s type alone implies equations that every function of that type satisfies; from the type $\forall T.\text{fn}([T])\to [T]$ it derives that such a function commutes with map.

Concept checks