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:
“Lise: Look, monsieur, I don’t know what type of girl you think I am, but I’m not. And now I would like to return to my friends.
Jerry: I thought you were bored with them. You sure looked it.
Lise: You should see me now.
Jerry: Ouch.”
—Alan Jay Lerner (1918–1986)
“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)