MetaPRL Type Inference Resource

The type inference resource provides the base resource for the type inference algorithm. The resource has the following declarations:

type typeinf_func = unify_subst -> term -> unify_subst * term
type typeinf_comp = typeinf_func -> typeinf_func
type typeinf_resource_info = term * typeinf_comp
type typeinf_data
resource (typeinf_resource_info, typeinf_func, typeinf_data) typeinf_resource

The type inference algorithm is an extension of Algorithm W. A type inference component taks a partial unification of variables to types, and a term, and it produces a new partial unification, togher with a term representing the type of the term argument.

Components are added to the type inference algorithm by specifying a pattern for the inference, and a function to produce the type inference component. Examples of type inference components are in modules for the ITT theory.