Unification (computer Science) - Type Inference

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:

  1. 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.
  2. Two type constants unify only if they are the same type.
  3. 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:

    Mediocre people have an answer for everything and are astonished at nothing. They always want to have the air of knowing better than you what you are going to tell them; when, in their turn, they begin to speak, they repeat to you with the greatest confidence, as if dealing with their own property, the things that they have heard you say yourself at some other place.... A capable and superior look is the natural accompaniment of this type of character.
    Eugène Delacroix (1798–1863)

    The inference is, that God has restated the superiority of the West. God always does like that when a thousand white people surround one dark one. Dark people are always “bad” when they do not admit the Divine Plan like that. A certain Javanese man who sticks up for Indonesian Independence is very lowdown by the papers, and suspected of being a Japanese puppet.
    Zora Neale Hurston (1891–1960)