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”?

### Like this:

Like Loading...

*Related*

Even so, the game does punish players of this play style in its latter stages, so if you have been button mashing

Square or Triangle up until this point, you will struggle.