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:
“I can barely conceive of a type of beauty in which there is no Melancholy.”
—Charles Baudelaire (1821–1867)
“I shouldn’t want you to be surprised, or to draw any particular inference from my making speeches, or not making speeches, out there. I don’t recall any candidate for President that ever injured himself very much by not talking.”
—Calvin Coolidge (1872–1933)