This article may be too technical for most readers to understand. Please help improve this article to make it understandable to non-experts, without removing the technical details. The talk page may contain suggestions. (October 2010)

This article includes a list of references, related reading or external links, but its sources remain unclear because it lacks inline citations. Please improve this article by introducing more precise citations. (October 2010)

A type system associates a type with each computed value. By examining the flow of these values, a type system attempts to ensure or prove that no type errors can occur. The particular type system in question determines exactly what constitutes a type error, but in general the aim is to prevent operations expecting a certain kind of value being used with values for which that operation does not make sense (logic errors); memory errors will also be prevented. Type systems are often specified as part of programming languages, and built into the interpreters and compilers for them; although they can also be implemented as optional tools.

In computer science, a type system may be defined as "a tractable syntactic framework for classifying phrases according to the kinds of values they compute".^[1]

A compiler may also use the static type of a value to optimize the storage it needs and the choice of algorithms for operations on the value. In many C compilers the Unknown extension tag "source" data type, for example, is represented in 32 bits, in accord with the IEEE specification for single-precision floating point numbers. They will thus use floating-point-specific microprocessor operations on those values (floating-point addition, multiplication, etc.).

The depth of type constraints and the manner of their evaluation affect the typing of the language. A programming language may further associate an operation with varying concrete algorithms on each type in the case of type polymorphism. Type theory is the study of type systems, although the concrete type systems of programming languages originate from practical issues of computer architecture, compiler implementation, and language design.

Fundamentals[link]

Assigning data types (typing) gives meaning to sequences of bits. Types usually have associations either with values in memory or with objects such as variables. Because any value simply consists of a sequence of bits in a computer, hardware makes no intrinsic distinction even between memory addresses, instruction code, characters, integers and floating-point numbers, being unable to discriminate between them based on bit pattern alone. Associating a sequence of bits and a type informs programs and programmers how that sequence of bits should be understood.

Advantages provided by type systems include:

• Abstraction (or modularity) – Types allow programmers to think about programs at a higher level than the bit or byte, not bothering with low-level implementation. For example, programmers can think of a string as a collection of character values instead of as a mere array of bytes. Or, types can allow programmers to express the interface between two subsystems. This helps localize the definitions required for interoperability of the subsystems and prevents inconsistencies when those subsystems communicate.
• Documentation – In more expressive type systems, types can serve as a form of documentation, since they can illustrate the intent of the programmer. For instance, timestamps may be represented as integers—but if a programmer declares a function as returning a timestamp type rather than merely an integer type, this documents part of the meaning of the function.
• Optimization – Static type-checking may provide useful compile-time information. For example, if a type requires that a value must align in memory at a multiple of four bytes, the compiler may be able to use more efficient machine instructions.
• Safety – Use of types may allow a compiler to detect meaningless or probably invalid code. For example, we can identify an expression 3 / "Hello, World" as invalid, because the rules of arithmetic do not specify how to divide an integer by a string. As discussed below, strong typing offers more safety, but generally does not guarantee complete safety (see type safety for more information).

Strong type systems can also have a downside, particularly with regard to forcing the programmer to engage in the unnecessary "bookkeeping" of making unnecessary explicit conversions in contexts where an implicit conversion would cause no harm. Pascal's type system has been described as "too strong", because the size of an array or string is part of its type, making some programming tasks very difficult.^[2][3] On the contrary, in some languages, such as Haskell, types are automatically inferred, so despite the strong type system, (most) type annotations are unnecessary.

Type safety contributes to program correctness, but cannot guarantee it unless the type checking itself becomes an undecidable problem. Depending on the specific type system, a program may give the wrong result and be safely typed, producing no compiler errors. For instance, division by zero is not caught by the type checker in most programming languages; instead it is a runtime error. To prove the absence of more general defects, other kinds of formal methods, collectively known as program analyses, are in common use, as well as software testing, a widely used empirical method for finding errors that the type checker cannot detect.

A program typically associates each value with one particular type (although a type may have more than one subtype). Other entities, such as objects, modules, communication channels, dependencies, or even types themselves, can become associated with a type. Some implementations might make the following identifications (though these are technically different concepts):

• class – a type of an object
• data type – a type of a value
• kind – a type of a type

A type system, specified for each programming language, controls the ways typed programs may behave, and makes behavior outside these rules illegal. An effect system typically provides more fine-grained control than does a type system.

Formally, type theory studies type systems. More elaborate type systems (such as dependent types) allow for finer-grained program specifications to be verified by a type checker, but this comes at a price, as type inference and other properties generally become undecidable, and type checking itself is dependent on user-supplied proofs. It is challenging to find a sufficiently expressive type system that satisfies all programming practices in type safe manner. As Mark Manasse concisely put it:^[4]

The fundamental problem addressed by a type theory is to insure that programs have meaning. The fundamental problem caused by a type theory is that meaningful programs may not have meanings ascribed to them. The quest for richer type systems results from this tension.

Type checking[link]

The process of verifying and enforcing the constraints of types – type checking – may occur either at compile-time (a static check) or run-time (a dynamic check). If a language specification requires its typing rules strongly (i.e., more or less allowing only those automatic type conversions that do not lose information), one can refer to the process as strongly typed, if not, as weakly typed. The terms are not usually used in a strict sense.

Static typing[link]

A programming language is said to use static typing when type checking is performed during compile-time as opposed to run-time. Statically typed languages include ActionScript 3, Ada, C, D, Eiffel, F#, Fortran, Go, Haskell, haXe, JADE, Java, ML, Objective-C, OCaml, Pascal, and Scala. C++ is statically typed, aside from its run-time type information system. The C# type system performs static-like compile-time type checking, but also includes full runtime type checking. Perl is statically typed with respect to distinguishing arrays, hashes, scalars, and subroutines.

Static typing is a limited form of program verification (see type safety): accordingly, it allows many type errors to be caught early in the development cycle. Static type checkers evaluate only the type information that can be determined at compile time, but are able to verify that the checked conditions hold for all possible executions of the program, which eliminates the need to repeat type checks every time the program is executed. Program execution may also be made more efficient (e.g. faster or taking reduced memory) by omitting runtime type checks and enabling other optimizations.

Because they evaluate type information during compilation and therefore lack type information that is only available at run-time, static type checkers are conservative. They will reject some programs that may be well-behaved at run-time, but that cannot be statically determined to be well-typed. For example, even if an expression <complex test> always evaluates to true at run-time, a program containing the code

if <complex test> then 42 else <type error>

will be rejected as ill-typed, because a static analysis cannot determine that the else branch won't be taken.^[1] The conservative behaviour of static type checkers is advantageous when <complex test> evaluates to false infrequently: A static type checker can detect type errors in rarely used code paths. Without static type checking, even code coverage tests with 100% coverage may be unable to find such type errors. The tests may fail to detect such type errors, because the combination of all places where values are created and all places where a certain value is used must be taken into account.

The most widely used statically typed languages are not formally type safe. They have "loopholes" in the programming language specification enabling programmers to write code that circumvents the verification performed by a static type checker and so address a wider range of problems. For example, most C-style languages have type punning, and Haskell has such features as unsafePerformIO: such operations may be unsafe at runtime, in that they can cause unwanted behaviour due to incorrect typing of values when the program runs.

Dynamic typing[link]

A programming language is said to be dynamically typed when the majority of its type checking is performed at run-time as opposed to at compile-time. In dynamic typing values have types, but variables do not; that is, a variable can refer to a value of any type. Dynamically typed languages include APL, Erlang, Groovy, JavaScript, Lisp, Lua, MATLAB, GNU Octave, Perl (for user-defined types, but not built-in types), PHP, Pick BASIC, Prolog, Python, Ruby, Smalltalk and Tcl.

Implementations of dynamically typed languages generally associate run-time objects with "tags" containing their type information. This run-time classification is then used to implement type checks and dispatch overloaded functions, but can also enable pervasive uses of dynamic dispatch, late binding and similar idioms that would be cumbersome at best in a statically typed language, requiring the use of variant types or similar features.

More broadly, as explained below, dynamic typing can improve support for dynamic programming language features, such as generating types and functionality based on run-time data. (Nevertheless, dynamically typed languages need not support any or all such features, and some dynamic programming languages are statically typed.) On the other hand, dynamic typing provides fewer a priori guarantees: a dynamically typed language accepts and attempts to execute some programs that would be ruled as invalid by a static type checker, either due to errors in the program or due to static type checking being too conservative.

Dynamic typing may result in runtime type errors—that is, at runtime, a value may have an unexpected type, and an operation nonsensical for that type is applied. Such errors may occur long after the place where the programming mistake was made—that is, the place where the wrong type of data passed into a place it should not have. This may make the bug difficult to locate.

Dynamically typed language systems' run-time checks can potentially be more sophisticated than those of statically typed languages, as they can use dynamic information as well as any information from the source code. On the other hand, runtime checks only assert that conditions hold in a particular execution of the program, and the checks are repeated for every execution of the program.

Development in dynamically typed languages is often supported by programming practices such as unit testing. Testing is a key practice in professional software development, and is particularly important in dynamically typed languages. In practice, the testing done to ensure correct program operation can detect a much wider range of errors than static type-checking, but full test coverage over all possible executions of a program (including timing, user inputs, etc.), if even possible, would be extremely costly and impractical. Static typing helps by providing strong guarantees of a particular subset of commonly made errors never occurring

Combinations of dynamic and static typing[link]

The presence of static typing in a programming language does not necessarily imply the absence of all dynamic typing mechanisms. For example, Java and some other ostensibly statically typed languages, support downcasting and other type operations that depend on runtime type checks, a form of dynamic typing. More generally, most programming languages include mechanisms for dispatching over different 'kinds' of data, such as disjoint unions, polymorphic objects, and variant types: Even when not interacting with type annotations or type checking, such mechanisms are materially similar to dynamic typing implementations. See programming language for more discussion of the interactions between static and dynamic typing.

Certain languages, for example Clojure or Cython, are dynamically typed by default, but allow this behaviour to be overridden through the use of explicit type hints that result in static typing. One reason to use such hints would be to achieve the performance benefits of static typing in performance-sensitive parts of code.

As of the 4.0 Release, the .NET Framework supports a variant of dynamic typing via the System.Dynamic namespace whereby a static object of type 'dynamic' is a placeholder for the .NET runtime to interrogate its dynamic facilities to resolve the object reference.

Static and dynamic type checking in practice[link]

The choice between static and dynamic typing requires trade-offs.

Static typing can find type errors reliably at compile time. This should increase the reliability of the delivered program. However, programmers disagree over how commonly type errors occur, and thus disagree over the proportion of those bugs that are coded that would be caught by appropriately representing the designed types in code. Static typing advocates believe programs are more reliable when they have been well type-checked, while dynamic typing advocates point to distributed code that has proven reliable and to small bug databases. The value of static typing, then, presumably increases as the strength of the type system is increased. Advocates of dependently typed languages such as Dependent ML and Epigram have suggested that almost all bugs can be considered type errors, if the types used in a program are properly declared by the programmer or correctly inferred by the compiler.^[5]

Static typing usually results in compiled code that executes more quickly. When the compiler knows the exact data types that are in use, it can produce optimized machine code. Further, compilers for statically typed languages can find assembler shortcuts more easily. Some dynamically typed languages such as Common Lisp allow optional type declarations for optimization for this very reason. Static typing makes this pervasive. See optimization.

By contrast, dynamic typing may allow compilers to run more quickly and allow interpreters to dynamically load new code, since changes to source code in dynamically typed languages may result in less checking to perform and less code to revisit. This too may reduce the edit-compile-test-debug cycle.

Statically typed languages that lack type inference (such as C and Java) require that programmers declare the types they intend a method or function to use. This can serve as additional documentation for the program, which the compiler will not permit the programmer to ignore or permit to drift out of synchronization. However, a language can be statically typed without requiring type declarations (examples include Haskell, Scala|Ocaml and to a lesser extent C#), so explicit type declaration is not a necessary requirement for static typing in all languages.

Dynamic typing allows constructs that some static type checking would reject as illegal. For example, eval functions, which execute arbitrary data as code, become possible. An eval function is possible with static typing, but requires advanced uses of algebraic data types. Furthermore, dynamic typing better accommodates transitional code and prototyping, such as allowing a placeholder data structure (mock object) to be transparently used in place of a full-fledged data structure (usually for the purposes of experimentation and testing).

Dynamic typing is used in duck typing that can support easier code reuse.

Dynamic typing typically makes metaprogramming more effective and easier to use. For example, C++ templates are typically more cumbersome to write than the equivalent Ruby or Python code. More advanced run-time constructs such as metaclasses and introspection are often more difficult to use in statically typed languages. In some languages, such features may also be used e.g. to generate new types and behaviors on the fly, based on run-time data. Such advanced constructs are often provided by dynamic programming languages; many of these are dynamically typed, although dynamic typing need not be related to dynamic programming languages.

Strong and weak typing: Liskov Definition[link]

In 1974 Liskov and Zilles described a strong-typed language as one in which "whenever an object is passed from a calling function to a called function, its type must be compatible with the type declared in the called function."^[6] Jackson wrote, "In a strongly typed language each data area will have a distinct type and each process will state its communication requirements in terms of these types."^[7]

Strong and weak typing[link]

A type system is said to feature strong typing when it specifies one or more restrictions on how operations involving values of different data types can be intermixed. A computer language that implements strong typing will prevent the successful execution of an operation on arguments that have the wrong type.

Weak typing means that a language implicitly converts (or casts) types when used. Consider the following example:

var x := 5;    // (1)  (x is an integer)
var y := "37"; // (2)  (y is a string)
x + y;         // (3)  (?)

In a weakly typed language, the result of this operation depends on language-specific rules. Visual Basic would convert the string "37" into the number 37, perform addition, and produce the number 42. JavaScript would convert the number 5 to the string "5," perform string concatenation, and produce the string "537." In JavaScript, the conversion to string is applied regardless of the order of the operands (for example, y + x would be "375") while in AppleScript, the left-most operand determines the type of the result, so that x + y is the number 42 but y + x is the string "375".

In the same manner, due to JavaScript's dynamic type conversions: <source lang=JavaScript> var y = 2 / 0; // y now equals a constant for infinity y == Number.POSITIVE_INFINITY // returns true Infinity == Number.POSITIVE_INFINITY // returns true "Infinity" == Infinity // returns true y == "Infinity" // returns true </source>

A C cast gone wrong exemplifies the problems that can occur if strong typing is absent: if a programmer casts a value from one type to another in C, not only must the compiler allow the code at compile time, but the runtime must allow it as well. This may permit more compact and faster C code, but it can make debugging more difficult.

Safely and unsafely typed systems[link]

A third way of categorizing the type system of a programming language uses the safety of typed operations and conversions. Computer scientists consider a language "type-safe", if it does not allow operations or conversions that lead to erroneous conditions.

Some observers use the term memory-safe language (or just safe language) to describe languages that do not allow undefined operations to occur. For example, a memory-safe language will check array bounds, or else statically guarantee (i.e., at compile time before execution) that array accesses out of the array boundaries will cause compile-time and perhaps runtime errors.

<source lang=VB> var x := 5; // (1) var y := "37"; // (2) var z := x + y; // (3) </source>

In languages like Visual Basic, variable Unknown extension tag "source" in the example acquires the value 42. While the programmer may or may not have intended this, the language defines the result specifically, and the program does not crash or assign an ill-defined value to Unknown extension tag "source". In this respect, such languages are type-safe; however, in some languages, if the value of Unknown extension tag "source" was a string that could not be converted to a number (e.g. "Hello World"), the results would be undefined. Such languages are type-safe (in that they will not crash), but can easily produce undesirable results. In other languages like JavaScript, the numeric operand would be converted to a string, and then concatenation performed. In this case, the results are not undefined and are predictable.

Now let us look at the same example in C:

<source lang=C> int x = 5; char y[] = "37"; char* z = x + y; </source>

In this example Unknown extension tag "source" will point to a memory address five characters beyond Unknown extension tag "source", equivalent to three characters after the terminating zero character of the string pointed to by Unknown extension tag "source". The content of that location is undefined, and might lie outside addressable memory. The mere computation of such a pointer may result in undefined behavior (including the program crashing) according to C standards, and in typical systems dereferencing z at this point could cause the program to crash. We have a well-typed, but not memory-safe program—a condition that cannot occur in a type-safe language.

In some languages, like JavaScript, the use of special numeric values and constants allows type-safety for mathematical operations without resulting in runtime errors. For example, when dividing a Unknown extension tag "source" by a Unknown extension tag "source", or a Unknown extension tag "source" by zero.

<source lang=JavaScript> var x = 32; var aString = new String("A"); x = x/aString; // x now equals the constant NaN, meaning Not A Number isNaN(x); // returns true typeof(x); // returns "number" var y = 2 / 0; // y now equals a constant for infinity y == Number.POSITIVE_INFINITY; // returns true typeof(y); // returns "number" </source>

Variable levels of type checking[link]

Some languages allow different levels of checking to apply to different regions of code. Examples include:-

• The use strict directive in Perl applies stronger checking.
• The @ operator in PHP suppresses some error messages.
• The Option Strict On in VB.NET allows the compiler to require a conversion between objects.

Additional tools such as lint and IBM Rational Purify can also be used to achieve a higher level of strictness.

Optional type systems[link]

It has been proposed, chiefly by Gilad Bracha, that the choice of type system be made independent of choice of language; that a type system should be a module that can be "plugged" into a language as required. He believes this is advantageous, because what he calls mandatory type systems make languages less expressive and code more fragile.^[8] The requirement that types do not affect the semantics of the language is difficult to fulfil: for instance, class based inheritance becomes impossible.

Polymorphism and types[link]

The term "polymorphism" refers to the ability of code (in particular, methods or classes) to act on values of multiple types, or to the ability of different instances of the same data structure to contain elements of different types. Type systems that allow polymorphism generally do so in order to improve the potential for code re-use: in a language with polymorphism, programmers need only implement a data structure such as a list or an associative array once, rather than once for each type of element with which they plan to use it. For this reason computer scientists sometimes call the use of certain forms of polymorphism generic programming. The type-theoretic foundations of polymorphism are closely related to those of abstraction, modularity and (in some cases) subtyping.

Duck typing[link]

In "duck typing",^[9] a statement calling a method m on an object does not rely on the declared type of the object; only that the object, of whatever type, must supply an implementation of the method called, when called, at run-time.

Duck typing differs from structural typing in that, if the part (of the whole module structure) needed for a given local computation is present at runtime, the duck type system is satisfied in its type identity analysis. On the other hand, a structural type system would require the analysis of the whole module structure at compile time to determine type identity or type dependence.

Duck typing differs from a nominative type system in a number of aspects. The most prominent ones are that for duck typing, type information is determined at runtime (as contrasted to compile time), and the name of the type is irrelevant to determine type identity or type dependence; only partial structure information is required for that for a given point in the program execution.

Duck typing uses the premise that (referring to a value) "if it walks like a duck, and quacks like a duck, then it is a duck" (this is a reference to the duck test that is attributed to James Whitcomb Riley). The term may have been coined^{[citation needed]} by Alex Martelli in a 2000 message^[10] to the comp.lang.python newsgroup (see Python).

Specialized type systems[link]

Many type systems have been created that are specialized for use in certain environments with certain types of data, or for out-of-band static program analysis. Frequently, these are based on ideas from formal type theory and are only available as part of prototype research systems.

Dependent types[link]

Dependent types are based on the idea of using scalars or values to more precisely describe the type of some other value. For example, Failed to parse (Missing texvc executable; please see math/README to configure.): matrix(3, 3)

might be the type of a 3×3 matrix. We can then define typing rules such as the following rule for matrix multiplication:

Failed to parse (Missing texvc executable; please see math/README to configure.): matrix_{multiply} : matrix(k, m) \times matrix(m, n) \to matrix(k, n)

where Failed to parse (Missing texvc executable; please see math/README to configure.): k , Failed to parse (Missing texvc executable; please see math/README to configure.): m , Failed to parse (Missing texvc executable; please see math/README to configure.): n

are arbitrary positive integer values. A variant of ML called Dependent ML has been created based on this type system, but because type checking for conventional dependent types is undecidable, not all programs using them can be type-checked without some kind of limits. Dependent ML limits the sort of equality it can decide to Presburger arithmetic. Other languages such as Epigram make the value of all expressions in the language decidable so that type checking can be decidable. It is also possible to make the language[vague] Turing-complete at the price of undecidable type checking, as in Cayenne.

Linear types[link]

Linear types, based on the theory of linear logic, and closely related to uniqueness types, are types assigned to values having the property that they have one and only one reference to them at all times. These are valuable for describing large immutable values such as files, strings, and so on, because any operation that simultaneously destroys a linear object and creates a similar object (such as 'str = str + "a"') can be optimized "under the hood" into an in-place mutation. Normally this is not possible, as such mutations could cause side effects on parts of the program holding other references to the object, violating referential transparency. They are also used in the prototype operating system Singularity for interprocess communication, statically ensuring that processes cannot share objects in shared memory in order to prevent race conditions. The Clean language (a Haskell-like language) uses this type system in order to gain a lot of speed^{[not specific enough to verify]} while remaining safe.

Intersection types[link]

Intersection types are types describing values that belong to both of two other given types with overlapping value sets. For example, in most implementations of C the signed char has range -128 to 127 and the unsigned char has range 0 to 255, so the intersection type of these two types would have range 0 to 127. Such an intersection type could be safely passed into functions expecting either signed or unsigned chars, because it is compatible with both types.

Intersection types are useful for describing overloaded function types: For example, if "Unknown extension tag "source" → Unknown extension tag "source"" is the type of functions taking an integer argument and returning an integer, and "Unknown extension tag "source" → Unknown extension tag "source"" is the type of functions taking a float argument and returning a float, then the intersection of these two types can be used to describe functions that do one or the other, based on what type of input they are given. Such a function could be passed into another function expecting an "Unknown extension tag "source" → Unknown extension tag "source"" function safely; it simply would not use the "Unknown extension tag "source" → Unknown extension tag "source"" functionality.

In a subclassing hierarchy, the intersection of a type and an ancestor type (such as its parent) is the most derived type. The intersection of sibling types is empty.

The Forsythe language includes a general implementation of intersection types. A restricted form is refinement types.

Union types[link]

Union types are types describing values that belong to either of two types. For example, in C, the signed char has range -128 to 127, and the unsigned char has range 0 to 255, so the union of these two types would have range -128 to 255. Any function handling this union type would have to deal with integers in this complete range. More generally, the only valid operations on a union type are operations that are valid on both types being unioned. C's "union" concept is similar to union types, but is not typesafe, as it permits operations that are valid on either type, rather than both. Union types are important in program analysis, where they are used to represent symbolic values whose exact nature (e.g., value or type) is not known.

In a subclassing hierarchy, the union of a type and an ancestor type (such as its parent) is the ancestor type. The union of sibling types is a subtype of their common ancestor (that is, all operations permitted on their common ancestor are permitted on the union type, but they may also have other valid operations in common).

Existential types[link]

Existential types are frequently used in connection with record types to represent modules and abstract data types, due to their ability to separate implementation from interface. For example, the type "T = ∃X { a: X; f: (X → int); }" describes a module interface that has a data member of type X and a function that takes a parameter of the same type X and returns an integer. This could be implemented in different ways; for example:

• intT = { a: int; f: (int → int); }
• floatT = { a: float; f: (float → int); }

These types are both subtypes of the more general existential type T and correspond to concrete implementation types, so any value of one of these types is a value of type T. Given a value "t" of type "T", we know that "t.f(t.a)" is well-typed, regardless of what the abstract type X is. This gives flexibility for choosing types suited to a particular implementation while clients that use only values of the interface type—the existential type—are isolated from these choices.

In general it's impossible for the typechecker to infer which existential type a given module belongs to. In the above example intT { a: int; f: (int → int); } could also have the type ∃X { a: X; f: (int → int); }. The simplest solution is to annotate every module with its intended type, e.g.:

• intT = { a: int; f: (int → int); } as ∃X { a: X; f: (X → int); }

Although abstract data types and modules had been implemented in programming languages for quite some time, it wasn't until 1988 that John C. Mitchell and Gordon Plotkin established the formal theory under the slogan: "Abstract [data] types have existential type".^[11] The theory is a second-order typed lambda calculus similar to System F, but with existential instead of universal quantification.

Explicit or implicit declaration and inference[link]

It has been suggested that Manifest typing be merged into this article or section. (Discuss) Proposed since August 2009.

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 Unknown extension tag "source" that adds Unknown extension tag "source" and Unknown extension tag "source" together, the compiler can infer that Unknown extension tag "source" and Unknown extension tag "source" must be numbers – since addition is only defined for numbers. Therefore, any call to Unknown extension tag "source" 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 Unknown extension tag "source" might imply a type of floating-point, while Unknown extension tag "source" 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.)

Types of types[link]

A type of types is a kind. Kinds appear explicitly in typeful programming, such as a type constructor in the Haskell language.

Types fall into several broad categories:

• Primitive types – the simplest kind of type; e.g., integer and floating-point number
  • Boolean
  • Integral types – types of whole numbers; e.g., integers and natural numbers
  • Floating point types – types of numbers in floating-point representation
• Reference types
• Option types
  • Nullable types
• Composite types – types composed of basic types; e.g., arrays or records.

  Abstract data types

• Algebraic types
• Subtype
• Derived type
• Object types; e.g., type variable
• Partial type
• Recursive type
• Function types; e.g., binary functions
• universally quantified types, such as parameterized types
• existentially quantified types, such as modules
• Refinement types – types that identify subsets of other types
• Dependent types – types that depend on terms (values)
• Ownership types – types that describe or constrain the structure of object-oriented systems
• Pre-defined types provided for convenience in real-world applications, such as date, time and money.

Unified Type System[link]

Some languages like C# have a unified type system. This means that all C# types including primitive types inherit from a single root object. Every type in C# inherits from the Object class. Java has several primitive types that are not objects. Java provides wrapper object types that exist together with the primitive types so developers can use either the wrapper object types or the simpler non-object primitive types.

Compatibility: equivalence and subtyping[link]

A type-checker for a statically typed language must verify that the type of any expression is consistent with the type expected by the context in which that expression appears. For instance, in an assignment statement of the form x := e, the inferred type of the expression e must be consistent with the declared or inferred type of the variable x. This notion of consistency, called compatibility, is specific to each programming language.

If the type of e and the type of x are the same and assignment is allowed for that type, then this is a valid expression. In the simplest type systems, therefore, the question of whether two types are compatible reduces to that of whether they are equal}} (or equivalent). Different languages, however, have different criteria for when two type expressions are understood to denote the same type. These different equational theories}} of types vary widely, two extreme cases being structural type systems, in which any two types are equivalent that describe values with the same structure, and nominative type systems, in which no two syntactically distinct type expressions denote the same type (i.e., types must have the same "name" in order to be equal).

In languages with subtyping, the compatibility relation is more complex. In particular, if A is a subtype of B, then a value of type A can be used in a context where one of type B is expected, even if the reverse is not true. Like equivalence, the subtype relation is defined differently for each programming language, with many variations possible. The presence of parametric or ad hoc polymorphism in a language may also have implications for type compatibility.

Programming style[link]

Some programmers prefer statically typed languages; others prefer dynamically typed languages. Statically typed languages alert programmers to type errors during compilation, and they may perform better at runtime. Advocates of dynamically typed languages claim they better support rapid prototyping and that type errors are only a small subset of errors in a program.^[12][13] Likewise, there is often no need to manually declare all types in statically typed languages with type inference; thus, the need for the programmer to explicitly specify types of variables is automatically lowered for such languages; and some dynamic languages have run-time optimisers^[14][15] that can generate fast code approaching the speed of static language compilers, often by using partial type inference.^{[citation needed]}

See also[link]

• Type rules
• Covariance and contravariance (computer science)
• Operator overloading
• Polymorphism in object-oriented programming
• Programming language
• Signedness
• Type system cross reference list
• Type signature
• Type theory

References[link]

Further reading[link]

The Wikibook Haskell has a page on the topic of Class Declarations

The Wikibook Ada Programming has a page on the topic of Types

• Smith, Chris, What To Know Before Debating Type Systems
• Tratt, Laurence, Dynamically Typed Languages, Advances in Computers, Vol. 77, pp. 149–184, July 2009

Peter Steele
Background information
Birth name	Peter Thomas Ratajczyk
Also known as	Peter Steele; Pete Steele; Lord Petrus Steele
Born	(1962-01-04)January 4, 1962
Origin	Brooklyn, New York, U.S.
Died	April 14, 2010(2010-04-14) (aged 48)
Genres	Gothic metal, doom metal, thrash metal
Occupations	Singer-songwriter, musician
Instruments	Vocals, bass, guitar, keyboards
Years active	1979–2010
Labels	Roadrunner, SPV America
Associated acts	Type O Negative, Carnivore, Fallout
Website	typeonegative.net

Peter Thomas Ratajczyk (January 4, 1962 – April 14, 2010),^[1] better known by his stage name Peter Steele, was the lead singer, bassist, and composer for the gothic metal band Type O Negative.^[2] Before forming Type O Negative, he had created the metal group Fallout and the thrash band Carnivore.^[3]

As the frontman for Type O Negative, Steele was known for his vampiric affect, towering stature,^[4] rich bass-baritone vocals,^{[2][5][6][7][8]} and a dark, often self-deprecating sense of humor.^[9][10] His lyrics were often intensely personal, dealing with subjects including love, loss, and addiction.^[9] Steele credited Black Sabbath and The Beatles as his key musical inspirations.^[2]

Early life[link]

Steele was born in Red Hook, Brooklyn to a Roman Catholic family^[11] of Polish, Danish, Icelandic and Russian (his grandparents lived in Russia) heritage and was raised in the Bensonhurst and Brighton Beach neighborhoods of Brooklyn.^[12] Steele was the youngest of six children, with five older sisters.^[7] His father fought in World War II^[11] and later worked at a shipyard.^[13] Steele started taking guitar lessons at age 12, moving on to bass six months later.^[7]

Steele worked for the New York City Department of Parks and Recreation up until he began touring with Type O Negative in the summer of 1994.^[11] He was based at Brooklyn Heights Promenade,^[14] where his job involved park maintenance,^[15] driving vehicles including garbage trucks and steamrollers,^[16] and eventual promotion to the role of Park Supervisor.^[11] Steele considered his days working for the Parks Department to be among his happiest.^[5]

Musical career[link]

Fallout and Carnivore (1979-1987)[link]

In 1979, Steele formed the heavy metal band Fallout. In 1982, after the split of Fallout, Steele formed the thrash metal band Carnivore. With Carnivore, Steele's lyrics were often harsh and politically incorrect, dealing with religion, war, race and misogyny. Carnivore released their debut self-titled album in 1985. In 1987 they released Retaliation, before splitting up later that same year.

Type O Negative[link]

Formation[link]

Steele formed the band in 1989 along with his childhood friends Josh Silver, Kenny Hickey and Sal Abruscato (later replaced by Johnny Kelly).^[9] The band originally used the name "Repulsion", but had to change name in 1990 due to legal issues with the German grindcore band of the same name. The band then used the name "Subzero".^[17] Steele had a tattoo of a minus sign contained within the number 0 that he originally intended to represent the Subzero band logo.^[17] After discovering that another band was already using the Subzero name, and with his tattoo in mind, Steele came up with the name "Type O Negative" after hearing a radio advertisement requesting donations of type O negative blood.^[17] When Type O Negative signed with Roadrunner Records, Steele signed his recording contract with a mixture of his blood and semen.^[18]

[edit] Slow, Deep and Hard and The Origin of the Feces (1991-1992)

Type O Negative's debut album, Slow, Deep and Hard, was released in 1991. The album incorporated the thrash elements of Carnivore merged with doom metal. Steele had written the music in the space of one night in the aftermath of a relationship break-up,^[19] and this was reflected in the lyrical topics of heartbreak, fantasies of revenge, and the contemplation of suicide; something Steele had himself attempted: “On October 15th, 1989. I slashed my wrists. All I can say is that I fell in love with the wrong person.”^[11]

Steele caused some controversy when touring in Europe to support Slow Deep and Hard, thanks to misunderstandings over his social and political views, with some critics going so far as to brand him a Nazi sympathizer,^[20][21] even though his bandmate, Josh Silver, is Jewish.^[5] Steele suggested that the European press had misunderstood his humor,^[19] and that his sarcasm was sometimes lost in translation to print.^[7]

In 1992, Type O Negative released the "live" album The Origin of the Feces. The album included a fictitious hostile audience and an evacuation of the venue after a bomb threat had supposedly been called in.^[21] This simulated some of the real-life response Steele and Type O Negative had recently received while on tour in Europe.^[21] The original album cover featured a close-up shot of Steele's anus.^[22]

[edit] Bloody Kisses, October Rust and World Coming Down (1993-2002)

In 1993, Type O Negative released their breakthrough album Bloody Kisses. The album focused primarily on romance, love, sex, and death. The song "Black No.1 (Little Miss Scare-All)" pays tribute to gothic subculture and is an ode to a goth girl Steele had once dated.^[19] Steele attacked his detractors with the songs "We Hate Everyone" and "Kill All the White People", which dealt directly with the band’s rumored racist ideology and served to erode any such accusations.^[21][23] Bloody Kisses eventually achieved Platinum status and established Type O Negative as one of gothic metal's most influential bands.^[8]

Type O Negative released the album October Rust in 1996. It featured a more multi-layered and melodic sound than its predecessor, though it retained similar lyrical themes. Steele penned the majority of the material on October Rust whilst on the road touring,^[24] though he had conceived some of the basic musical ideas during his early-teens.^[24] Steele designed the Vinland flag that first appeared on the October Rust artwork. It has since appeared on every subsequent release by the band. The flag encompassed a variety of Steele's interests, political beliefs and his heritage.^[25] Steele based the design on a Nordic cross flag that incorporates his favorite colors.^[25] The concept of Vinland is also referred to in the title of the track "The Glorious Liberation of the People's Technocratic Republic of Vinnland by the Combined Forces of the United Territories of Europa".^[25] "My Girlfriend's Girlfriend" is a tale about a ménage à trois^[26] that Steele based on a few true life experiences.^[7] The song "Green Man" had two meanings for Steele; it is written about the Celtic embodiment of nature, and Steele's time with the Parks Department, when young children used to call him "The Green Man".^{[citation needed]} The song introduction includes a sample of the garbage truck once driven by Steele.^[24] The song "Red Water (Christmas Mourning)" is about his father's death.^[14] October Rust eventually achieved Gold status.^[27]

Steele had been dealing with personal problems during the recording and mixing of 1999's stripped-down and heavier sounding World Coming Down.^[27] The themes of drug abuse and addiction appeared on the album, most notably on the song "White Slavery".^[28] Death also featured heavily on the album, with Steele mourning the loss of loved ones on the tracks "Everyone I Love is Dead" and "Everything Dies". Steele recounted his experience with psychiatric treatment on the song "Who Will Save the Sane?". On "Pyretta Blaze" Steele tells of his sexual fantasy involving fire.^[29] Steele noted the emotional strain caused by executing songs from World Coming Down in a live setting.^[2][13] The setlists for live shows performed since the initial tour to support World Coming Down usually featured very few selections from the album.

In 2000, Steele made a guest appearance on the song "Just Say No To Love" from Iommi, the first solo album by Black Sabbath guitarist Tony Iommi.^[30] In 2001, Steele made a guest appearance on the song "Cross the Line" from the Biohazard album Uncivilization.^[31] In 2002, he guest appeared on the track "Descent" from the Doro album Fight.^[32]

[edit] Life Is Killing Me and Dead Again (2003-2010)

Type O Negative released the album Life Is Killing Me in 2003. Lyrically the album dealt with issues including self pity, hatred, drugs, death and religion.^[27] On the title track Steele offers his criticism of the medical profession.^[5][33] The song “Nettie” centers around Steele's mother, while “Todd's Ship Gods (Above All Things)” is about his father.^[27] "The Dream is Dead" refers to Steele finding it difficult to celebrate Valentine's Day as the date coincided with the anniversary of his father's death.^[32] Steele wrote the song "(We Were) Electrocute" about a "stunning" ex-girlfriend, and how they would attract the interest of passers-by when out together as a couple.^[34] Steele's favorite female television characters are the inspiration for the track "How Could She?".^[27] "I Like Goils" makes light of the attention Steele received from gay men, specifically after his photoshoot for Playgirl magazine.^[34]

Steele performing in Berlin with Type O Negative, 2007

In 2005, Type O Negative left Roadrunner Records. Steele had never been happy with the conditions of the recording contract and had described it as "a millstone around my neck".^[29] Steele revealed that Type O Negative's split from Roadrunner Records, aside from a poor offer, had to do with an allegedly unauthorized release of a Best Of compilation.^[35] Steele remained on friendly terms with the staff at Roadrunner Records and in October 2005 he appeared on the Roadrunner United album to help celebrate the label's 25th anniversary.^[36]

There were unconfirmed rumors at one point of Steele's death after the band website posted an image of a tombstone bearing his name and the dates 1962-2005.^[37] According to an article dated May 14, 2005, Steele was not dead; the gag was related to their fresh signing with SPV Records. The website discontinued the tombstone picture in October 2005.

In 2006, Steele reactivated Carnivore with a new lineup that included longtime Type O Negative collaborator Paul Bento.^[38] The band played at the Wacken Open Air festival in 2006.^[39]

Steele made his final recording on the 2007 album Dead Again. He revealed on MTV's Headbangers Ball that the new alliance with SPV Records was probably his favorite thing about Dead Again from a production standpoint.^[40] Steele considered Dead Again to be less melancholic and more positive compared to the band's previous albums.^[41] The album cover depicts the Russian mystic Rasputin, a historical figure that Steele admired.^[5] The title track touches on drug abuse and Steele's sense of having killed part of himself after suffering a relapse.^[41] "Tripping a Blind Man" is a diatribe on how Steele felt after his involuntary commitment was brought about by his family.^[42] "Halloween in Heaven" is a song about dead rockstars that Steele was inspired to write by the death of his close friend Dimebag Darrell.^[41]

Further appearances[link]

[edit] Playgirl

Following the success of Bloody Kisses, Steele began to receive attention outside of music. He appeared as a nude centerfold of Playgirl in 1995.^[43] Steele later found out via bandmate Kenny Hickey's contacts that only 23% of the magazine subscribers were female,^[44] and after being asked by men to sign copies of the magazine, Steele somewhat regretted the decision: “After I did it, I thought, 'Oh my God, what did I do?'. It was more than upsetting that so many guys had it. Girls, OK, but there just seemed to be at least as many guys. Not that I'm homophobic, but it was certainly irritating.”^[29] In a 2007 interview, Steele reflected on the posing as merely a naïve publicity stunt.^[45]

Television and film[link]

Steele went on to appear as a guest on the talk shows Ricki Lake, The Jerry Springer Show, and The Howard Stern Show. In 2003, Steele had an acting role in the episode "Exeunt Omnes" of the HBO drama series Oz. Also in 2003 he appeared in the film Dirtbags (Armpit of Metal).^[46] He followed this with a role in the 2005 film Bad Acid.^[47] Steele is among the musicians featured in the 2011 documentary Living the American Nightmare.^[48]

Personal life[link]

Steele was widely known for standing 6'8" (203 cm) tall,^[4] giving him a famously menacing stage appearance. Despite this, Steele admitted to suffering from stage fright which he overcame by drinking alcohol before shows, and by drinking red wine when on stage.^[33][34]

Outside of music, Steele spent time lifting weights both at home and on his tour bus.^[7][18][49] Steele also enjoyed reading books on the subject of science^[7][18] and he had an interest in European culture.^[15][34] Steele liked working on his house^[7][13] and was interested in architecture and civil engineering.^[11][13] Steele also worked on his cars,^[7] including a heavily modified 1985 Pontiac Grand Prix he customized himself.^[50] Steele had a love for cats^[51] and kept several as pets.^[11][33]

Steele at an in-store signing in London, circa 1997

During 2005, Steele disappeared for an extended period with no explanation. Rumors of his death, terminal illness, and other speculations increased until the mystery was dispelled in an interview on the 2006 DVD Symphony for the Devil. In the interview Steele briefly mentions his incarceration in Rikers Island and "the psych ward at Kings County Hospital". Steele's family members had staged an intervention and insisted he check into a mental institution.^[4] Steele later confirmed he had been suffering from paranoia caused by his heavy substance abuse.^[4] Steele had been using cocaine since the age of 35, a decision he expressed great regret about.^[41][45] Steele then attended rehab for cocaine and alcohol addiction,^[45] and later served a 30-day prison term for assaulting a love rival.^[4][45] Steele made light of his incarceration by wearing a prison uniform on stage during live performances.

Steele stated in a 2003 interview that he was bipolar, and linked his mood swings to the types of songs he wrote.^[34] He also suffered from clinical depression for which he had received occasional psychiatric treatment.^[52][53][54] During a 2007 interview Steele explained:

“I’ve always been a very depressed person, but that’s only one side of me, you know. It makes me feel better when I can express my depression, my anger, my frustration through music...sonic therapy.”^[41]

In April 2007, Steele revealed that he began identifying himself as Roman Catholic in recent years, after decades of self-professed atheism.^[11] In an interview with Decibel magazine, Steele explained:

“There are no atheists in foxholes, they say, and I was a foxhole atheist for a long time. But after going through a midlife crisis and having many things change very quickly, it made me realize my mortality. And when you start to think about death, you start to think about what’s after it. And then you start hoping there is a God. For me, it’s a frightening thought to go nowhere. I also can’t believe that people like Stalin and Hitler are gonna go to the same place as Mother Teresa.”^[45]

Death[link]

Peter Steele died of heart failure on April 14, 2010 at the age of 48.^{[55][56][57][58]} Prior to his death, Steele had been enjoying a long period of sobriety and improved health and was imminently due to begin writing and recording new music.^[59] His wake was held at Byrnes Funeral Home in Gerritsen Beach, Brooklyn, and he is buried at Saint Charles Cemetery in Farmingdale, Long Island. On November 21, 2011, an oak tree was planted in Prospect Park to commemorate Steele.^[60]

References[link]

External links[link]

Wikiquote has a collection of quotations related to: Peter Steele

• Official Type O Negative web site
• Peter Steele at the Internet Movie Database
• Peter Steele at Allmusic
• Peter Steele at the Notable Names Database
• Peter Steele at Find a Grave