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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск
Типизация данных

Типобезопасность
Вывод типов
Статическая типизация
Динамическая типизация
Сильная и слабая типизация
Зависимые типы
Утиная типизация

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

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

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

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

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

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

Формальное обоснование[править | править вики-текст]

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

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

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

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


Проверка согласования типов[править | править вики-текст]

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


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

Динамическая проверка типов и информация о типах[править | править вики-текст]

Строгий и нестрогий контроль типов[править | править вики-текст]

Типобезопасность и защита адресации памяти[править | править вики-текст]

Типизированные и бестиповые языки[править | править вики-текст]

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

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

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

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

Типы и полиморфизм[править | править вики-текст]

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

Утиная типизация[править | править вики-текст]

Специальные системы типов[править | править вики-текст]

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


Экзистенциальные типы[править | править вики-текст]

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

Понятие экзистенциального типа часто используется совместно с понятием типа записи для представления модулей и абстрактных типов данных, что обусловлено их назначением — отделением реализации от интерфейса. Например, тип 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 предоставляет ограниченную форму экзистенциальных типов посредством джокера[en]. В языках, реализующих классический let-полиморфизм в стиле ML, экзистенциальные типы могут быть симулированы посредством так называемых «значений, индексированных типами»[7].

Явное и неявное назначение типов[править | править вики-текст]

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

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

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

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

Унифицированные системы типов[править | править вики-текст]

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

Совместимость типов[править | править вики-текст]

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

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

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

Влияние на стиль программирования[править | править вики-текст]

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

См.также[править | править вики-текст]

Примечания[править | править вики-текст]

  1. Pierce, 2002, p. 1
  2. Cardelli, 2004, p. 1
  3. 1 2 Pierce, 2002, с. 208
  4. 1 2 3 Andrew Cooke. Introduction To Computer Languages. Проверено 13 июля 2012.
  5. John C. Mitchell, Gordon Plotkin Abstract [data types have existential type] // ACM Transactions on Programming Languages and Systems. — 1988. — Т. 10. — № 3. — С. 470–502.
  6. Existential types on HaskellWiki
  7. Type-Indexed Values
  8. Standard ECMA-334, 8.2.4 Type system unification.
  9. Erik Meijer, Peter Drayton. Static Typing Where Possible, Dynamic Typing When Needed: The End of the Cold War Between Programming Languages (англ.). Microsoft Corporation.
  10. Amanda Laucher, Paul Snively. Types vs Tests (англ.). InfoQ.
  11. Adobe and Mozilla Foundation to Open Source Flash Player Scripting Engine.
  12. Psyco, a Python specializing compiler.
  13. C-Extensions for Python. Cython (2013-05-11). Retrieved on 2013-07-17

Ссылки[править | править вики-текст]

Литература[править | править вики-текст]