Type checking is a process that verifies if a variable is compatible with a certain operation. Depending on when it happens, there are two paradigms:<ul><li class="ql-align-justify">Static typing → which happens at compile-time and doesn't allow a variable to be reassigned values of different types because types are bound to variables. (Java, Go, C++, Typescript)</li><li class="ql-align-justify">Dynamic typing → which happens at runtime and allows for variables to be reassigned values of different types because types are bound to values. (Python, Javascript, PHP, Perl)</li></ul>

When type checking happens

Depending on how the type checking is done, we have two paradigms:<ul><li class="ql-align-justify">Nominal typing → which determines compatibility based on a variable's type. (Java, C++, PHP, Perl)</li><li class="ql-align-justify">Structural typing / Duck typing → which determines compatibility based on the set of attributes and methods of a variable. (Python, Go, Javascript, Typescript)</li></ul>

How type checking is done

Type coercion is the implicit type conversion from one data type to another. Depending on whether the language does it, we have two paradigms:<ul><li class="ql-align-justify">Weak typing → where the language does type coercion (Javascript, PHP, C)</li><li class="ql-align-justify">Strong typing → where the language doesn't do type coercion and we must explicitly convert values from one data type to another. (Java, Go)</li></ul>

If type coercion is done

Typing paradigms in programming languages

computerscience

Computer Science

In <a href="https://en.wikipedia.org/wiki/Computer_programming">computer programming </a>, a type system is a <a href="https://en.wikipedia.org/wiki/Logical_system">logical system </a>comprising a set of rules that assigns a property called a <a href="https://en.wikipedia.org/wiki/Type_(computer_science)">type </a>(for example, <a href="https://en.wikipedia.org/wiki/Integer">integer </a>, <a href="https://en.wikipedia.org/wiki/Floating_point">floating point </a>, <a href="https://en.wikipedia.org/wiki/String_(computer_science)">string </a>) to every <a href="https://en.wikipedia.org/wiki/Term_(programming)">term </a> (a word, phrase, or other set of symbols). Usually the terms are various <a href="https://en.wikipedia.org/wiki/Language_construct">language constructs </a>of a <a href="https://en.wikipedia.org/wiki/Computer_program">computer program </a>, such as <a href="https://en.wikipedia.org/wiki/Variable_(computer_science)">variables </a>, <a href="https://en.wikipedia.org/wiki/Expression_(computer_science)">expressions </a>, <a href="https://en.wikipedia.org/wiki/Function_(computer_science)">functions </a>, or <a href="https://en.wikipedia.org/wiki/Modular_programming">modules </a>.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-FOOTNOTEPierce20021-1">[ 1] </a> A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.

Type systems formalize and enforce the otherwise implicit categories the programmer uses for <a href="https://en.wikipedia.org/wiki/Algebraic_data_type">algebraic data types </a>, <a href="https://en.wikipedia.org/wiki/Data_structure">data structures </a>, or other <a href="https://en.wikipedia.org/wiki/Data_type">data types </a>, such as "string", "array of float", "function returning boolean".

Type systems are often specified as part of <a href="https://en.wikipedia.org/wiki/Programming_language">programming languages </a>and built into <a href="https://en.wikipedia.org/wiki/Interpreter_(computing)">interpreters </a>and <a href="https://en.wikipedia.org/wiki/Compiler">compilers </a>, although the type system of a language can be extended by <a href="https://en.wikipedia.org/wiki/Extended_static_checking">optional tools </a>that perform added checks using the language's original type <a href="https://en.wikipedia.org/wiki/Syntax_(programming_languages)">syntax </a>and <a href="https://en.wikipedia.org/wiki/Formal_grammar">grammar </a>.

The main purpose of a type system in a programming language is to reduce possibilities for <a href="https://en.wikipedia.org/wiki/Bug_(computer_programming)">bugs </a>in computer programs due to <a href="https://en.wikipedia.org/wiki/Type_error">type errors </a>.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-FOOTNOTECardelli20041-2">[ 2] </a> The given type system in question determines what constitutes a type error, but in general, the aim is to prevent operations expecting a certain kind of value from being used with values of which that operation does not make sense (validity errors).

Type systems allow defining <a href="https://en.wikipedia.org/wiki/Interface_(computer_science)">interfaces </a>between different parts of a computer program, and then checking that the parts have been connected in a consistent way. This checking can happen statically (at <a href="https://en.wikipedia.org/wiki/Compile_time">compile time </a>), dynamically (at <a href="https://en.wikipedia.org/wiki/Run_time_(program_lifecycle_phase)">run time </a>), or as a combination of both.

Type systems have other purposes as well, such as expressing business rules, enabling certain <a href="https://en.wikipedia.org/wiki/Compiler_optimization">compiler optimizations </a>, allowing for <a href="https://en.wikipedia.org/wiki/Multiple_dispatch">multiple dispatch </a>, and providing a form of <a href="https://en.wikipedia.org/wiki/Software_documentation">documentation </a>.

An example of a simple type system is that of the <a href="https://en.wikipedia.org/wiki/C_(programming_language)">C language </a>. The portions of a C program are the <a href="https://en.wikipedia.org/wiki/Subroutine">function </a>definitions. One function is invoked by another function.

The <a href="https://en.wikipedia.org/wiki/Interface_(computing)">interface </a>of a function states the name of the function and a list of <a href="https://en.wikipedia.org/wiki/Parameter_(computer_programming)">parameters </a>that are passed to the function's code. The code of an invoking function states the name of the invoked, along with the names of <a href="https://en.wikipedia.org/wiki/Variable_(computer_science)">variables </a>that hold values to pass to it.

During a <a href="https://en.wikipedia.org/wiki/Computer_program">computer program </a>'s execution, the values are placed into temporary storage, then execution jumps to the code of the invoked function. The invoked function's code accesses the values and makes use of them.

If the instructions inside the function are written with the assumption of receiving an <a href="https://en.wikipedia.org/wiki/Integer_(computer_science)">integer </a>value, but the calling code passed a <a href="https://en.wikipedia.org/wiki/Floating-point_arithmetic">floating-point value </a>, then the wrong result will be computed by the invoked function.

The C compiler checks the types of the arguments passed to a function when it is called against the types of the parameters declared in the function's definition. If the types do not match, the compiler throws a compile-time error or warning.

A <a href="https://en.wikipedia.org/wiki/Compiler">compiler </a>may also use the static type of a value to optimize the storage it needs and the choice of <a href="https://en.wikipedia.org/wiki/Algorithm">algorithms </a>for operations on the value. In many <a href="https://en.wikipedia.org/wiki/C_(programming_language)">C </a>compilers the float <a href="https://en.wikipedia.org/wiki/Data_type">data type </a>, for example, is represented in 32 <a href="https://en.wikipedia.org/wiki/Bit">bits </a>, in accord with the <a href="https://en.wikipedia.org/wiki/IEEE_754-2008_revision">IEEE specification for single-precision floating point numbers </a>. They will thus use floating-point-specific <a href="https://en.wikipedia.org/wiki/Instruction_set">microprocessor operations </a>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 <a href="https://en.wikipedia.org/wiki/Programming_language">programming language </a>may further associate an operation with various resolutions for each type, in the case of type <a href="https://en.wikipedia.org/wiki/Polymorphism_(computer_science)">polymorphism </a>. <a href="https://en.wikipedia.org/wiki/Type_theory">Type theory </a>is the study of type systems. The concrete types of some programming languages, such as integers and strings, depend on practical issues of <a href="https://en.wikipedia.org/wiki/Computer_architecture">computer architecture </a>, compiler implementation, and <a href="https://en.wikipedia.org/wiki/Programming_language_design_and_implementation">language design </a>.

Formally, <a href="https://en.wikipedia.org/wiki/Type_theory">type theory </a>studies type systems. A programming language must have the opportunity to type check using the type system whether at compile time or runtime, manually annotated or automatically inferred. As Mark Manasse concisely put it:<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-FOOTNOTEPierce2002208-3">[ 3] </a>

The fundamental problem addressed by a type theory is to ensure 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.

Assigning a data type, termed typing , gives meaning to a sequence of <a href="https://en.wikipedia.org/wiki/Bit">bits </a>such as a value in <a href="https://en.wikipedia.org/wiki/Computer_memory">memory </a>or some <a href="https://en.wikipedia.org/wiki/Object_(computer_science)">object </a>such as a <a href="https://en.wikipedia.org/wiki/Variable_(computer_science)">variable </a>. The <a href="https://en.wikipedia.org/wiki/Computer_hardware">hardware </a>of a <a href="https://en.wikipedia.org/wiki/General_purpose_computer">general purpose computer </a>is unable to discriminate between for example a <a href="https://en.wikipedia.org/wiki/Memory_address">memory address </a>and an <a href="https://en.wikipedia.org/wiki/Instruction_code_(programming)">instruction code </a>, or between a <a href="https://en.wikipedia.org/wiki/Character_(computing)">character </a>, an <a href="https://en.wikipedia.org/wiki/Integer">integer </a>, or a <a href="https://en.wikipedia.org/wiki/Floating-point_number">floating-point number </a>, because it makes no intrinsic distinction between any of the possible values that a sequence of bits might mean .<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-Burroughs-4">[ note 1] </a> Associating a sequence of bits with a type conveys that <a href="https://en.wiktionary.org/wiki/meaning">meaning </a>to the programmable hardware to form a <a href="https://en.wikipedia.org/wiki/Symbolic_system">symbolic system </a> composed of that hardware and some program.

A program associates each value with at least one specific type, but it also can occur that one value is associated with many <a href="https://en.wikipedia.org/wiki/Subtyping">subtypes </a>. Other entities, such as <a href="https://en.wikipedia.org/wiki/Object_(computer_science)">objects </a>, <a href="https://en.wikipedia.org/wiki/Module_(programming)">modules </a>, <a href="https://en.wikipedia.org/wiki/Communication_channel">communication channels </a>, and <a href="https://en.wikipedia.org/wiki/Dependency_(computer_science)">dependencies </a>can become associated with a type. Even a type can become associated with a type. An implementation of a type system could in theory associate identifications called <a href="https://en.wikipedia.org/wiki/Data_type">data type </a> (a type of a value), <a href="https://en.wikipedia.org/wiki/Class_(computer_science)">class </a> (a type of an object), and <a href="https://en.wikipedia.org/wiki/Kind_(type_theory)">kind </a> (a type of a type , or metatype). These are the abstractions that typing can go through, on a hierarchy of levels contained in a system.

When a programming language evolves a more elaborate type system, it gains a more finely grained rule set than basic type checking, but this comes at a price when the type <a href="https://en.wikipedia.org/wiki/Inference">inferences </a>(and other properties) become <a href="https://en.wikipedia.org/wiki/Undecidable_problem">undecidable </a>, and when more attention must be paid by the programmer to annotate code or to consider computer-related operations and functioning. It is challenging to find a sufficiently expressive type system that satisfies all programming practices in a <a href="https://en.wikipedia.org/wiki/Type_safe">type safe </a>manner.

A programming language compiler can also implement a <a href="https://en.wikipedia.org/wiki/Dependent_type">dependent type </a> or an <a href="https://en.wikipedia.org/wiki/Effect_system">effect system </a> , which enables even more program specifications to be verified by a type checker. Beyond simple value-type pairs, a virtual "region" of code is associated with an "effect" component describing what is being done with what , and enabling for example to "throw" an error report. Thus the symbolic system may be a type and effect system , which endows it with more safety checking than type checking alone.

Whether automated by the compiler or specified by a programmer, a type system renders program behavior illegal if it falls outside the type-system rules. Advantages provided by programmer-specified type systems include:

<ul><li>Abstraction (or modularity ) – Types enable programmers to think at a higher level than the bit or byte, not bothering with <a href="https://en.wikipedia.org/wiki/Low-level_programming_language">low-level </a>implementation. For example, programmers can begin to think of a string as a set of character values instead of as a mere <a href="https://en.wikipedia.org/wiki/Array_(data_structure)">array </a>of bytes. Higher still, types enable programmers to think about and express <a href="https://en.wikipedia.org/wiki/Interface_(computer_science)">interfaces </a>between two of any -sized subsystems. This enables more levels of localization so that the definitions required for <a href="https://en.wikipedia.org/wiki/Interoperability">interoperability </a>of the subsystems remain consistent when those two subsystems communicate. </li><li>Documentation – In more expressive type systems, types can serve as a form of <a href="https://en.wikipedia.org/wiki/Documentation">documentation </a>clarifying the intent of the programmer. For example, if a programmer declares a function as returning a timestamp type, this documents the function when the timestamp type can be explicitly declared deeper in the code to be an integer type. </li> </ul>

Advantages provided by compiler-specified type systems include:

<ul><li>Optimization – Static type-checking may provide useful <a href="https://en.wikipedia.org/wiki/Compile_time">compile-time </a>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. </li><li>Safety – A type system enables the <a href="https://en.wikipedia.org/wiki/Compiler">compiler </a>to detect meaningless or invalid code. For example, we can identify an expression <code>3 / "Hello, World" </code>as invalid, when the rules do not specify how to divide an <a href="https://en.wikipedia.org/wiki/Integer">integer </a>by a <a href="https://en.wikipedia.org/wiki/String_(computer_science)">string </a>. Strong typing offers more safety, but cannot guarantee complete <a href="https://en.wikipedia.org/wiki/Type_safety">type safety </a> . </li> </ul>

A type error occurs when an operation receives a different type of data than it expected.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-Sethi1997-5">[ 4] </a> For example, a type error would happen if a line of code divides two integers, and is passed a string of letters instead of an integer.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-Sethi1997-5">[ 4] </a> It is an unintended condition<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-leakyCondition-8">[ note 2] </a> which might manifest in multiple stages of a program's development. Thus a facility for detection of the error is needed in the type system. In some languages, such as <a href="https://en.wikipedia.org/wiki/Haskell">Haskell </a>, for which <a href="https://en.wikipedia.org/wiki/Type_inference">type inference </a>is automated, <a href="https://en.wikipedia.org/wiki/Lint_(software)">lint </a>might be available to its compiler to aid in the detection of error.

Type safety contributes to <a href="https://en.wikipedia.org/wiki/Program_correctness">program correctness </a>, but might only guarantee correctness at the cost of making the type checking itself an <a href="https://en.wikipedia.org/wiki/Undecidable_problem">undecidable problem </a>(as in the <a href="https://en.wikipedia.org/wiki/Halting_problem">Halting problem </a>). In a type system with automated type checking, a program may prove to run incorrectly yet produce no compiler errors. <a href="https://en.wikipedia.org/wiki/Division_by_zero">Division by zero </a>is an unsafe and incorrect operation, but a type checker which only runs at <a href="https://en.wikipedia.org/wiki/Compile_time">compile time </a>does not scan for division by zero in most languages; that division would surface as a <a href="https://en.wikipedia.org/wiki/Runtime_error">runtime error </a>. To prove the absence of these defects, other kinds of <a href="https://en.wikipedia.org/wiki/Formal_method">formal methods </a>, collectively known as <a href="https://en.wikipedia.org/wiki/Program_analysis_(computer_science)">program analyses </a>, are in common use. Alternatively, a sufficiently expressive type system, such as in dependently typed languages, can prevent these kinds of errors (for example, expressing the type of non-zero numbers ). In addition, <a href="https://en.wikipedia.org/wiki/Software_testing">software testing </a>is an <a href="https://en.wikipedia.org/wiki/Empirical">empirical </a>method for finding errors that such a type checker would not detect.

The process of verifying and enforcing the constraints of types—type checking —may occur at <a href="https://en.wikipedia.org/wiki/Compile_time">compile time </a>(a static check) or at <a href="https://en.wikipedia.org/wiki/Runtime_(program_lifecycle_phase)">run-time </a>(a dynamic check).

If a language specification requires its typing rules strongly, more or less allowing only those automatic <a href="https://en.wikipedia.org/wiki/Type_conversion">type conversions </a>that do not lose information, one can refer to the process as strongly typed; i f not, as weakly typed .

The terms are not usually used in a strict sense.

Static type checking is the process of verifying the <a href="https://en.wikipedia.org/wiki/Type_safety">type safety </a>of a program based on analysis of a program's text (<a href="https://en.wikipedia.org/wiki/Source_code">source code </a>). If a program passes a static type checker, then the program is guaranteed to satisfy some set of type safety properties for all possible inputs.

Static type checking can be considered a limited form of <a href="https://en.wikipedia.org/wiki/Program_verification">program verification </a>(see <a href="https://en.wikipedia.org/wiki/Type_safety">type safety </a>), and in a type-safe language, can also be considered an optimization. If a compiler can prove that a program is well-typed, then it does not need to emit dynamic safety checks, allowing the resulting compiled binary to run faster and to be smaller.

Static type checking for <a href="https://en.wikipedia.org/wiki/Turing_completeness">Turing-complete </a>languages is inherently conservative. That is, if a type system is both sound (meaning that it rejects all incorrect programs) and decidable (meaning that it is possible to write an algorithm that determines whether a program is well-typed), then it must be incomplete (meaning there are correct programs, which are also rejected, even though they do not encounter runtime errors).<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-9">[ 7] </a> For example, consider a program containing the code:

Even if the expression <code><complex test> </code>always evaluates to <code>true </code>at run-time, most type checkers will reject the program as ill-typed, because it is difficult (if not impossible) for a static analyzer to determine that the <code>else </code>branch will not be taken.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-FOOTNOTEPierce2002-10">[ 8] </a> Consequently, a static type checker will quickly detect type errors in rarely used code paths. Without static type checking, even <a href="https://en.wikipedia.org/wiki/Code_coverage">code coverage </a>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.

A number of useful and common programming language features cannot be checked statically, such as <a href="https://en.wikipedia.org/wiki/Downcasting">downcasting </a>. Thus, many languages will have both static and dynamic type checking; the static type checker verifies what it can, and dynamic checks verify the rest.

Many languages with static type checking provide a way to bypass the type checker. Some languages allow programmers to choose between static and dynamic type safety. For example, historically C# declares variables statically,<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-Skeet-11">[ 9] </a> : 77, Section 3.2 but <a href="https://en.wikipedia.org/wiki/C_Sharp_4.0">C# 4.0 </a>introduces the <code>dynamic </code>keyword, which is used to declare variables to be checked dynamically at runtime.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-Skeet-11">[ 9] </a> : 117, Section 4.1 Other languages allow writing code that is not type-safe; for example, in <a href="https://en.wikipedia.org/wiki/C_(programming_language)">C </a>, programmers can freely cast a value between any two types that have the same size, effectively subverting the type concept.

For a list of languages with static type checking, see <a href="https://en.wikipedia.org/wiki/Category:Statically_typed_programming_languages">the category for statically typed languages </a>.

Dynamic type checking and runtime type information

Dynamic type checking is the process of verifying the type safety of a program at runtime. Implementations of dynamically type-checked languages generally associate each runtime object with a type tag (i.e., a reference to a type) containing its type information. This runtime type information (RTTI) can also be used to implement <a href="https://en.wikipedia.org/wiki/Dynamic_dispatch">dynamic dispatch </a>, <a href="https://en.wikipedia.org/wiki/Late_binding">late binding </a>, <a href="https://en.wikipedia.org/wiki/Downcasting">downcasting </a>, <a href="https://en.wikipedia.org/wiki/Reflective_programming">reflective programming </a>(reflection), and similar features.

Most type-safe languages include some form of dynamic type checking, even if they also have a static type checker.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-12">[ 10] </a> The reason for this is that many useful features or properties are difficult or impossible to verify statically. For example, suppose that a program defines two types, A and B, where B is a subtype of A. If the program tries to convert a value of type A to type B, which is known as <a href="https://en.wikipedia.org/wiki/Downcasting">downcasting </a>, then the operation is legal only if the value being converted is actually a value of type B. Thus, a dynamic check is needed to verify that the operation is safe. This requirement is one of the criticisms of downcasting.

By definition, dynamic type checking may cause a program to fail at runtime. In some programming languages, it is possible to anticipate and recover from these failures. In others, type-checking errors are considered fatal.

Programming languages that include dynamic type checking but not static type checking are often called "dynamically typed programming languages". For a list of such languages, see <a href="https://en.wikipedia.org/wiki/Category:Dynamically_typed_programming_languages">the category for dynamically typed programming languages </a>.

Combining static and dynamic type checking

Some languages allow both static and dynamic typing. For example, Java and some other ostensibly statically typed languages support <a href="https://en.wikipedia.org/wiki/Downcasting">downcasting </a>types to their <a href="https://en.wikipedia.org/wiki/Subtypes">subtypes </a>, querying an object to discover its dynamic type and other type operations that depend on runtime type information. Another example is <a href="https://en.wikipedia.org/wiki/Run-time_type_information">C++ RTTI </a>. More generally, most programming languages include mechanisms for dispatching over different 'kinds' of data, such as <a href="https://en.wikipedia.org/wiki/Disjoint_union">disjoint unions </a>, <a href="https://en.wikipedia.org/wiki/Dynamic_dispatch">runtime polymorphism </a>, and <a href="https://en.wikipedia.org/wiki/Variant_type">variant types </a>. Even when not interacting with type annotations or type checking, such mechanisms are materially similar to dynamic typing implementations. See <a href="https://en.wikipedia.org/wiki/Programming_language">programming language </a>for more discussion of the interactions between static and dynamic typing.

Objects in object-oriented languages are usually accessed by a reference whose static target type (or manifest type) is equal to either the object's run-time type (its latent type) or a supertype thereof. This is conformant with the <a href="https://en.wikipedia.org/wiki/Liskov_substitution_principle">Liskov substitution principle </a>, which states that all operations performed on an instance of a given type can also be performed on an instance of a subtype. This concept is also known as subsumption or <a href="https://en.wikipedia.org/wiki/Subtyping">subtype polymorphism </a>. In some languages subtypes may also possess <a href="https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)">covariant or contravariant </a>return types and argument types respectively.

Certain languages, for example <a href="https://en.wikipedia.org/wiki/Clojure">Clojure </a>, <a href="https://en.wikipedia.org/wiki/Common_Lisp">Common Lisp </a>, or <a href="https://en.wikipedia.org/wiki/Cython">Cython </a>are dynamically type checked by default, but allow programs to opt into static type checking by providing optional annotations. One reason to use such hints would be to optimize the performance of critical sections of a program. This is formalized by <a href="https://en.wikipedia.org/wiki/Type_system#Gradual_typing">gradual typing </a>. The programming environment <a href="https://en.wikipedia.org/wiki/DrRacket">DrRacket </a> , a pedagogic environment based on Lisp, and a precursor of the language <a href="https://en.wikipedia.org/wiki/Racket_(programming_language)#Development">Racket </a>is also soft-typed.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-13">[ 11] </a>

Conversely, as of version 4.0, the C# language provides a way to indicate that a variable should not be statically type checked. A variable whose type is <code>dynamic </code>will not be subject to static type checking. Instead, the program relies on runtime type information to determine how the variable may be used.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-14">[ 12] </a> <a href="https://en.wikipedia.org/wiki/Type_system#cite_note-Skeet-11">[ 9] </a> : 113–119

In <a href="https://en.wikipedia.org/wiki/Rust_(programming_language)">Rust </a>, the <code>dyn std ::any ::Any </code>type provides dynamic typing of <code>' static </code>types.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-15">[ 13] </a>

Static and dynamic type checking in practice

The choice between static and dynamic typing requires certain <a href="https://en.wikipedia.org/wiki/Trade-off">trade-offs </a>.

Static typing can find type errors reliably at compile time, which increases the reliability of the delivered program. However, programmers disagree over how commonly type errors occur, resulting in further disagreements over the proportion of those bugs that are coded that would be caught by appropriately representing the designed types in code.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-16">[ 14] </a> <a href="https://en.wikipedia.org/wiki/Type_system#cite_note-17">[ 15] </a> Static typing advocates[<a href="https://en.wikipedia.org/wiki/Wikipedia:Manual_of_Style/Words_to_watch#Unsupported_attributions">who? </a> ] believe programs are more reliable when they have been well type-checked, whereas dynamic-typing advocates[<a href="https://en.wikipedia.org/wiki/Wikipedia:Manual_of_Style/Words_to_watch#Unsupported_attributions">who? </a> ] point to distributed code that has proven reliable and to small bug databases.[<a href="https://en.wikipedia.org/wiki/Wikipedia:Citation_needed">citation needed </a> ] The value of static typing increases as the strength of the type system is increased. Advocates of <a href="https://en.wikipedia.org/wiki/Dependent_type">dependent typing </a>,[<a href="https://en.wikipedia.org/wiki/Wikipedia:Manual_of_Style/Words_to_watch#Unsupported_attributions">who? </a> ] implemented in languages such as <a href="https://en.wikipedia.org/wiki/Dependent_ML">Dependent ML </a>and <a href="https://en.wikipedia.org/wiki/Epigram_(programming_language)">Epigram </a>, 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.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-18">[ 16] </a>

Static typing usually results in compiled code that executes faster. When the compiler knows the exact data types that are in use (which is necessary for static verification, either through declaration or inference) it can produce optimized machine code. Some dynamically typed languages such as <a href="https://en.wikipedia.org/wiki/Common_Lisp">Common Lisp </a>allow optional type declarations for optimization for this reason.

By contrast, dynamic typing may allow compilers to run faster and <a href="https://en.wikipedia.org/wiki/Interpreter_(computing)">interpreters </a>to dynamically load new code, because changes to source code in dynamically typed languages may result in less checking to perform and less code to revisit.[<a href="https://en.wikipedia.org/wiki/Wikipedia:Please_clarify">clarification needed </a> ] This too may reduce the edit-compile-test-debug cycle.

Statically typed languages that lack <a href="https://en.wikipedia.org/wiki/Type_inference">type inference </a>(such as <a href="https://en.wikipedia.org/wiki/C_(programming_language)">C </a>and <a href="https://en.wikipedia.org/wiki/Java_(programming_language)">Java </a>prior to <a href="https://en.wikipedia.org/wiki/Java_version_history#Java_SE_10">version 10 </a>) require that programmers declare the types that a method or function must use. This can serve as added program documentation, that is active and dynamic, instead of static. This allows a compiler to prevent it from drifting out of synchrony, and from being ignored by programmers. However, a language can be statically typed without requiring type declarations (examples include <a href="https://en.wikipedia.org/wiki/Haskell_(programming_language)">Haskell </a>, <a href="https://en.wikipedia.org/wiki/Scala_(programming_language)">Scala </a>, <a href="https://en.wikipedia.org/wiki/OCaml">OCaml </a>, <a href="https://en.wikipedia.org/wiki/F_Sharp_(programming_language)">F# </a>, <a href="https://en.wikipedia.org/wiki/Swift_(programming_language)">Swift </a>, and to a lesser extent <a href="https://en.wikipedia.org/wiki/C_Sharp_(programming_language)">C# </a>and <a href="https://en.wikipedia.org/wiki/C%2B%2B">C++ </a>), so explicit type declaration is not a necessary requirement for static typing in all languages.

Dynamic typing allows constructs that some (simple) static type checking would reject as illegal. For example, <a href="https://en.wikipedia.org/wiki/Eval">eval </a> functions, which execute arbitrary data as code, become possible. An eval function is possible with static typing, but requires advanced uses of <a href="https://en.wikipedia.org/wiki/GADT">algebraic data types </a>. Further, dynamic typing better accommodates transitional code and prototyping, such as allowing a placeholder data structure (<a href="https://en.wikipedia.org/wiki/Mock_object">mock object </a>) to be transparently used in place of a full data structure (usually for the purposes of experimentation and testing).

Dynamic typing typically allows <a href="https://en.wikipedia.org/wiki/Duck_typing">duck typing </a>(which enables <a href="https://en.wikipedia.org/wiki/Duck_typing#Comparison_with_other_type_systems">easier code reuse </a>). Many[<a href="https://en.wikipedia.org/wiki/Wikipedia:Citing_sources">specify </a> ] languages with static typing also feature <a href="https://en.wikipedia.org/wiki/Duck_typing#In_statically_typed_languages">duck typing </a>or other mechanisms like <a href="https://en.wikipedia.org/wiki/Generic_programming">generic programming </a>that also enable easier code reuse.

Dynamic typing typically makes <a href="https://en.wikipedia.org/wiki/Metaprogramming">metaprogramming </a>easier to use. For example, <a href="https://en.wikipedia.org/wiki/Template_(C%2B%2B)">C++ templates </a>are typically more cumbersome to write than the equivalent <a href="https://en.wikipedia.org/wiki/Ruby_(programming_language)">Ruby </a>or <a href="https://en.wikipedia.org/wiki/Python_(programming_language)">Python </a>code since <a href="https://en.wikipedia.org/wiki/C%2B%2B">C++ </a>has stronger rules regarding type definitions (for both functions and variables). This forces a developer to write more <a href="https://en.wikipedia.org/wiki/Boilerplate_code">boilerplate code </a>for a template than a Python developer would need to. More advanced run-time constructs such as <a href="https://en.wikipedia.org/wiki/Metaclass">metaclasses </a>and <a href="https://en.wikipedia.org/wiki/Introspection_(computer_science)">introspection </a>are often harder 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 <a href="https://en.wikipedia.org/wiki/Dynamic_programming_language">dynamic programming languages </a>; many of these are dynamically typed, although dynamic typing need not be related to dynamic programming languages .

Languages are often colloquially referred to as strongly typed or weakly typed . In fact, there is no universally accepted definition of what these terms mean. In general, there are more precise terms to represent the differences between type systems that lead people to call them "strong" or "weak".

A third way of categorizing the type system of a programming language is by the safety of typed operations and conversions. Computer scientists use the term type-safe language to describe languages that do not allow operations or conversions that violate the rules of the type system.

Computer scientists use the term memory-safe language (or just safe language ) to describe languages that do not allow programs to access memory that has not been assigned for their use. For example, a memory-safe language will <a href="https://en.wikipedia.org/wiki/Bounds_checking">check array bounds </a>, 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.

Consider the following program of a language that is both type-safe and memory-safe:<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-19">[ 17] </a>

In this example, the variable <code>z </code>will have the value 42. Although this may not be what the programmer anticipated, it is a well-defined result. If <code>y </code>were a different string, one that could not be converted to a number (e.g. "Hello World"), the result would be well-defined as well. Note that a program can be type-safe or memory-safe and still crash on an invalid operation. This is for languages where the type system is not sufficiently advanced to precisely specify the validity of operations on all possible operands. But if a program encounters an operation that is not type-safe, terminating the program is often the only option.

Now consider a similar example in C:

In this example <code>z </code>will point to a memory address five characters beyond <code>y </code>, equivalent to three characters after the terminating zero character of the string pointed to by <code>y </code>. This is memory that the program is not expected to access. In C terms this is simply <a href="https://en.wikipedia.org/wiki/Undefined_behaviour">undefined behaviour </a>and the program may do anything; with a simple compiler it might actually print whatever byte is stored after the string "37". As this example shows, C is not memory-safe. As arbitrary data was assumed to be a character, it is also not a type-safe language.

In general, type-safety and memory-safety go hand in hand. For example, a language that supports pointer arithmetic and number-to-pointer conversions (like C) is neither memory-safe nor type-safe, because it allows arbitrary memory to be accessed as if it were valid memory of any type.

For more information, see <a href="https://en.wikipedia.org/wiki/Memory_safety">memory safety </a>.

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

<ul><li>The <code>use strict </code>directive in <a href="https://en.wikipedia.org/wiki/JavaScript">JavaScript </a><a href="https://en.wikipedia.org/wiki/Type_system#cite_note-20">[ 18] </a> <a href="https://en.wikipedia.org/wiki/Type_system#cite_note-21">[ 19] </a> <a href="https://en.wikipedia.org/wiki/Type_system#cite_note-22">[ 20] </a> and <a href="https://en.wikipedia.org/wiki/Perl">Perl </a>applies stronger checking. </li><li>The <code>declare(strict_types=1) </code>in <a href="https://en.wikipedia.org/wiki/PHP">PHP </a><a href="https://en.wikipedia.org/wiki/Type_system#cite_note-23">[ 21] </a> on a per-file basis allows only a variable of exact type of the type declaration will be accepted, or a <code>TypeError </code>will be thrown. </li><li>The <code>Option Strict On </code>in <a href="https://en.wikipedia.org/wiki/VB.NET">VB.NET </a>allows the compiler to require a conversion between objects. </li> </ul>

Additional tools such as <a href="https://en.wikipedia.org/wiki/Lint_(software)">lint </a>and <a href="https://en.wikipedia.org/wiki/IBM_Rational_Purify">IBM Rational Purify </a>can also be used to achieve a higher level of strictness.

It has been proposed, chiefly by <a href="https://en.wikipedia.org/wiki/Gilad_Bracha">Gilad Bracha </a>, 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 needed. He believes this is advantageous, because what he calls mandatory type systems make languages less expressive and code more fragile.<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-Bracha-24">[ 22] </a> The requirement that the type system does not affect the semantics of the language is difficult to fulfill.

Optional typing is related to, but distinct from, <a href="https://en.wikipedia.org/wiki/Gradual_typing">gradual typing </a>. While both typing disciplines can be used to perform static analysis of code (<a href="https://en.wikipedia.org/wiki/Static_typing">static typing </a>), optional type systems do not enforce type safety at runtime (<a href="https://en.wikipedia.org/wiki/Dynamic_typing">dynamic typing </a>).<a href="https://en.wikipedia.org/wiki/Type_system#cite_note-Bracha-24">[ 22] </a> <a href="https://en.wikipedia.org/wiki/Type_system#cite_note-25">[ 23] </a>

The term polymorphism refers to the ability of code (especially, functions 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 <a href="https://en.wikipedia.org/wiki/Associative_array">associative array </a>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 <a href="https://en.wikipedia.org/wiki/Generic_programming">generic programming </a> . The type-theoretic foundations of polymorphism are closely related to those of <a href="https://en.wikipedia.org/wiki/Abstraction_(computer_science)">abstraction </a>, <a href="https://en.wikipedia.org/wiki/Module_(programming)">modularity </a>and (in some cases) <a href="https://en.wikipedia.org/wiki/Subtyping">subtyping </a>.

Many type systems have been created that are specialized for use in certain environments with certain types of data, or for out-of-band <a href="https://en.wikipedia.org/wiki/Static_program_analysis">static program analysis </a>. Frequently, these are based on ideas from formal <a href="https://en.wikipedia.org/wiki/Type_theory">type theory </a>and are only available as part of prototype research systems.

The following table gives an overview over type theoretic concepts that are used in specialized type systems. The names M, N, O range over terms and the names

range over types. The following notation will be used:

<ul><li><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d19edef7b46722a36691321bc46d47dfb44ed7a9">means that <img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f82cade9898ced02fdd08712e5f0c0151758a0dd">has type <img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/59f59b7c3e6fdb1d0365a494b81fb9a696138c36">; </li><li><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c9625cd78ee58da84ad5ea620df5441d81058aba">is that application of <img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f82cade9898ced02fdd08712e5f0c0151758a0dd">on <img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f5e3890c981ae85503089652feb48b191b57aae3">; </li><li><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2c9f20140a5b2c9c8c251fd7995c0946af39ff50">(resp. <img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c002d47c768eee1680120285b350790d373dbf23">) describes the type which results from replacing all occurrences of the type variable α (resp. term variable x ) in <img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/38a7dcde9730ef0853809fefc18d88771f95206c">by the type σ (resp. term N ). </li> </ul>

<ol><li><a href="https://en.wikipedia.org/wiki/Type_system#cite_ref-26">^ </a> Also referred to as dependent product type , since <img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e6240662486d75eeca20d70a294d7fadd3197bde">. </li><li><a href="https://en.wikipedia.org/wiki/Type_system#cite_ref-27">^ </a> Also referred to as dependent sum type , since <img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8f773dcf7d9ba08678680ac0b961b0f0ba454f28">. </li> </ol>

<a href="https://en.wikipedia.org/wiki/Dependent_type">Dependent types </a>are based on the idea of using scalars or values to more precisely describe the type of some other value. For example,

matrix. We can then define typing rules such as the following rule for matrix multiplication:

where k , m , n are arbitrary positive integer values. A variant of <a href="https://en.wikipedia.org/wiki/ML_(programming_language)">ML </a>called <a href="https://en.wikipedia.org/wiki/Dependent_ML">Dependent ML </a>has been created based on this type system, but because type checking for conventional dependent types is <a href="https://en.wikipedia.org/wiki/Decidable_set">undecidable </a>, 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 <a href="https://en.wikipedia.org/wiki/Presburger_arithmetic">Presburger arithmetic </a>.

Other languages such as <a href="https://en.wikipedia.org/wiki/Epigram_(programming_language)">Epigram </a>make the value of all expressions in the language decidable so that type checking can be decidable. However, in general <a href="https://en.wikipedia.org/wiki/Halting_Problem">proof of decidability is undecidable </a>, so many programs require hand-written annotations that may be very non-trivial. As this impedes the development process, many language implementations provide an easy way out in the form of an option to disable this condition. This, however, comes at the cost of making the type-checker run in an <a href="https://en.wikipedia.org/wiki/Infinite_loop">infinite loop </a>when fed programs that do not type-check, causing the compilation to fail.

<a href="https://en.wikipedia.org/wiki/Linear_type">Linear types </a>, based on the theory of <a href="https://en.wikipedia.org/wiki/Linear_logic">linear logic </a>, and closely related to <a href="https://en.wikipedia.org/wiki/Uniqueness_type">uniqueness types </a>, 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 <a href="https://en.wikipedia.org/wiki/Immutable_value">immutable values </a>such as files, strings, and so on, because any operation that simultaneously destroys a linear object and creates a similar object (such as <code>str = str + "a" </code>) 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 <a href="https://en.wikipedia.org/wiki/Referential_transparency">referential transparency </a>. They are also used in the prototype operating system <a href="https://en.wikipedia.org/wiki/Singularity_(operating_system)">Singularity </a>for interprocess communication, statically ensuring that processes cannot share objects in shared memory in order to prevent race conditions. The <a href="https://en.wikipedia.org/wiki/Clean_(programming_language)">Clean </a>language (a <a href="https://en.wikipedia.org/wiki/Haskell_(programming_language)">Haskell </a>-like language) uses this type system in order to gain a lot of speed (compared to performing a deep copy) while remaining safe.

Type Checking Paradigms

When type checking happens

How type checking is done

If type coercion is done

Typing paradigms in programming languages

Similar ideas