All right, finally we are getting to typing judgments, which are the bread and butter of type inference algorithms. We said in the previous episode that the values that are manipulated by a program written in Exp are either values of primitive types, or functions from one value to another, and that this set of values is called V:

To each monotype μ corresponds a subset V , as detailed in [5];
if v∈V is in the subset for μ we write v:μ.

Recall that a monotype is a type with no “generic” type arguments. So for instance, the monotype int has values that are all possible integers. The monotype int → int has values like “the function that takes an integer and doubles it”. This syntax simply means that the value on the left of the colon is an instance of the monotype on the right.

Further we write v:τ if v:μ for every monotype instance μ of τ, 
and we write  v:σ if v:τ for every τ which is a generic instance
of σ.

Let’s consider an example. Suppose we have the identity function λx.x and the type scheme ∀β(β → β). We could make an instance of that type scheme, say int → int. Plainly λx.x is a function that takes ints and returns ints. In fact, for any instance of that type scheme, the identity function fits the bill. So we say that λx.x:∀β(β → β).

Note that if there were even a single instance of the scheme that did not match the function, then we could not make the judgment that the function is a member of that type scheme. For example, suppose we have a function square that takes an int and returns its square. We cannot say that square:∀β(β → β) because square is not a member of, say, (int → int) → (int → int).

Next time: what is an “environment”?