Excessive explanation, part fourteen

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 I1/4 corresponds a subset V , as detailed in [5];if vaV is in the subset for I1/4 we write v:I1/4.

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 a' 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:I if v:I1/4 for every monotype instance I1/4 of I, and we write v:If if v:I for every I which is a generic instanceof If.

Let's consider an example. Suppose we have the identity function Ix.x and the type scheme aI^2(I^2 a' I^2). We could make an instance of that type scheme, say int a' int. Plainly Ix.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 Ix.x:aI^2(I^2 a' I^2).

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:aI^2(I^2 a' I^2) because square is not a member of, say, (int a' int) a' (int a' int).

Next time: what is an "environment"?