Русская Википедия:Система типов
Шаблон:About Шаблон:Типизация данных Система типов — совокупность правил в языках программирования, назначающих свойства, именуемые типами, различным конструкциям, составляющим программу — таким как переменные, выражения, функции или модули. Основная роль системы типов заключается в уменьшении числа багов в программахШаблон:Sfn посредством определения интерфейсов между различными частями программы и последующей проверки согласованности взаимодействия этих частей. Эта проверка может происходить статически (Шаблон:Iw) или динамически (во время выполнения), а также быть комбинацией обоих видов.
Определение
По Шаблон:Iw, система типов — разрешимый синтаксический метод доказательства отсутствия определённых поведений программы путём классификации конструкций в соответствии с видами вычисляемых значенийШаблон:Sfn.
Описание
Пример простой системы типов можно видеть в языке Си. Части программы на Си оформляются в виде определений функций. Функции вызывают друг друга. Интерфейс функции задаёт имя функции и список значений, которые передаются её телу. Вызывающая функция постулирует имя функции, которую хочет вызвать, и имена переменных, хранящих значения, которые требуется передать. Во время исполнения программы значения помещаются во временное хранилище, и затем исполнение передаётся в тело вызываемой функции. Код вызываемой функции осуществляет доступ к значениям и использует их. Если инструкции в теле функции написаны в предположении, что им на обработку должно быть передано целое значение, но вызывающий код передал число с плавающей точкой, то вызванная функция вычислит неверный результат. Компилятор Си проверяет типы, заданные для каждой переданной переменной, в отношении к типам, заданным для каждой переменной в интерфейсе вызываемой функции. Если типы не совпадают, компилятор порождает ошибку времени компиляции.
Технически, система типов назначает тип каждому вычисленному значению и затем, отслеживая последовательность этих вычислений, предпринимает попытку проверить или доказать отсутствие ошибок согласования типов. Конкретная система типов может определять, что именно приводит к ошибке, но обычно целью является предотвращение того, чтобы операции, предполагающие определённые свойства своих параметров, получали параметры, для которых эти операции не имеют смысла — предотвращение логических ошибок. Дополнительно это также предотвращает ошибки адресации памяти.
Системы типов обычно определяются как часть языков программирования и встраиваются в их интерпретаторы и компиляторы. Однако система типов языка может быть расширена посредством Шаблон:Iw, осуществляющих дополнительные проверки на основе исходного синтаксиса типизации в языке.
Компилятор также может использовать статический тип значения для оптимизации хранилища и для выбора алгоритмической реализации операций над этим значением. Например, во многих компиляторах Си тип float представляется 32 битами, в соответствии со спецификацией IEEE для операций с плавающей точкой одинарной точности. На основании этого будет использоваться специальный набор инструкций микропроцессора для значений этого типа (сложение, умножение и другие операции).
Количество налагаемых на типы ограничений и способ их вычисления определяют типизацию языка. Помимо этого, в случае полиморфизма типов, язык может также задать для каждого типа операцию варьирования конкретных алгоритмов. Изучением систем типов занимается теория типов, хотя на практике конкретная система типов языка программирования основывается на особенностях архитектуры компьютера, реализации компилятора и общем образе языка.
Формальное обоснование
Формальным обоснованием для систем типов служит теория типов. В состав языка программирования включается система типов для осуществления проверки типов Шаблон:Iw или во время выполнения, требующая явного провозглашения типов или выводящая их самостоятельно. Марк Мэнесси (Шаблон:Lang-en) сформулировал проблему такШаблон:Sfn: Шаблон:Начало цитатыОсновная проблема, решаемая теорией типов, состоит в том, чтобы убедиться, что программы являются осмысленными. Основная проблема, порождаемая теорией типов, состоит в том, что осмысленные программы могут не соответствовать поведению, ожидаемому от них по замыслу. Следствием этой напряжённости является поиск более мощных систем типов.Шаблон:OqШаблон:Конец цитаты
Операция назначения типа, называемая типизацией, придаёт смысл цепочкам бит, таким как значение в памяти компьютера, или объектам, таким как переменная. Компьютер не имеет возможности отличить, к примеру, адрес в памяти от инструкции кода, или символ от целого числа или числа с плавающей запятой, поскольку цепочки бит, представляющие эти различные по смыслу значения, не имеют каких-либо явных особенностей, позволяющих делать предположения об их смысле. Назначение цепочкам бит типа предоставляет это осмысление, превращая тем самым программируемое аппаратное обеспечение в символьную систему, состоящую из этого аппаратного обеспечения и программы.
Проверка согласования типов
Процесс проверки и установления ограничений для типов — контроль типов или проверка соответствия типов — может осуществляться как Шаблон:Iw (статическая типизация), так и во время выполнения (динамическая типизация). Возможны и промежуточные решения (ср. Последовательная типизация).
Если спецификация языка требует, чтобы правила типизации исполнялись строго (то есть допуская в той или иной мере лишь те автоматические преобразования типов, которые не теряют информацию), такой язык называется сильно типизированным (Шаблон:Lang-en; в русской литературе преобладает вариант перевода строго типизированным), в противном случае — слабо типизированным. Эти термины являются условными и не используются в формальных обоснованиях.
Статическая проверка типов
Динамическая проверка типов и информация о типах
Строгий и нестрогий контроль типов
Типобезопасность и защита адресации памяти
Типизированные и бестиповые языки
Язык называют типизированным, если спецификация каждой операции определяет типы данных, к которым эта операция может применяться, подразумевая её неприменимость к иным типам[1]. Например, данные, которые представляет «этот текст в кавычках», имеют тип «строка». В большинстве языков программирования деление числа на строку не имеет смысла, и большинство современных языков отвергнет программу, которая пытается выполнить такую операцию. В одних языках бессмысленная операция будет выявлена Шаблон:Iw (статическая типизация), и отвергнута компилятором. В других она будет выявлена во время выполнения программы (динамическая типизация), порождая исключительную ситуацию.
Особый случай типизированных языков представляют однотиповые языки (Шаблон:Lang-en), то есть языки с единственным типом. Обычно это языки сценариев или разметки, такие как REXX и SGML, единственным типом данных в которых является символьная строка, используемая для представления как символьных, так и числовых данных.
Бестиповые языки, в противоположность типизированным, позволяют осуществлять любую операцию над любыми данными, которые в них представляются цепочками бит произвольной длины[1]. Бестиповыми является большинство языков ассемблера. Примерами высокоуровневых бестиповых языков служат BCPL, Шаблон:Iw, Forth, Рефал.
На практике, лишь некоторые языки могут считаться типизированными с точки зрения теории типов (разрешая или отвергая все операции), большинство современных языков предлагают лишь некую степень типизированности[1]. Многие промышленные языки предоставляют возможность обойти или нарушить систему типов, поступаясь типобезопасностью ради более точного контроля над исполнением программы (каламбур типизации).
Типы и полиморфизм
Шаблон:Main Термин «полиморфизм» означает способность кода выполняться над значениями множества разных типов, или возможность разных экземпляров одной и той же структуры данных содержать элементы разных типов. Некоторые системы типов допускают полиморфизм для потенциального повышения коэффициента повторного использования кода: в языках с полиморфизмом программистам достаточно реализовать структуры данных, такие как список или ассоциативный массив, лишь единожды, и не требуется разрабатывать по одной реализации для каждого типа элементов, которые планируется хранить в этих структурах. По этой причине некоторые учёные в области информатики иногда называют использование определённых форм полиморфизма «обобщённым программированием». Обоснования полиморфизма с точки зрения теории типов практически те же, что и для абстракции, модульности и в ряде случаев Шаблон:Iw.
Утиная типизация
Специальные системы типов
Ряд специальных систем типов был разработан для использования в определённых условиях с определёнными данными, а также для статического анализа программ. В большинстве своём они основываются на идеях формальной теории типов и используются лишь в составе исследовательских систем.
Экзистенциальные типы
Экзистенциальные типы, то есть типы, определённые посредством экзистенциального квантификатора (квантора существования), представляют собой механизм инкапсуляции на уровне типов: это композитный тип, скрывающий реализацию некоего типа в своём составе.
Понятие экзистенциального типа часто используется совместно с понятием типа записи для представления модулей и абстрактных типов данных, что обусловлено их назначением — отделением реализации от интерфейса. Например, тип 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 годуШаблон:Sfn. Теория представляет собой типизированное лямбда-исчисление второго порядка, аналогичное Системе F, но с экзистенциальной квантификацией вместо универсальной.
Экзистенциальные типы явным образом доступны в качестве экспериментального расширения языка Haskell, где они представляют собой специальный синтаксис, позволяющий использовать переменную типа в определении алгебраического типа, не вынося её в сигнатуру конструктора типов, то есть не повышая его арность[2]. Язык Java предоставляет ограниченную форму экзистенциальных типов посредством Шаблон:Iw. В языках, реализующих классический let-полиморфизм в стиле ML, экзистенциальные типы могут быть симулированы посредством так называемых «значений, индексированных типами»[3].
Явное и неявное назначение типов
Шаблон:Main Многие статические системы типов, например, такие как в языках Си и Java, требуют провозглашения типа: программист должен явно назначать каждой переменной конкретный тип. Другие, такие как система типов Хиндли — Милнера, применяемая в языках ML и Haskell, осуществляют выведение типов: компилятор выстраивает заключение о типах переменных на основании того, как программист использует эти переменные.
Например, для функции f(x,y), осуществляющей сложение x и y, компилятор может сделать вывод, что x и y должны быть числами — поскольку операция сложения определена только для чисел. Следовательно, вызов где-либо в программе функции f для параметров, отличных от числовых, (например, для строки или списка) сигнализирует об ошибке.
Числовые и строковые константы и выражения обычно зачастую выражают тип в конкретном контексте. Например, выражение 3.14 может подразумевать вещественное число, тогда как [1,2,3] может быть списком целых — обычно массивом.
Вообще говоря, выведение типов возможно, если оно принципиально разрешимо в теории типов. Более того, даже если выведение неразрешимо для данной теории типов, выведение зачастую возможно для многих реальных программ. Система типов языка Haskell, являющаяся разновидностью системы типов Хиндли — Милнера, представляет собой ограничение Шаблон:Iw для так называемых полиморфных типов первого ранга, на которых выведение разрешимо. Многие компиляторы Хаскела предоставляют полиморфизм произвольного ранга в качестве расширения, но это делает выведение типов неразрешимым, так что требуется явное провозглашение типов. Однако, проверка согласования типов остаётся разрешимой и для программ с полиморфизмом первого ранга типы по-прежнему выводимы.
Унифицированные системы типов
Некоторые языки, например, C#, имеют унифицированную систему типов[4]. Это означает, что все типы языка вплоть до примитивных наследуются от единого корневого объекта (в случае с C# — от класса Object). В Java есть несколько примитивных типов, не являющихся объектами. Наряду с ними Java также предоставляет обёрточные объектные типы, так что разработчик может использовать примитивные или объектные типы по своему усмотрению.
Совместимость типов
Механизм проверки согласования типов в языке со статической типизацией проверяет, что всякое выражение соответствует типу, ожидаемому тем контекстом, в котором оно присутствует. Например, в операторе присваивания вида x := e выведенный для выражения e тип должен соответствовать типу, который провозглашён или выведен для переменной x. Нотация соответствия, называемая совместимостью, специфична для каждого языка.
Если e и x имеют единый тип, и присваивание разрешено для этого типа, то это выражение является корректным. Поэтому в простейших системах типов вопрос совместимости двух типов упрощается до вопроса их равенства (эквивалентности). Однако разные языки имеют разные критерии для определения совместимости типов двух выражений. Эти теории эквивалентности варьируются между двумя крайними случаями: Шаблон:Нп2, в которых два типа эквивалентны, если описывают одинаковую внутреннюю структуру значения; и Шаблон:Нп2, в которых синтаксически различные типы никогда не эквивалентны (то есть два типа равны только в том случае, если равны их идентификаторы).
В языках с Шаблон:Iw правила совместимости более сложные. Например, если A является подтипом B, то значение, принадлежащее типу A, может быть использовано в контексте, ожидающем значение типа B, даже если обратное неверно. Как и в случае эквивалентности, отношения подтипов различаются в разных языках, и здесь возможно много вариантов правил. Наличие в языке параметрического или ситуативного полиморфизма может также влиять на совместимость типов.
Влияние на стиль программирования
Одни программисты предпочитают статические системы типов, другие — динамические. Статически типизированные языки сигнализируют об ошибках согласования типов на Шаблон:Iw, могут порождать более эффективно исполняемый код, и для таких языков осуществимо более релевантное автодополнение в интегрированных средах разработки. Сторонники динамической типизации утверждают, что они лучше подходят для быстрого прототипирования, и что ошибки согласования типов составляют лишь малую часть возможных ошибок в программахШаблон:Sfn[5]. С другой стороны, в статически типизированных языках явная декларация типов обычно не требуется, если язык поддерживает вывод типов, а некоторые динамически типизированные языки производят оптимизацию на этапе выполнения программы[6][7], зачастую посредством применения частичного вывода типов[8].
См. также
- Сравнение систем типов
- Ковариантность и контравариантность (программирование)
- Полиморфизм
- Перегрузка операторов
- Шаблон:Iw
- Шаблон:Iw
- Шаблон:Iw
Примечания
Литература
Ссылки
Шаблон:Wikibooks Шаблон:Wikibooks
- ↑ 1,0 1,1 1,2 Шаблон:Cite web
- ↑ Шаблон:Cite web
- ↑ Шаблон:Cite web
- ↑ Standard ECMA-334 Шаблон:Wayback, 8.2.4 Type system unification.
- ↑ Шаблон:Cite web
- ↑ Шаблон:Cite web
- ↑ Шаблон:Cite web
- ↑ C-Extensions for Python Шаблон:Wayback. Cython (2013-05-11). Retrieved on 2013-07-17
