CSC448: Type Checking Revisited: Substitutions and Instances [115/133]

Consider the following grammar for types:

t, u ::= int
       | string
       | 'a          (type variable)
       | t list      (list of t)
       | t -> u      (functions from t to u)
        

A substitution is a map from type variables to other types. Applying a substitution replaces type variables whenever they are in the domain of the map.

If a type t can be obtained by applying a substitution to another type u, then we write t <= u.

What is the relationship between the following types?

'a list
'b list
int list
string list
('b -> 'c) list
('c -> 'b) list
(int -> 'c) list
('b -> string) list
(int -> string) list
(int -> int) list
(string -> string) list
('d -> 'd) list
        

Now we can say that the type inference process should find the maximum element (assuming that there are any maximal elements and that there is only one maximal element). We have to work up to the equivalence induced by the preorder <=.

See p370 of the Dragon book.