Type System - Explicit or Implicit Declaration and Inference

Explicit or Implicit Declaration and Inference

For more details on this topic, see Type inference.

Many static type systems, such as those of C and Java, require type declarations: The programmer must explicitly associate each variable with a particular type. Others, such as Haskell's, perform type inference: The compiler draws conclusions about the types of variables based on how programmers use those variables. For example, given a function f(x, y) that adds x and y together, the compiler can infer that x and y must be numbers – since addition is only defined for numbers. Therefore, any call to f elsewhere in the program that specifies a non-numeric type (such as a string or list) as an argument would signal an error.

Numerical and string constants and expressions in code can and often do imply type in a particular context. For example, an expression 3.14 might imply a type of floating-point, while might imply a list of integers – typically an array.

Type inference is in general possible, if it is decidable in the type theory in question. Moreover, even if inference is undecidable in general for a given type theory, inference is often possible for a large subset of real-world programs. Haskell's type system, a version of Hindley-Milner, is a restriction of System Fω to so-called rank-1 polymorphic types, in which type inference is decidable. Most Haskell compilers allow arbitrary-rank polymorphism as an extension, but this makes type inference undecidable. (Type checking is decidable, however, and rank-1 programs still have type inference; higher rank polymorphic programs are rejected unless given explicit type annotations.)

Read more about this topic:  Type System

Famous quotes containing the words explicit, implicit, declaration and/or inference:

    Like dreaming, reading performs the prodigious task of carrying us off to other worlds. But reading is not dreaming because books, unlike dreams, are subject to our will: they envelop us in alternative realities only because we give them explicit permission to do so. Books are the dreams we would most like to have, and, like dreams, they have the power to change consciousness, turning sadness to laughter and anxious introspection to the relaxed contemplation of some other time and place.
    Victor Null, South African educator, psychologist. Lost in a Book: The Psychology of Reading for Pleasure, introduction, Yale University Press (1988)

    The true colour of life is the colour of the body, the colour of the covered red, the implicit and not explicit red of the living heart and the pulses. It is the modest colour of the unpublished blood.
    Alice Meynell (1847–1922)

    It is an axiom in political science that unless a people are educated and enlightened it is idle to expect the continuance of civil liberty or the capacity for self-government.
    —Texas Declaration of Independence (March 2, 1836)

    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)