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

Определение

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

Описание

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

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

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

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

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

Формальное обоснование

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

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

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

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.

— Марк Мэнесси

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

Проверка согласования типов

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

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

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

Динамическая проверка типов и информация о типах

Строгий и нестрогий контроль типов

Типобезопасность и защита адресации памяти

Типизированные и бестиповые языки

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

Особый случай типизированных языков представляют однотиповые языки ( англ. single-type language ), то есть языки с единственным типом. Обычно это языки сценариев или разметки , такие как 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 , то 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 году . Теория представляет собой типизированное лямбда-исчисление второго порядка, аналогичное Системе F , но с экзистенциальной квантификацией вместо универсальной .

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

Явное и неявное назначение типов

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

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

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

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

Унифицированные системы типов

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

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

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

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

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

Влияние на стиль программирования

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

См. также

• Ковариантность и контравариантность (программирование)
• Полиморфизм
• Перегрузка операторов

Примечания

Литература

• Luca Cardelli, Peter Wegner. . — , 1985. — С. 471—523 . — ISSN .
• Benjamin C. Pierce. Types and Programming Languages. — MIT Press, 2002. — ISBN 978-0-262-16209-8 .
• Luca Cardelli. . — 2nd. — CRC Press, 2004. — ISBN 158488360X .
• John C. Mitchell, Gordon Plotkin. types have existential type] // ACM Transactions on Programming Languages and Systems. — 1988. — Т. 10 , № 3 . — С. 470–502 .
• Tratt, Laurence. . — 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. .
• Erik Meijer, Peter Drayton. (англ.) . Microsoft Corporation.
• (рус.)