Система типов — совокупность правил в языках программирования, назначающих свойства, именуемые типами, различным конструкциям, составляющим программу — таким как переменные, выражения, функции или модули. Основная роль системы типов заключается в уменьшении числа багов в программах посредством определения интерфейсов между различными частями программы и последующей проверки согласованности взаимодействия этих частей. Эта проверка может происходить статически () или динамически (во время выполнения), а также быть комбинацией обоих видов.
Определение По , система типов — разрешимый синтаксический метод доказательства отсутствия определённых поведений программы путём классификации конструкций в соответствии с видами вычисляемых значений.
Описание Пример простой системы типов можно видеть в языке Си. Части программы на Си оформляются в виде определений функций. Функции вызывают друг друга. Интерфейс функции задаёт имя функции и список значений, которые передаются её телу. Вызывающая функция постулирует имя функции, которую хочет вызвать, и имена переменных, хранящих значения, которые требуется передать. Во время исполнения программы значения помещаются во временное хранилище, и затем исполнение передаётся в тело вызываемой функции. Код вызываемой функции осуществляет доступ к значениям и использует их. Если инструкции в теле функции написаны в предположении, что им на обработку должно быть передано целое значение, но вызывающий код передал число с плавающей точкой, то вызванная функция вычислит неверный результат. Компилятор Си проверяет типы, заданные для каждой переданной переменной, в отношении к типам, заданным для каждой переменной в интерфейсе вызываемой функции. Если типы не совпадают, компилятор порождает ошибку времени компиляции.
Технически, система типов назначает тип каждому вычисленному значению и затем, отслеживая последовательность этих вычислений, предпринимает попытку проверить или доказать отсутствие ошибок согласования типов. Конкретная система типов может определять, что именно приводит к ошибке, но обычно целью является предотвращение того, чтобы операции, предполагающие определённые свойства своих параметров, получали параметры, для которых эти операции не имеют смысла — предотвращение логических ошибок. Дополнительно это также предотвращает ошибки адресации памяти.
Системы типов обычно определяются как часть языков программирования и встраиваются в их интерпретаторы и компиляторы. Однако система типов языка может быть расширена посредством , осуществляющих дополнительные проверки на основе исходного синтаксиса типизации в языке.
Компилятор также может использовать статический тип значения для оптимизации хранилища и для выбора алгоритмической реализации операций над этим значением. Например, во многих компиляторах Си тип float представляется 32 битами, в соответствии со спецификацией IEEE для операций с плавающей точкой одинарной точности. На основании этого будет использоваться специальный набор инструкций микропроцессора для значений этого типа (сложение, умножение и другие операции).
Количество налагаемых на типы ограничений и способ их вычисления определяют типизацию языка. Помимо этого, в случае полиморфизма типов, язык может также задать для каждого типа операцию варьирования конкретных алгоритмов. Изучением систем типов занимается теория типов, хотя на практике конкретная система типов языка программирования основывается на особенностях архитектуры компьютера, реализации компилятора и общем образе языка.
Формальное обоснование Формальным обоснованием для систем типов служит теория типов. В состав языка программирования включается система типов для осуществления проверки типов или во время выполнения, требующая явного провозглашения типов или выводящая их самостоятельно. Марк Мэнесси () сформулировал проблему так: Основная проблема, решаемая теорией типов, состоит в том, чтобы убедиться, что программы являются осмысленными. Основная проблема, порождаемая теорией типов, состоит в том, что осмысленные программы могут не соответствовать поведению, ожидаемому от них по замыслу. Следствием этой напряжённости является поиск более мощных систем типов.
Операция назначения типа, называемая типизацией, придаёт смысл цепочкам бит, таким как значение в памяти компьютера, или объектам, таким как переменная. Компьютер не имеет возможности отличить, к примеру, адрес в памяти от инструкции кода, или символ от целого числа или числа с плавающей запятой, поскольку цепочки бит, представляющие эти различные по смыслу значения, не имеют каких-либо явных особенностей, позволяющих делать предположения об их смысле. Назначение цепочкам бит типа предоставляет это осмысление, превращая тем самым программируемое аппаратное обеспечение в символьную систему, состоящую из этого аппаратного обеспечения и программы.
Проверка согласования типов Процесс проверки и установления ограничений для типов — контроль типов или проверка соответствия типов — может осуществляться как (статическая типизация), так и во время выполнения (динамическая типизация). Возможны и промежуточные решения (ср. Последовательная типизация).
Если спецификация языка требует, чтобы правила типизации исполнялись строго (то есть допуская в той или иной мере лишь те автоматические преобразования типов, которые не теряют информацию), такой язык называется сильно типизированным (; в русской литературе преобладает вариант перевода строго типизированным), в противном случае — слабо типизированным. Эти термины являются условными и не используются в формальных обоснованиях.
Статическая проверка типов
Динамическая проверка типов и информация о типах
Строгий и нестрогий контроль типов
Типобезопасность и защита адресации памяти
Типизированные и бестиповые языки Язык называют типизированным, если спецификация каждой операции определяет типы данных, к которым эта операция может применяться, подразумевая её неприменимость к иным типам. Например, данные, которые представляет «этот текст в кавычках», имеют тип «строка». В большинстве языков программирования деление числа на строку не имеет смысла, и большинство современных языков отвергнет программу, которая пытается выполнить такую операцию. В одних языках бессмысленная операция будет выявлена (статическая типизация), и отвергнута компилятором. В других она будет выявлена во время выполнения программы (динамическая типизация), порождая исключительную ситуацию.
Особый случай типизированных языков представляют однотиповые языки (), то есть языки с единственным типом. Обычно это языки сценариев или разметки, такие как REXX и SGML, единственным типом данных в которых является символьная строка, используемая для представления как символьных, так и числовых данных.
Бестиповые языки, в противоположность типизированным, позволяют осуществлять любую операцию над любыми данными, которые в них представляются цепочками бит произвольной длины. Бестиповыми является большинство языков ассемблера. Примерами высокоуровневых бестиповых языков служат BCPL, , Forth, Рефал.
На практике, лишь некоторые языки могут считаться типизированными с точки зрения теории типов (разрешая или отвергая все операции), большинство современных языков предлагают лишь некую степень типизированности. Многие промышленные языки предоставляют возможность обойти или нарушить систему типов, поступаясь типобезопасностью ради более точного контроля над исполнением программы (каламбур типизации).
Типы и полиморфизм
Термин «полиморфизм» означает способность кода выполняться над значениями множества разных типов, или возможность разных экземпляров одной и той же структуры данных содержать элементы разных типов. Некоторые системы типов допускают полиморфизм для потенциального повышения коэффициента повторного использования кода: в языках с полиморфизмом программистам достаточно реализовать структуры данных, такие как список или ассоциативный массив, лишь единожды, и не требуется разрабатывать по одной реализации для каждого типа элементов, которые планируется хранить в этих структурах. По этой причине некоторые учёные в области информатики иногда называют использование определённых форм полиморфизма «обобщённым программированием». Обоснования полиморфизма с точки зрения теории типов практически те же, что и для абстракции, модульности и в ряде случаев .
Утиная типизация
Специальные системы типов Ряд специальных систем типов был разработан для использования в определённых условиях с определёнными данными, а также для статического анализа программ. В большинстве своём они основываются на идеях формальной теории типов и используются лишь в составе исследовательских систем.
Экзистенциальные типы Экзистенциальные типы, то есть типы, определённые посредством экзистенциального квантификатора (квантора существования), представляют собой механизм инкапсуляции на уровне типов: это композитный тип, скрывающий реализацию некоего типа в своём составе.
Понятие экзистенциального типа часто используется совместно с понятием типа записи для представления модулей и абстрактных типов данных, что обусловлено их назначением — отделением реализации от интерфейса. Например, тип T = ∃X { a: X; f: (X → int); } описывает интерфейс модуля (семейства модулей с одинаковой сигнатурой), имеющий в своём составе значение данных типа X и функцию, принимающую параметр в точности этого же типа X и возвращающую целое число. Реализация может быть различной:
intT = { a: int; f: (int → int); } floatT = { a: float; f: (float → int); }
Оба типа являются подтипами более общего экзистенциального типа T и соответствуют конкретно реализованным типам, так что любое значение, принадлежащее любому из них, принадлежит также к типу T. Если t — значение типа T, то проходит проверку типов, вне зависимости от того, к какому абстрактному типу принадлежит X. Это даёт гибкость при выборе типов, подходящих для конкретной реализации, так как пользователи извне обращаются только к значениям интерфейсного (экзистенциального) типа и изолированы от этих вариаций.
В общем случае механизм проверки согласования типов не способен определить, к какому именно экзистенциальному типу принадлежит данный модуль. В примере выше также мог бы иметь тип . Простейшим решением является явное указание для каждого модуля подразумеваемого в нём типа, например:
intT = { a: int; f: (int → int); } as ∃X { a: X; f: (X → int); }
Хотя абстрактные типы данных и модули использовались в языках программирования довольно давно, формальная модель экзистенциальных типов была построена лишь к 1988 году. Теория представляет собой типизированное лямбда-исчисление второго порядка, аналогичное Системе F, но с экзистенциальной квантификацией вместо универсальной.
Экзистенциальные типы явным образом доступны в качестве экспериментального расширения языка Haskell, где они представляют собой специальный синтаксис, позволяющий использовать переменную типа в определении алгебраического типа, не вынося её в сигнатуру конструктора типов, то есть не повышая его арность. Язык Java предоставляет ограниченную форму экзистенциальных типов посредством . В языках, реализующих классический let-полиморфизм в стиле ML, экзистенциальные типы могут быть симулированы посредством так называемых «значений, индексированных типами».
Явное и неявное назначение типов
Многие статические системы типов, например, такие как в языках Си и Java, требуют провозглашения типа: программист должен явно назначать каждой переменной конкретный тип. Другие, такие как система типов Хиндли — Милнера, применяемая в языках ML и Haskell, осуществляют выведение типов: компилятор выстраивает заключение о типах переменных на основании того, как программист использует эти переменные.
Например, для функции f(x,y), осуществляющей сложение x и y, компилятор может сделать вывод, что x и y должны быть числами — поскольку операция сложения определена только для чисел. Следовательно, вызов где-либо в программе функции f для параметров, отличных от числовых, (например, для строки или списка) сигнализирует об ошибке.