Система типов

Эта статья поднимает множество проблем. Пожалуйста, помогите улучшить его или обсудите эти проблемы на странице обсуждения . ( Узнайте, как и когда удалить эти сообщения-шаблоны ) Эта статья включает в себя список общих ссылок , но он остается в значительной степени непроверенным, поскольку в нем отсутствует достаточное количество соответствующих встроенных ссылок . Пожалуйста, помогите улучшить эту статью, добавив более точные цитаты. ( Октябрь 2010 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) Эта статья написана как личное размышление, личное эссе или аргументированное эссе , в котором излагаются личные чувства редактора Википедии или представлены оригинальные аргументы по теме. Пожалуйста, помогите улучшить его , переписав в энциклопедическом стиле . ( Июль 2016 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) ( Узнайте, как и когда удалить этот шаблон сообщения )

В языках программирования система типов - это логическая система, содержащая набор правил, которые присваивают свойство, называемое типом, различным конструкциям компьютерной программы , таким как переменные , выражения , функции или модули . ^[1] Эти типы формализуют и применяют неявные категории, которые программист использует для алгебраических типов данных, структур данных или других компонентов (например, «строка», «массив с плавающей запятой», «функция, возвращающая логическое значение»). Основная цель системы типов - уменьшить вероятность ошибок.в компьютерных программах ^[2] , определяя интерфейсы между различными частями компьютерной программы, а затем проверяя, что эти части были соединены последовательным образом. Эта проверка может происходить статически (во время компиляции ), динамически (во время выполнения ) или как комбинация обоих. Системы типов имеют и другие цели, такие как выражение бизнес-правил, включение определенных оптимизаций компилятора , разрешение множественной отправки , предоставление формы документации и т. Д.

Система типов связывает тип с каждым вычисленным значением и, исследуя поток этих значений, пытается гарантировать или доказать, что ошибки типа не могут произойти. Данная система типов, о которой идет речь, определяет, что составляет ошибку типа, но в целом цель состоит в том, чтобы предотвратить операции, ожидающие использования определенного вида значения со значениями, для которых эта операция не имеет смысла ( логические ошибки ). Системы типов часто указываются как часть языков программирования и встроены в интерпретаторы и компиляторы, хотя система типов языка может быть расширена дополнительными инструментами, которые выполняют дополнительные проверки с использованием синтаксиса и грамматики исходного типа языка.

Обзор использования [ править ]

Пример простой системы типа является то , что на языке Си . Части программы C - это определения функций . Одна функция вызывается другой функцией. Интерфейс функции указывает имя функции и список значений, которые передаются в код функции. В коде вызывающей функции указывается имя вызываемой функции, а также имена переменных, которые содержат значения для передачи ей. Во время выполнения значения помещаются во временное хранилище, затем выполнение переходит к коду вызванной функции. Код вызываемой функции получает доступ к значениям и использует их. Если инструкции внутри функции написаны с предположением получения целочисленного значения, но вызывающий код передалзначение с плавающей запятой , то вызванная функция будет вычислять неверный результат. Компилятор C проверяет типы аргументов, переданных функции, когда она вызывается, по типам параметров, объявленных в определении функции. Если типы не совпадают, компилятор выдает ошибку времени компиляции.

Компилятор может также использовать тип статики значение для оптимизации хранения он нуждается и выбор алгоритмов для операций по стоимости. Например, во многих компиляторах C тип данных с плавающей запятой представлен в 32- битном формате в соответствии со спецификацией IEEE для чисел с плавающей запятой одинарной точности . Таким образом, они будут использовать микропроцессорные операции с плавающей запятой над этими значениями (сложение с плавающей запятой, умножение и т. Д.).

Глубина ограничений типа и способ их оценки влияют на типизацию языка. Язык программирования может дополнительно связать операцию с различными разрешениями для каждого типа, в случае типа полиморфизма . Теория типов - это изучение систем типов. Конкретные типы некоторых языков программирования, такие как целые числа и строки, зависят от практических вопросов компьютерной архитектуры, реализации компилятора и дизайна языка.

Основы [ править ]

Формально теория типов изучает системы типов. Язык программирования должен иметь вхождение для проверки типа с использованием системы типов, будь то во время компиляции или во время выполнения, с аннотациями вручную или с автоматическим выводом. Как кратко выразился Марк Манассе : ^[3]

Фундаментальная проблема, решаемая теорией типов, состоит в том, чтобы гарантировать, что программы имеют смысл. Основная проблема, вызванная теорией типов, состоит в том, что значимые программы могут не иметь значения, приписываемого им. Стремление к более богатым системам типов проистекает из этого противоречия.

Присвоение типа данных, называемое типизацией , придает смысл последовательности битов, такой как значение в памяти или некоторый объект, такой как переменная . Аппаратное обеспечение компьютера общего назначения неспособно различать, например, адрес памяти и код инструкции , или между символом , целым числом или числом с плавающей запятой , поскольку оно не делает внутреннего различия между любыми из возможных значений, которые последовательность битов может означать . ^{[примечание 1]} Связывание последовательности битов с типом означает, чтоозначает, что программируемое оборудование формирует символическую систему, состоящую из этого оборудования и некоторой программы.

Программа связывает каждое значение по крайней мере с одним конкретным типом, но также может случиться так, что одно значение связано со многими подтипами . Другие сущности, такие как объекты , модули , каналы связи и зависимости, могут быть связаны с типом. Даже тип может быть связан с типом. Реализация системы типов теоретически может связывать идентификации, называемые типом данных (тип значения), классом (типом объекта) и типом ( типом типа или метатипом). Это абстракции, через которые может проходить типизация в иерархии уровней, содержащихся в системе.

Когда язык программирования развивает более сложную систему типов, он получает более детализированный набор правил, чем базовая проверка типов, но за это приходится расплачиваться, когда выводы типа (и другие свойства) становятся неразрешимыми , и когда необходимо уделять больше внимания программист для аннотирования кода или рассмотрения операций и функционирования, связанных с компьютером. Трудно найти достаточно выразительную систему типов, которая удовлетворяла бы всем методам программирования безопасным способом.

Чем больше ограничений типов накладывает компилятор, тем сильнее типизирован язык программирования. Строго типизированные языки часто требуют от программиста явного преобразования в контекстах, где неявное преобразование не причинит вреда. Система типов Паскаля была описана как «слишком сильная», потому что, например, размер массива или строки является частью его типа, что затрудняет некоторые задачи программирования. ^{[4] [5]} Haskell также строго типизирован, но его типы определяются автоматически, поэтому явные преобразования часто не нужны.

Компилятор языка программирования может также реализовать зависимый тип или систему эффектов , что позволяет проверять еще больше программных спецификаций с помощью средства проверки типов. Помимо простых пар значение-тип, виртуальная «область» кода связана с компонентом «эффекта», описывающим, что и с чем делается , и позволяющим, например, «выдавать» отчет об ошибке. Таким образом, символьная система может быть системой типов и эффектов , что наделяет ее большей проверкой безопасности, чем только проверка типов.

Независимо от того, автоматизирована ли она компилятором или указана программистом, система типов делает поведение программы незаконным, если оно выходит за рамки правил системы типов. Преимущества, предоставляемые системами типов, определяемыми программистом, включают:

• Абстракция (или модульность ) - типы позволяют программистам думать на более высоком уровне, чем бит или байт, не беспокоясь о низкоуровневой реализации. Например, программисты могут начать думать о строке как о наборе символьных значений, а не как о простом массиве байтов. Более того, типы позволяют программистам обдумывать и выражать интерфейсы между двумя подсистемами любого размера. Это обеспечивает больше уровней локализации, так что определения, необходимые для взаимодействия подсистем, остаются согласованными, когда эти две подсистемы обмениваются данными.
• Документация. В более выразительных системах типов типы могут служить формой документации, разъясняющей намерения программиста. Например, если программист объявляет функцию как возвращающую тип отметки времени, это документирует функцию, когда тип отметки времени может быть явно объявлен глубже в коде как целочисленный тип.

Преимущества, предоставляемые системами типов, определяемыми компилятором, включают:

• Оптимизация. Статическая проверка типов может предоставить полезную информацию во время компиляции. Например, если для типа требуется, чтобы значение в памяти было выровнено с точностью до четырех байтов, компилятор может использовать более эффективные машинные инструкции.
• Безопасность - система типов позволяет компилятору обнаруживать бессмысленный или, возможно, неверный код. Например, мы можем идентифицировать выражение 3 / "Hello, World"как недопустимое, если в правилах не указано, как делить целое число на строку . Строгая типизация обеспечивает большую безопасность, но не может гарантировать полную безопасность типов .

Ошибки типа [ править ]

Ошибка типа - это непреднамеренное состояние, которое может проявляться на нескольких этапах разработки программы. Таким образом, в системе типов требуется средство обнаружения ошибки. В некоторых языках, таких как Haskell, для которых определение типа автоматизировано, компилятор может использовать lint для помощи в обнаружении ошибок.

Безопасность типов способствует правильности программы , но может гарантировать правильность только за счет того, что сама проверка типов становится неразрешимой проблемой . ^{[ необходимая цитата ]} В системе типов с автоматической проверкой типов программа может работать некорректно, но при этом безопасно набираться и не вызывать ошибок компилятора. Деление на ноль - небезопасная и неправильная операция, но средство проверки типов, работающее только во время компиляции , не сканирует деление на ноль на большинстве языков, и тогда это остается как ошибка времени выполнения . Чтобы доказать отсутствие этих дефектов более общего, чем типов, используются другие формальные методы., в совокупности известные как программный анализ , широко используются. В качестве альтернативы достаточно выразительная система типов, например, в языках с зависимой типизацией, может предотвратить подобные ошибки (например, выражение типа ненулевых чисел ). Кроме того, тестирование программного обеспечения - это эмпирический метод поиска ошибок, которые средство проверки типов не может обнаружить.

Проверка типа [ править ]

Процесс проверки и применения ограничений типов - проверка типов - может происходить либо во время компиляции (статическая проверка), либо во время выполнения . Если спецификация языка строго требует своих правил типизации (т. Е. Более или менее разрешающих только те автоматические преобразования типов, которые не теряют информацию), можно называть процесс строго типизированным , а если нет - слабо типизированным . Эти термины обычно не используются в строгом смысле.

Статическая проверка типа [ править ]

Статическая проверка типов - это процесс проверки типовой безопасности программы на основе анализа текста программы ( исходного кода ). Если программа проходит проверку статического типа, то программа гарантированно удовлетворяет некоторому набору свойств безопасности типа для всех возможных входных данных.

Статическая проверка типов может рассматриваться как ограниченная форма проверки программы (см. Безопасность типов ), а на языке безопасности типов может считаться также оптимизацией. Если компилятор может доказать, что программа хорошо типизирована, ему не нужно производить динамические проверки безопасности, что позволяет скомпилированному двоичному файлу работать быстрее и быть меньшего размера.

Статическая проверка типов для полных по Тьюрингу языков по своей сути консервативна. То есть, если система типов является одновременно надежной (это означает, что она отклоняет все неправильные программы) и разрешимой (что означает, что можно написать алгоритм, который определяет, правильно ли типизирована программа), то она должна быть неполной (что означает наличие являются правильными программами, которые также отклоняются, даже если они не обнаруживают ошибок времени выполнения). ^[6] Например, рассмотрим программу, содержащую код:

if <complex test> then <do something> else <signal that there is a type error>

Даже если выражение <complex test>всегда вычисляется trueво время выполнения, большинство средств проверки типов отклонят программу как некорректно типизированную, потому что для статического анализатора трудно (если вообще возможно) определить, что elseпереход не будет выполнен. ^[7] И наоборот, средство проверки статического типа быстро обнаруживает ошибки типа в редко используемых путях кода. Без проверки статического типа даже тесты покрытия кода со 100% покрытием могут не найти такие ошибки типа. Тесты могут не обнаружить такие ошибки типа, потому что необходимо учитывать комбинацию всех мест, где создаются значения, и всех мест, где используется определенное значение.

Ряд полезных и распространенных функций языка программирования невозможно проверить статически, например, приведение с понижением . Таким образом, во многих языках есть как статическая, так и динамическая проверка типов; средство проверки статического типа проверяет то, что может, а динамические проверки проверяют все остальное.

Многие языки со статической проверкой типов предоставляют способ обойти проверку типов. Некоторые языки позволяют программистам выбирать между безопасностью статического и динамического типов. Например, C # различает статически типизированные и динамически типизированные переменные. Использование первых проверяется статически, тогда как использование последних проверяется динамически. Другие языки позволяют писать код, который не является типобезопасным; например, в C программисты могут свободно преобразовывать значение между любыми двумя типами, имеющими одинаковый размер, эффективно подрывая концепцию типа.

Список языков с проверкой статического типа см. В категории языков со статической типизацией .

Информация о динамической проверке типа и времени выполнения [ править ]

Проверка динамического типа - это процесс проверки типовой безопасности программы во время выполнения. Реализации языков с динамической проверкой типов обычно связывают каждый объект среды выполнения с тегом типа (т. Е. Ссылкой на тип), содержащим информацию о его типе. Эта информация о типе времени выполнения (RTTI) также может использоваться для реализации динамической отправки , позднего связывания , преобразования с понижением , отражения и подобных функций.

Большинство языков с безопасным типом включают некоторую форму проверки динамического типа, даже если в них также есть средство проверки статического типа. ^{[ необходима цитата ] [8]} Причина в том, что многие полезные функции или свойства трудно или невозможно проверить статически. Например, предположим, что программа определяет два типа, A и B, где B является подтипом A. Если программа пытается преобразовать значение типа A в тип B, что называется понижающим преобразованием , тогда операция допустима только если преобразуемое значение на самом деле является значением типа B. Таким образом, необходима динамическая проверка, чтобы убедиться, что операция безопасна. Это требование является одним из критических замечаний по поводу понижения.

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 the category for dynamically-typed programming languages.

Combining static and dynamic type checking[edit]

Some languages allow both static and dynamic typing. For example, Java and some other ostensibly statically-typed languages support downcasting types to their subtypes, querying an object to discover its dynamic type and other type operations that depend on runtime type information. Another example is C++ RTTI. More generally, most programming languages include mechanisms for dispatching over different 'kinds' of data, such as disjoint unions, runtime polymorphism, 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.

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 Liskov substitution principle, 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 subtype polymorphism. In some languages subtypes may also possess covariant or contravariant return types and argument types respectively.

Certain languages, for example Clojure, Common Lisp, or Cython 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 gradual typing. The programming environment DrRacket, a pedagogic environment based on Lisp, and a precursor of the language Racket is also soft-typed.^[9]

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 dynamic will not be subject to static type checking. Instead, the program relies on runtime type information to determine how the variable may be used.^[10]

Static and dynamic type checking in practice[edit]

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

Static typing can find type errors reliably at compile time, which should increase 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.^[11][12] Static typing advocates^[who?] believe programs are more reliable when they have been well type-checked, whereas dynamic-typing advocates^[who?] point to distributed code that has proven reliable and to small bug databases.^{[citation needed]} The value of static typing, then, presumably^[vague] increases as the strength of the type system is increased. Advocates of dependent typing,^[who?] implemented in 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.^[13]

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 Common Lisp allow optional type declarations for optimization for this reason.

By contrast, dynamic typing may allow compilers to run faster and interpreters 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.^{[clarification needed]} This too may reduce the edit-compile-test-debug cycle.

Statically-typed languages that lack type inference (such as C and Java prior to version 10) 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 Haskell, Scala, OCaml, F#, and to a lesser extent C# and 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. Further, 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 data structure (usually for the purposes of experimentation and testing).

Dynamic typing typically allows duck typing (which enables easier code reuse). Many^[specify] languages with static typing also feature duck typing or other mechanisms like generic programming that also enable easier code reuse.

Dynamic typing typically makes metaprogramming easier to use. For example, C++ templates are typically more cumbersome to write than the equivalent Ruby or Python code since C++ has stronger rules regarding type definitions (for both functions and variables). This forces a developer to write more boilerplate code for a template than a Python developer would need to. More advanced run-time constructs such as metaclasses and introspection 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 dynamic programming languages; many of these are dynamically typed, although dynamic typing need not be related to dynamic programming languages.

Strong and weak type systems[edit]

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".

Type safety and memory safety[edit]

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 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.

Consider the following program of a language that is both type-safe and memory-safe:^[14]

var x := 5;
var y := "37";
var z := x + y;

In this example, the variable z will have the value 42. Although this may not be what the programmer anticipated, it is a well-defined result. If y 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; in fact, 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:

int x = 5;char y[] = "37";char* z = x + y;

In this example z will point to a memory address five characters beyond y, equivalent to three characters after the terminating zero character of the string pointed to by y. This is memory that the program is not expected to access. It may contain garbage data, and it certainly doesn't contain anything useful. As this example shows, C is neither a memory-safe nor 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 memory safety.

Variable levels of type checking[edit]

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

• The use strict directive in JavaScript^[15][16][17] and Perl applies stronger checking.
• The declare(strict_types=1) in PHP^[18] on a per-file basis allows only a variable of exact type of the type declaration will be accepted, or a TypeError will be thrown.
• 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[edit]

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 needed. He believes this is advantageous, because what he calls mandatory type systems make languages less expressive and code more fragile.^[19] The requirement that types do not affect the semantics of the language is difficult to fulfill.

Optional typing is related to, but distinct from, gradual typing. While both typing disciplines can be used to perform static analysis of code (static typing), optional type systems do not enforce type safety at runtime (dynamic typing). ^[19][20]

Polymorphism and types[edit]

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 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.

Specialized type systems[edit]

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.

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 ${\displaystyle \sigma ,\tau }$ range over types. The notation ${\displaystyle \tau [\alpha :=\sigma ]}$ (resp. ${\displaystyle \tau [x:=N]}$) describes the type which results from replacing all occurrences of the type variable α (resp. term variable x) in τ by the type σ (resp. term N).

Type notion	Notation	Meaning
Function	${\displaystyle \sigma \to \tau }$	If M has type ${\displaystyle \sigma \to \tau }$ and N has type σ, then the application ${\displaystyle M(N)}$ has type τ.
Product	${\displaystyle \sigma \times \tau }$	If M has type ${\displaystyle \sigma \times \tau }$, then ${\displaystyle M=(N,O)}$ is a pair such that N has type σ and O has type τ.
Sum	${\displaystyle \sigma +\tau }$	If M has type ${\displaystyle \sigma +\tau }$, then either ${\displaystyle M=\iota _{1}(N)}$ is the first injection such that N has type σ, or ${\displaystyle M=\iota _{2}(N)}$ is the second injection such that N has type τ.
Intersection	${\displaystyle \sigma \cap \tau }$	If M has type ${\displaystyle \sigma \cap \tau }$, then M has type σ and M has type τ.
Union	${\displaystyle \sigma \cup \tau }$	If M has type ${\displaystyle \sigma \cup \tau }$, then M has type σ or M has type τ.
Record	${\displaystyle \langle x:\tau \rangle }$	If M has type ${\displaystyle \langle x:\tau \rangle }$, then M has a member x that has type τ.
Polymorphic	${\displaystyle \forall \alpha .\tau }$	If M has type ${\displaystyle \forall \alpha .\tau }$, then M has type ${\displaystyle \tau [\alpha :=\sigma ]}$ for any type σ.
Existential	${\displaystyle \exists \alpha .\tau }$	If M has type ${\displaystyle \exists \alpha .\tau }$, then M has type ${\displaystyle \tau [\alpha :=\sigma ]}$ for some type σ.
Recursive	${\displaystyle \mu \alpha .\tau }$	If M has type ${\displaystyle \mu \alpha .\tau }$, then M has type ${\displaystyle \tau [\alpha :=\mu \alpha .\tau ]}$.
Dependent function	${\displaystyle (x:\sigma )\to \tau }$	If M has type ${\displaystyle (x:\sigma )\to \tau }$ and N has type σ, then the application ${\displaystyle M(N)}$ has type ${\displaystyle \tau [x:=N]}$.
Dependent product	${\displaystyle (x:\sigma )\times \tau }$	If M has type ${\displaystyle (x:\sigma )\times \tau }$, then ${\displaystyle M=(N,O)}$ is a pair such that N has type σ and O has type ${\displaystyle \tau [x:=N]}$.
Dependent intersection[21]	${\displaystyle (x:\sigma )\cap \tau }$	If M has type ${\displaystyle (x:\sigma )\cap \tau }$, then M has type σ and M has type ${\displaystyle \tau [x:=M]}$.
Familial intersection[21]	${\displaystyle \bigcap _{x:\sigma }\tau }$	If M has type ${\displaystyle \bigcap _{x:\sigma }\tau }$, then M has type ${\displaystyle \tau [x:=N]}$ for any term N of type σ.
Familial union[21]	${\displaystyle \bigcup _{x:\sigma }\tau }$	If M has type ${\displaystyle \bigcup _{x:\sigma }\tau }$, then M has type ${\displaystyle \tau [x:=N]}$ for some term N of type σ.

Dependent types[edit]

Dependent types are based on the idea of using scalars or values to more precisely describe the type of some other value. For example, ${\displaystyle \mathrm {matrix} (3,3)}$ might be the type of a ${\displaystyle 3\times 3}$ matrix. We can then define typing rules such as the following rule for matrix multiplication:

${\displaystyle \mathrm {matrix} _{\mathrm {multiply} }:\mathrm {matrix} (k,m)\times \mathrm {matrix} (m,n)\to \mathrm {matrix} (k,n)}$

where k, m, 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. However, in general proof of decidability is undecidable, 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 infinite loop when fed programs that do not type-check, causing the compilation to fail.

Linear types[edit]

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 (compared to performing a deep copy) while remaining safe.

Intersection types[edit]

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 "int → int" is the type of functions taking an integer argument and returning an integer, and "float → float" 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 "int → int" function safely; it simply would not use the "float → float" 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[edit]

Union types are types describing values that belong to either of two types. For example, in C, the signed char has a -128 to 127 range, and the unsigned char has a 0 to 255 range, so the union of these two types would have an overall "virtual" range of -128 to 255 that may be used partially depending on which union member is accessed. 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[edit]

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 named a of type X and a function named f 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".^[22] The theory is a second-order typed lambda calculus similar to System F, but with existential instead of universal quantification.

Gradual typing[edit]

Gradual typing is a type system in which variables may be assigned a type either at compile-time (which is static typing) or at run-time (which is dynamic typing), allowing software developers to choose either type paradigm as appropriate, from within a single language.^[23] In particular, gradual typing uses a special type named dynamic to represent statically-unknown types, and gradual typing replaces the notion of type equality with a new relation called consistency that relates the dynamic type to every other type. The consistency relation is symmetric but not transitive.^[24]

Explicit or implicit declaration and inference[edit]

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

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

Type inference is in general possible, if it is computable in the type system in question. Moreover, even if inference is not computable in general for a given type system, 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 computable. Most Haskell compilers allow arbitrary-rank polymorphism as an extension, but this makes type inference not computable. (Type checking is decidable, however, and rank-1 programs still have type inference; higher rank polymorphic programs are rejected unless given explicit type annotations.)

Decision problems[edit]

A type system that assigns types to terms in type environments using type rules is naturally associated with the decision problems of type checking, typability, and type inhabitation.^[25]

• Given a type environment ${\displaystyle \Gamma }$, a term ${\displaystyle e}$, and a type ${\displaystyle \tau }$, decide whether the term ${\displaystyle e}$ can be assigned the type ${\displaystyle \tau }$ in the type environment.
• Given a term ${\displaystyle e}$, decide whether there exists a type environment ${\displaystyle \Gamma }$ and a type ${\displaystyle \tau }$ such that the term ${\displaystyle e}$ can be assigned the type ${\displaystyle \tau }$ in the type environment ${\displaystyle \Gamma }$.
• Given a type environment ${\displaystyle \Gamma }$ and a type ${\displaystyle \tau }$, decide whether there exists a term ${\displaystyle e}$ that can be assigned the type ${\displaystyle \tau }$ in the type environment.

Unified type system[edit]

Some languages like C# or Scala have a unified type system.^[26] This means that all C# types including primitive types inherit from a single root object. Every type in C# inherits from the Object class. Some languages, like Java and Raku, have a root type but also have primitive types that are not objects.^[27] 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. Raku automatically converts primitive types to objects when their methods are accessed.^[28]

Compatibility: equivalence and subtyping[edit]

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 example, 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. Thus, in the simplest type systems, 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 that describe values with the same structure are equivalent, 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 B is a subtype of A, then a value of type B can be used in a context where one of type A is expected (covariant), 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.

See also[edit]

• Comparison of type systems
• Covariance and contravariance (computer science)
• Polymorphism in object-oriented programming
• Type rules
• Type signature
• Type theory

Notes[edit]

References[edit]

Further reading[edit]

• Cardelli, Luca; Wegner, Peter (December 1985). "On Understanding Types, Data Abstraction, and Polymorphism" (PDF). ACM Computing Surveys. 17 (4): 471–523. CiteSeerX 10.1.1.117.695. doi:10.1145/6041.6042. S2CID 2921816.
• Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.
• Cardelli, Luca (2004). "Type systems" (PDF). In Allen B. Tucker (ed.). CRC Handbook of Computer Science and Engineering (2nd ed.). CRC Press. ISBN 978-1584883609.
• Tratt, Laurence (July 2009). "5. Dynamically Typed Languages". Advances in Computers. 77. Elsevier. pp. 149–184. doi:10.1016/S0065-2458(09)01205-4. ISBN 978-0-12-374812-6.

External links[edit]

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

The Wikibook Haskell has a page on the topic of: Class declarations

• Media related to Type systems at Wikimedia Commons
• Smith, Chris (2011). "What to Know Before Debating Type Systems".