Type System Article Index for
Type
Website Links For
Type System
 

Information About

Type System




A Compiler may use the static type of a value to optimize the storage it needs and the choice of algorithms for operations on the value. For example, in many C compilers the "float" Data Type is represented in 32 Bit s, in accordance with the IEEE Specification for single-precision floating point numbers. Thus, C uses floating-point-specific operations on those values (floating-point addition, multiplication, etc.).

The depth of type constraints and the manner of their evaluation affects the ''typing'' of the language. Further, a programming language may 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.


BASIS

Assigning data types (''typing'') gives meaning to collections of Bit s. Types usually have associations either with values in Memory or with Objects such as Variables . Because any value simply consists of a set of bits in a Computer , hardware makes no distinction even between Memory Address es, Instruction Code , Characters , Integer s and Floating-point Number s. Types inform programs and programmers how they should treat those bits.

Major functions that type systems provide include:
  • Safety - Use of types may allow a Compiler to detect meaningless or probably invalid code. For example, we can identify an expression "Hello, World" --- 3 as invalid because one cannot multiply (in the usual sense) a String Literal by an Integer . As discussed below, strong typing offers more safety, but it does not necessarily guarantee complete safety (see Type-safety for more information).

  • Optimization - Static type-checking may provide useful information to a compiler. For example, if a type says a value must align at a multiple of 4, the compiler may be able to use more efficient machine instructions.

  • 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 a subtype of integers—but if a programmer declares a function as returning a timestamp rather than merely an integer, this documents part of the meaning of the function.

  • Abstraction (or '''modularity''') - Types allow programmers to think about programs at a higher level, not bothering with low-level implementation. For example, programmers can think of a string as a value instead of as a mere array of bytes. Or types can allow programmers to express the Interface between two subsystems. This localizes the definitions required for interoperability of the subsystems and prevents inconsistencies when those subsystems communicate.


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. For example:

A ''type system'', specified in each programming language, stipulates the ways typed programs may behave and makes behavior outside these rules illegal. An '' Effect System '' typically provides more fine-grained control than a type system.

More formally, Type Theory studies type systems.


TYPE CHECKING

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 enforces type rules strongly (that is, generally allowing only those automatic type conversions which do not lose information), one can refer to the process as ''strongly typed'', if not, as ''weakly typed''.


Static typing

In most compiled computer languages, like C, C++ and Pascal, the data type of every variable, parameter and function return value is known at compile time. The programmer has to provide the type information through Declaration s. This is known as static typing (but some statically typed languages may include Implicit Declarations ). A programming language is statically typed if type checking may be performed without testing equivalence of run-time expressions. A statically typed programming language respects the distinction between run-time and compile-time phases of processing. A language has a compile-time phase if separate modules of a program can be type checked separately ( Separate Compilation ), without information about all modules that exist at run time. Static type-checking becomes a primary task of the Semantic Analysis carried out by a Compiler .


Dynamic typing

  Last Harper
  First Robert
  Last2 Pierce
  First2 Benjamin C
  Year 2005
  Editor-last Pierce
  Editor-first Benjamin C
  Chapter Design Considerations for ML-Style Module Systems
  Title Advanced Topics in Types and Programming Languages
  Place Cambridge, MA
  Publisher MIT Press
  Pages 305