_(Programming language)s usually come with a type-system, a *(term) for some algebraic structure whose elements are the _(type)s of data that can be manipulated in the language, together with a mapping from the set of objects involved in defining the semantics of the language into the typesystem. 

<h2>_(Static) vs _(Dynamic) Typing</h2>

When the types are known in advance and decisions about them are made at compile-time, the typing is said to be _(static); when the types can be known only when code is executed at run-time, the typing is said to be _(dynamic). (Some people from the _(Scheme) community talk about "latent" vs "manifest" types rather than _(static) vs _(dynamic) types, but this vocabulary is not widely recognized.)

<h2>Strong vs Weak Typing</h2>

When the types detected or declared are strictly enforced by the language's semantics, the language is <em>strongly</em>-typed; when the semantics of the language allows for inconsistencies between the compile-time type and the run-time type, the language is <em>weakly</em>-typed. Sometimes, languages are weakly-typed at one level, but strongly-typed at another. Weak typing means that the invariants (program properties) expressible in the type system are (sometimes much) weaker.

<h2>Type Declaration vs Type Inference</h2>

Some typed language such as _(Pascal) or _(Java) require that types be explicitly declared for all functions and variables in a program. Other typed languages, such as _(ML) or _(Haskell), will infer the type of an expression depending on its structure and context, without the need for programmer declaration, except maybe in difficult or ambiguous cases.  This is also referred to as explicit vs implicit static typing.

<h2>Orthogonal vs Interdependent Typing</h2>

In some languages (notably _(CAML|ML), or _(Cecil)), the semantics and the typesystem can be given independently, the typesystem serving as a <em>restriction of the set of valid programs</em>, that allows eliminating bugs or enabling various compiler optimizations. The typesystem could then be called _(orthogonal) to the _(dynamic) semantics. In other languages (notably _(Lisp), the _(C|C language) or _(Java)), it is impossible to define the _(dynamic) semantics of the language without involving its typesystem; the typesystem could thus be called "interdependent" with the _(dynamic) semantics of the language. These terms are not very common, as far as I (_(Fare)) know.

<h2>Discussion</h2>

Strong type systems allow catching a lot of common programming mistakes (typos, thinkos, lack of propagation of program modifications) that usually require a lot of debugging time to catch. _(static) type systems particularly allow catching them quickly, as early as compile-time, without having to even worry about them. Type inference allows for such bug-catching to have no associated development costs, as long as the typesystem is powerful enough to express the considered program without the need for abuse or contortions.

Some argue that you can always determine _(static) or _(dynamic) information about a program, and call it is type. For them, the distinction is between trivial _(static) typing and rich _(static) typing, between trivial _(dynamic) typing and rich _(dynamic) typing. Trivial here means that the compiler (resp. the runtime system) cannot use _(static) (resp. _(dynamic)) information about an expressions' type so as to avoid checks and make early decisions about program behaviour, whereas rich means that it can.

Often, otherwise strongly typed languages have escapes allowing for weak typing (pointer/array dereference in the _(C|C language) or _(C++), typecasting in _(C|C language), _(C++) or _(Java); magic in _(OCAML)). Such languages can usually still be neatly divided into weakly typed and strongly typed. Indeed, in the case of _(C|C language) and _(C++), the weak typing features are essential to any reasonably sized project, and their implicit rather than explicit character prevents any easy syntactic distinction between programs that abuse or don't abuse the type-system; hence _(C|C language) and _(C++) are definitely weakly-typed languages. In the case of _(OCAML), such abuse is not an essential feature to normal user programs, and made explicit through the use of the keyword "magic" (or of special linking to routines written in _(C|C language) or other languages) that can be easily detected and avoided, - so _(OCAML) is definitely a strongly-typed language. In the case of _(Java), the "weaknesses" in the type-system are explicit typecasts (but a runtime check ensures that an object can only be cast to a superclass of its class, of which it is a member, and for which there can be no _(static) method discrepancy), and by the special <code>NULL</code> pointer (but the semantics again is well defined, although different for "_(static)" and other methods); _(Java) is thus strongly typed, although the invariants attached to its types may be less obvious and less nicely explained than in other strongly typed languages.

On a different note, otherwise _(static)ally typed languages sometimes have escapes that allow for _(dynamic) typing. For instance the _(CLOS MOP), or RTTI in _(C++), _(Java) or _(Mercury), allow programs to inspect and modify objects whose type is not _(static)ally known. This enables the development of some generic software infrastructure, but at the same time forces the implementation to keep at runtime information that might otherwise have been thrown away at compile-time (as it is in _(OCAML) for instance), with all the associated space and time overhead. _(dynamic)ally typed languages have this overhead, anyway.

Inferred _(Static) Strong Types, such as exist in _(ML), _(Haskell), _(Clean) or _(Mercury), are those that bring the most information on programs out of the least programmer efforts, allowing to express the stronger and richer invariants. Because they do not usually require any type declaration, they remove the burden that people used to _(dynamic) programming languages usually feel about rich typing. However, because of language design and implementation issues (notably the simplicity of the typesystem and the guarantee that the process of typing will terminate promptly), most languages with strong _(static) inferred types also restrict the expressiveness of their typesystem in such ways that advanced users of _(dynamic)ally typed language will find them impossible to use (notably those who like _(dynamic) interactive systems and/or _(Lisp) _(macro)s). A notable exception, _(Cayenne), is an extension _(Haskell) with dependent types (types that depend on values), that allows to express arbitrary computations within the type system at compile-time; unhappily, it is more designed as a proof of concept than as a really usable programming language.

Compilers for languages without a rich _(static) type system can nevertheless infer types from programs that follow common programming styles, and use these types to produce more efficient code, or emit warnings that help catch bugs. A case in point is CMUCL (a _(Common Lisp) compiler). _(Common Lisp), a strongly _(dynamic)ally typed language, allows the programmer to declare _(static) types for expressions, so as to help the compiler. CMUCL takes advantage of these declarations as well as of information it can infer from the language's semantics so as to construct precise types for expressions and produce efficient code that avoids runtime type dispatch. The situation of CMUCL is rather peculiar, since, depending on its the programmer-accessible safety settings, the declarations can be used either to tighten the type-safety of the language, or on the contrary to make it weakly-typed and provide an escape for low-level optimizations. Because this escape requires explicit and easily toggled safety settings, and is not essential to normal programs, CMUCL, like _(Common Lisp) in general, is still a strongly _(dynamic)ally typed language.

<ul class="links">
<li>_(Type Systems| http://citeseer.nj.nec.com/cardelli97type.html) by _(Luca Cardelli), covering a lot of the issues very precisely.
<li>_(Types and Programming Languages: The Next Generation| http://www.cis.upenn.edu/~bcpierce/papers/tng-lics2003-slides.pdf), a talk by _(Benjamin J. Pierce) on the progress from 1993 to 2003 on _(type system)s and programming languages.
</ul>