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

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

По Пирсу^[англ.], система типов — разрешимый синтаксический метод доказательства отсутствия определённых поведений программы путём классификации конструкций в соответствии с видами вычисляемых значений^[2].

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

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

Системы типов обычно определяются как часть языков программирования и встраиваются в их интерпретаторы и компиляторы. Однако система типов языка может быть расширена посредством специальных инструментов^[англ.], осуществляющих дополнительные проверки на основе исходного синтаксиса типизации в языке.

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

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

Формальным обоснованием для систем типов служит теория типов. В состав языка программирования включается система типов для осуществления проверки типов во время компиляции^[англ.] или во время выполнения, требующая явного провозглашения типов или выводящая их самостоятельно. Марк Мэнесси (англ. Mark Manasse) сформулировал проблему так^[3]:

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

Оригинальный текст (англ.)

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.

— Марк Мэнесси^[3]

Операция назначения типа, называемая типизацией, придаёт смысл цепочкам бит, таким как значение в памяти компьютера, или объектам, таким как переменная. Компьютер не имеет возможности отличить, к примеру, адрес в памяти от инструкции кода, или символ от целого числа или числа с плавающей запятой, поскольку цепочки бит, представляющие эти различные по смыслу значения, не имеют каких-либо явных особенностей, позволяющих делать предположения об их смысле. Назначение цепочкам бит типа предоставляет это осмысление, превращая тем самым программируемое аппаратное обеспечение в символьную систему, состоящую из этого аппаратного обеспечения и программы.

Процесс проверки и установления ограничений для типов — контроль типов или проверка соответствия типов — может осуществляться как на стадии компиляции^[англ.] (статическая типизация), так и во время выполнения (динамическая типизация). Возможны и промежуточные решения (ср. Последовательная типизация).

Если спецификация языка требует, чтобы правила типизации исполнялись строго (то есть допуская в той или иной мере лишь те автоматические преобразования типов, которые не теряют информацию), такой язык называется сильно типизированным (англ. strongly typed; в русской литературе преобладает вариант перевода строго типизированным), в противном случае — слабо типизированным. Эти термины являются условными и не используются в формальных обоснованиях.

Язык называют типизированным, если спецификация каждой операции определяет типы данных, к которым эта операция может применяться, подразумевая её неприменимость к иным типам^[4]. Например, данные, которые представляет «этот текст в кавычках», имеют тип «строка». В большинстве языков программирования деление числа на строку не имеет смысла, и большинство современных языков отвергнет программу, которая пытается выполнить такую операцию. В одних языках бессмысленная операция будет выявлена в процессе компиляции^[англ.] (статическая типизация), и отвергнута компилятором. В других она будет выявлена во время выполнения программы (динамическая типизация), порождая исключительную ситуацию.

Особый случай типизированных языков представляют однотиповые языки (англ. single-type language), то есть языки с единственным типом. Обычно это языки сценариев или разметки, такие как REXX и SGML, единственным типом данных в которых является символьная строка, используемая для представления как символьных, так и числовых данных.

Бестиповые языки, в противоположность типизированным, позволяют осуществлять любую операцию над любыми данными, которые в них представляются цепочками бит произвольной длины^[4]. Бестиповыми является большинство языков ассемблера. Примерами высокоуровневых бестиповых языков служат BCPL, BLISS^[англ.], Forth, Рефал.

На практике, лишь некоторые языки могут считаться типизированными с точки зрения теории типов (разрешая или отвергая все операции), большинство современных языков предлагают лишь некую степень типизированности^[4]. Многие промышленные языки предоставляют возможность обойти или нарушить систему типов, поступаясь типобезопасностью ради более точного контроля над исполнением программы (каламбур типизации).

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

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

Экзистенциальные типы, то есть типы, определённые посредством экзистенциального квантификатора (квантора существования), представляют собой механизм инкапсуляции на уровне типов: это композитный тип, скрывающий реализацию некоего типа в своём составе.

Понятие экзистенциального типа часто используется совместно с понятием типа записи для представления модулей и абстрактных типов данных, что обусловлено их назначением — отделением реализации от интерфейса. Например, тип 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, то t.f(t.a) проходит проверку типов, вне зависимости от того, к какому абстрактному типу принадлежит X. Это даёт гибкость при выборе типов, подходящих для конкретной реализации, так как пользователи извне обращаются только к значениям интерфейсного (экзистенциального) типа и изолированы от этих вариаций.

В общем случае механизм проверки согласования типов не способен определить, к какому именно экзистенциальному типу принадлежит данный модуль. В примере выше intT { a: int; f: (int → int); } также мог бы иметь тип ∃X { a: X; f: (int → int); }. Простейшим решением является явное указание для каждого модуля подразумеваемого в нём типа, например:

• intT = { a: int; f: (int → int); } as ∃X { a: X; f: (X → int); }

Хотя абстрактные типы данных и модули использовались в языках программирования довольно давно, формальная модель экзистенциальных типов была построена лишь к 1988 году^[5]. Теория представляет собой типизированное лямбда-исчисление второго порядка, аналогичное Системе F, но с экзистенциальной квантификацией вместо универсальной.

Экзистенциальные типы явным образом доступны в качестве экспериментального расширения языка Haskell, где они представляют собой специальный синтаксис, позволяющий использовать переменную типа в определении алгебраического типа, не вынося её в сигнатуру конструктора типов, то есть не повышая его арность^[6]. Язык Java предоставляет ограниченную форму экзистенциальных типов посредством джокера^[англ.]. В языках, реализующих классический let-полиморфизм в стиле ML, экзистенциальные типы могут быть симулированы посредством так называемых «значений, индексированных типами»^[7].

Многие статические системы типов, например, такие как в языках Си и Java, требуют провозглашения типа: программист должен явно назначать каждой переменной конкретный тип. Другие, такие как система типов Хиндли — Милнера, применяемая в языках ML и Haskell, осуществляют выведение типов: компилятор выстраивает заключение о типах переменных на основании того, как программист использует эти переменные.

Например, для функции f(x,y), осуществляющей сложение x и y, компилятор может сделать вывод, что x и y должны быть числами — поскольку операция сложения определена только для чисел. Следовательно, вызов где-либо в программе функции f для параметров, отличных от числовых, (например, для строки или списка) сигнализирует об ошибке.

Числовые и строковые константы и выражения обычно зачастую выражают тип в конкретном контексте. Например, выражение 3.14 может подразумевать вещественное число, тогда как [1,2,3] может быть списком целых — обычно массивом.

Вообще говоря, выведение типов возможно, если оно принципиально разрешимо в теории типов. Более того, даже если выведение неразрешимо для данной теории типов, выведение зачастую возможно для многих реальных программ. Система типов языка Haskell, являющаяся разновидностью системы типов Хиндли — Милнера, представляет собой ограничение Системы Fω^[англ.] для так называемых полиморфных типов первого ранга, на которых выведение разрешимо. Многие компиляторы Хаскела предоставляют полиморфизм произвольного ранга в качестве расширения, но это делает выведение типов неразрешимым, так что требуется явное провозглашение типов. Однако, проверка согласования типов остаётся разрешимой и для программ с полиморфизмом первого ранга типы по-прежнему выводимы.

Некоторые языки, например, C#, имеют унифицированную систему типов^[8]. Это означает, что все типы языка вплоть до примитивных наследуются от единого корневого объекта (в случае с C# — от класса Object). В Java есть несколько примитивных типов, не являющихся объектами. Наряду с ними Java также предоставляет обёрточные объектные типы, так что разработчик может использовать примитивные или объектные типы по своему усмотрению.

Механизм проверки согласования типов в языке со статической типизацией проверяет, что всякое выражение соответствует типу, ожидаемому тем контекстом, в котором оно присутствует. Например, в операторе присваивания вида x := e выведенный для выражения e тип должен соответствовать типу, который провозглашён или выведен для переменной x. Нотация соответствия, называемая совместимостью, специфична для каждого языка.

Если e и x имеют единый тип, и присваивание разрешено для этого типа, то это выражение является корректным. Поэтому в простейших системах типов вопрос совместимости двух типов упрощается до вопроса их равенства (эквивалентности). Однако разные языки имеют разные критерии для определения совместимости типов двух выражений. Эти теории эквивалентности варьируются между двумя крайними случаями: структурными системами типов (англ. structural type system), в которых два типа эквивалентны, если описывают одинаковую внутреннюю структуру значения; и номинативными системами типов (англ. nominative type system), в которых синтаксически различные типы никогда не эквивалентны (то есть два типа равны только в том случае, если равны их идентификаторы).

В языках с подтипами^[англ.] правила совместимости более сложные. Например, если A является подтипом B, то значение, принадлежащее типу A, может быть использовано в контексте, ожидающем значение типа B, даже если обратное неверно. Как и в случае эквивалентности, отношения подтипов различаются в разных языках, и здесь возможно много вариантов правил. Наличие в языке параметрического или ситуативного полиморфизма может также влиять на совместимость типов.

Одни программисты предпочитают статические системы типов, другие — динамические. Статически типизированные языки сигнализируют об ошибках согласования типов на этапе компиляции^[англ.], могут порождать более эффективно исполняемый код, и для таких языков осуществимо более релевантное автодополнение в интегрированных средах разработки. Сторонники динамической типизации утверждают, что они лучше подходят для быстрого прототипирования, и что ошибки согласования типов составляют лишь малую часть возможных ошибок в программах^[9][10]. С другой стороны, в статически типизированных языках явная декларация типов обычно не требуется, если язык поддерживает вывод типов, а некоторые динамически типизированные языки производят оптимизацию на этапе выполнения программы^[11][12], зачастую посредством применения частичного вывода типов^[13].

• Сравнение систем типов
• Ковариантность и контравариантность (программирование)
• Полиморфизм
• Перегрузка операторов
• Наличие знака^[англ.]
• Правила, устанавливаемые для типов^[англ.]
• Сигнатура типа^[англ.]

• Luca Cardelli, Peter Wegner. On Understanding Types, Data Abstraction, and Polymorphism. — ACM Computing Surveys, 1985. — С. 471—523. — ISSN 0360-0300.
• Benjamin C. Pierce. Types and Programming Languages. — MIT Press, 2002. — ISBN 978-0-262-16209-8.
• Luca Cardelli. CRC Handbook of Computer Science and Engineering. — 2nd. — CRC Press, 2004. — ISBN 158488360X.
• John C. Mitchell, Gordon Plotkin. Abstract [data types have existential type] // ACM Transactions on Programming Languages and Systems. — 1988. — Т. 10, № 3. — С. 470–502.
• Tratt, Laurence. Dynamically Typed Languages. — Advances in Computers, 2009. — С. 149–184.
• Gonzalez, T.; Diaz-Herrera, J.; Tucker, A. Type Systems (by Stephania Weirich) // Computing Handbook, Third Edition: Computer Science and Software Engineering. — CRC Press, 2015. — 2326 p. — ISBN 9781439898536.

• Smith, Chris. What To Know Before Debating Type Systems.
• Erik Meijer, Peter Drayton. Static Typing Where Possible, Dynamic Typing When Needed: The End of the Cold War Between Programming Languages (англ.). Microsoft Corporation.
• Ликбез по типизации в языках программирования (рус.)