Standardizing

As a result of, e.g., currying, the shape of a function type may change in the course of a type-checking/inference process. Type comparison may thus be tested on various structurally different, although syntactically congruent, forms of a same type. A type must therefore assume a canonical form in order to be compared. This is what standardizing a type does. This is a two-fold operation that:

1. flattens the domains of function types; and,

2. renames the type parameters.

The flattening phase simply amounts to applying Equation (4.1) as a rewrite rule, although backwards (i.e., from right to left) and as much as possible. The second (renaming) phase consists in making a consistent copy of all types reachable from a type's root.