Type Inference
Unification is used during type inference, for instance in the functional programming language Haskell. On one hand, the programmer does not need to provide type information for every function, on the other hand it is used to detect typing errors. The Haskell expression 1: is not correctly typed, because the list construction function ":" is of type a->-> and for the first argument "1" the polymorphic type variable "a" has to denote the type Int whereas "" is of type, but "a" cannot be both Char and Int at the same time.
Like for prolog an algorithm for type inference can be given:
- Any type variable unifies with any type expression, and is instantiated to that expression. A specific theory might restrict this rule with an occurs check.
- Two type constants unify only if they are the same type.
- Two type constructions unify only if they are applications of the same type constructor and all of their component types recursively unify.
Due to its declarative nature, the order in a sequence of unifications is (usually) unimportant.
Note that in the terminology of first-order logic, an atom is a basic proposition and is unified similarly to a Prolog term.
Read more about this topic: Unification (computer Science)
Famous quotes containing the words type and/or inference:
“It took six weeks of debate in the Senate to get the Arms Embargo Law repealed—and we face other delays during the present session because most of the Members of the Congress are thinking in terms of next Autumn’s election. However, that is one of the prices that we who live in democracies have to pay. It is, however, worth paying, if all of us can avoid the type of government under which the unfortunate population of Germany and Russia must exist.”
—Franklin D. Roosevelt (1882–1945)
“Rules and particular inferences alike are justified by being brought into agreement with each other. A rule is amended if it yields an inference we are unwilling to accept; an inference is rejected if it violates a rule we are unwilling to amend. The process of justification is the delicate one of making mutual adjustments between rules and accepted inferences; and in the agreement achieved lies the only justification needed for either.”
—Nelson Goodman (b. 1906)