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

редактировать
Эта статья о системах типов с точки зрения компьютерного программирования. Для теоретической переформулировки см. Теория типов.
Системы типов
Общие понятия
Основные категории
Второстепенные категории

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

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

СОДЕРЖАНИЕ

  • 1 Обзор использования
  • 2 Основы
    • 2.1 Типовые ошибки
  • 3 Проверка типа
    • 3.1 Статическая проверка типа
    • 3.2 Динамическая проверка типов и информация о типах среды выполнения
    • 3.3 Сочетание статической и динамической проверки типов
    • 3.4 Статическая и динамическая проверка типов на практике
    • 3.5 Системы сильного и слабого типов
    • 3.6 Безопасность типов и безопасность памяти
    • 3.7 Переменные уровни проверки типа
    • 3.8 Системы опционального типа
  • 4 Полиморфизм и типы
  • 5 Системы специализированного типа
    • 5.1 Зависимые типы
    • 5.2 Линейные типы
    • 5.3 Типы перекрестков
    • 5.4 Типы союзов
    • 5.5 Экзистенциальные типы
    • 5.6 Постепенный набор текста
  • 6 Явное или неявное объявление и вывод
  • 7 Проблемы с решением
  • 8 Единая система типов
  • 9 Совместимость: эквивалентность и подтипы
  • 10 См. Также
  • 11 Примечания
  • 12 Ссылки
  • 13 Дальнейшее чтение
  • 14 Внешние ссылки

Обзор использования

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

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

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

Основы

Формально теория типов изучает системы типов. Язык программирования должен иметь возможность проверки типа с использованием системы типов, будь то во время компиляции или во время выполнения, с аннотациями вручную или с автоматическим выводом. Как кратко выразился Марк Манассе :

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

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

Программа связывает каждое значение по крайней мере с одним конкретным типом, но также может случиться так, что одно значение связано со многими подтипами. Другие сущности, такие как объекты, модули, каналы связи и зависимости, могут быть связаны с типом. Даже тип может быть связан с типом. Реализация системы типов теоретически может связывать идентификации, называемые типом данных (тип значения), классом (типом объекта) и типом ( типом типа или метатипом). Это абстракции, через которые может проходить типизация в иерархии уровней, содержащихся в системе.

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

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

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

Независимо от того, автоматизировано ли это компилятором или указано программистом, система типов делает поведение программы незаконным, если оно выходит за рамки правил системы типов. Преимущества, предоставляемые системами типов, заданными программистом, включают:

  • Абстракция (или модульность) - типы позволяют программистам думать на более высоком уровне, чем бит или байт, не беспокоясь о низкоуровневой реализации. Например, программисты могут начать думать о строке как о наборе символьных значений, а не как о простом массиве байтов. Более того, типы позволяют программистам обдумывать и выражать интерфейсы между двумя подсистемами любого размера. Это обеспечивает больше уровней локализации, так что определения, необходимые для взаимодействия подсистем, остаются согласованными, когда эти две подсистемы обмениваются данными.
  • Документация. В более выразительных системах типов типы могут служить формой документации, разъясняющей намерения программиста. Например, если программист объявляет функцию как возвращающую тип отметки времени, это документирует функцию, когда тип отметки времени может быть явно объявлен глубже в коде как целочисленный тип.

Преимущества, предоставляемые системами типов, определяемыми компилятором, включают:

  • Оптимизация. Статическая проверка типов может предоставить полезную информацию во время компиляции. Например, если для типа требуется, чтобы значение в памяти было выровнено с точностью, кратной четырем байтам, компилятор может использовать более эффективные машинные инструкции.
  • Безопасность - система типов позволяет компилятору обнаруживать бессмысленный или недопустимый код. Например, мы можем идентифицировать выражение 3 / "Hello, World"как недопустимое, если в правилах не указано, как делить целое число на строку. Строгая типизация обеспечивает большую безопасность, но не может гарантировать полную безопасность типов.

Ошибки типа

Ошибка типа - это непреднамеренное состояние, которое может проявляться на нескольких этапах разработки программы. Таким образом, в системе типов требуется средство обнаружения ошибки. В некоторых языках, таких как Haskell, для которых определение типа автоматизировано, компилятор может получить доступ к lint, чтобы помочь в обнаружении ошибки.

Безопасность типов способствует правильности программы, но может гарантировать правильность только за счет того, что сама проверка типов становится неразрешимой проблемой. В системе типов с автоматической проверкой типов программа может работать некорректно, но при этом не вызывать ошибок компилятора. Деление на ноль - небезопасная и неправильная операция, но средство проверки типов, работающее только во время компиляции, не сканирует деление на ноль на большинстве языков, и тогда это остается как ошибка времени выполнения. Чтобы доказать отсутствие этих дефектов, широко используются другие виды формальных методов, в совокупности известные как программный анализ. В качестве альтернативы, достаточно выразительная система типов, например, в языках с зависимой типизацией, может предотвратить подобные ошибки (например, выражение типа ненулевых чисел). Кроме того, тестирование программного обеспечения - это эмпирический метод поиска ошибок, которые средство проверки типов не может обнаружить.

Проверка типа

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

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

Статическая проверка типов - это процесс проверки типовой безопасности программы на основе анализа текста программы ( исходного кода ). Если программа проходит проверку статического типа, то программа гарантированно удовлетворяет некоторому набору свойств безопасности типов для всех возможных входных данных.

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

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

if lt;complex testgt; then lt;do somethinggt; else lt;signal that there is a type errorgt;

Даже если выражение lt;complex testgt;всегда оценивается trueво время выполнения, большинство средств проверки типов отклонят программу как некорректно типизированную, потому что для статического анализатора трудно (если не невозможно) определить, что elseветвление не будет выполнено. Следовательно, средство проверки статического типа быстро обнаружит ошибки типа в редко используемых путях кода. Без проверки статического типа даже тесты покрытия кода со 100% покрытием могут не найти такие ошибки типа. Тесты могут не обнаружить такие ошибки типа, потому что необходимо учитывать комбинацию всех мест, где создаются значения, и всех мест, где используется определенное значение.

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

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

Список языков с проверкой статического типа см. В категории языков со статической типизацией.

Проверка динамического типа и информация о типе среды выполнения

См. Также: Динамический язык программирования и Интерпретируемый язык.

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

Большинство языков с типобезопасностью включают в себя некоторую форму проверки динамического типа, даже если в них также есть средство проверки статического типа. Причина этого в том, что многие полезные функции или свойства трудно или невозможно проверить статически. Например, предположим, что программа определяет два типа, A и B, где B является подтипом A. Если программа пытается преобразовать значение типа A в тип B, что называется понижающим преобразованием, тогда операция допустима только если преобразуемое значение на самом деле является значением типа B. Таким образом, необходима динамическая проверка, чтобы убедиться, что операция безопасна. Это требование является одним из критических замечаний по поводу понижения.

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

Языки программирования, которые включают проверку динамического типа, но не проверку статического типа, часто называют «языками программирования с динамической типизацией». Список таких языков см. В категории языков программирования с динамической типизацией.

Сочетание статической и динамической проверки типов

Некоторые языки допускают как статическую, так и динамическую типизацию. Например, Java и некоторые другие якобы статически типизированные языки поддерживают приведение типов к их подтипам, запросы объекта для обнаружения его динамического типа и другие операции с типами, которые зависят от информации о типе среды выполнения. Другой пример - C ++ RTTI. В более общем смысле, большинство языков программирования включают механизмы для диспетчеризации различных «типов» данных, таких как непересекающиеся объединения, полиморфизм времени выполнения и вариантные типы. Даже если они не взаимодействуют с аннотациями типов или проверкой типов, такие механизмы по существу аналогичны реализациям динамической типизации. См. Язык программирования для более подробного обсуждения взаимодействия между статической и динамической типизацией.

К объектам в объектно-ориентированных языках обычно обращаются по ссылке, статический целевой тип (или тип манифеста) которой равен либо типу времени выполнения объекта (его скрытому типу), либо его супертипу. Это соответствует принципу подстановки Лискова, который гласит, что все операции, выполняемые с экземпляром данного типа, также могут выполняться с экземпляром подтипа. Эта концепция также известна как подчинение или полиморфизм подтипа. В некоторых языках подтипы также могут иметь ковариантные или контравариантные возвращаемые типы и типы аргументов соответственно.

Некоторые языки, например Clojure, Common Lisp или Cython, по умолчанию проверяются динамически, но позволяют программам выбирать статическую проверку типа, предоставляя дополнительные аннотации. Одна из причин использования таких подсказок - это оптимизация производительности критических разделов программы. Это формализуется постепенным набором текста. Программная среда DrRacket, педагогическая среда, основанная на Lisp и предшественник языка Racket, также имеет мягкую типизацию.

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

В Русте, то тип обеспечивает динамическое типирование типов. std::any'static

Проверка статических и динамических типов на практике

Выбор между статической и динамической типизацией требует определенных компромиссов.

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

Статическая типизация обычно приводит к более быстрому выполнению скомпилированного кода. Когда компилятор знает, какие именно типы данных используются (что необходимо для статической проверки, посредством объявления или вывода), он может создать оптимизированный машинный код. Некоторые языки с динамической типизацией, такие как Common Lisp, по этой причине допускают необязательные объявления типов для оптимизации.

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

Языки со статической типизацией, в которых отсутствует вывод типов (например, C и Java до версии 10 ), требуют, чтобы программисты объявляли типы, которые должен использовать метод или функция. Это может служить добавленной программной документацией, которая является активной и динамической, а не статической. Это позволяет компилятору предотвратить его отклонение от синхронности и игнорирование программистами. Однако язык может быть статически типизирован без объявления типов (примеры включают Haskell, Scala, OCaml, F # и, в меньшей степени, C # и C ++ ), поэтому явное объявление типа не является обязательным требованием для статической типизации на всех языках.

Динамическая типизация допускает конструкции, которые некоторые (простые) проверки статического типа могут отклонить как недопустимые. Например, становятся возможными функции eval, которые выполняют произвольные данные как код. Eval функция возможна при статической типизации, но требует передовых использования алгебраических типов данных. Кроме того, динамическая типизация лучше приспособлена к переходному коду и созданию прототипов, например, позволяя прозрачно использовать структуру данных заполнителя ( фиктивный объект ) вместо полной структуры данных (обычно для целей экспериментов и тестирования).

Динамическая типизация обычно позволяет набирать текст «уткой» (что упрощает повторное использование кода ). Многие языки со статической типизацией также имеют утиную типизацию или другие механизмы, такие как универсальное программирование, которые также упрощают повторное использование кода.

Динамическая типизация обычно упрощает использование метапрограммирования. Например, шаблоны C ++ обычно сложнее писать, чем эквивалентный код Ruby или Python, поскольку в C ++ есть более строгие правила в отношении определений типов (как для функций, так и для переменных). Это вынуждает разработчика писать больше стандартного кода для шаблона, чем разработчику Python. Более сложные конструкции времени выполнения, такие как метаклассы и интроспекция, часто труднее использовать в языках со статической типизацией. В некоторых языках такие функции также могут использоваться, например, для генерации новых типов и поведения на лету на основе данных времени выполнения. Такие продвинутые конструкции часто предоставляются динамическими языками программирования ; многие из них имеют динамическую типизацию, хотя динамическая типизация не обязательно связана с динамическими языками программирования.

Системы сильного и слабого типов

Основная статья: Сильная и слабая типизация

Языки часто в просторечии называют строго или слабо типизированными. Фактически не существует общепринятого определения того, что означают эти термины. В общем, существуют более точные термины для обозначения различий между системами типов, которые заставляют людей называть их «сильными» или «слабыми».

Безопасность типов и безопасность памяти

Основная статья: Безопасность типов

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

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

Рассмотрим следующую программу на языке, который является безопасным как для типов, так и для памяти:

var x := 5; var y := "37"; var z := x + y;

В этом примере переменная zбудет иметь значение 42. Хотя это может быть не тем, что ожидал программист, это вполне определенный результат. Если бы yбыла другая строка, которую нельзя было преобразовать в число (например, «Hello World»), результат также был бы четко определен. Обратите внимание, что программа может быть безопасной по типу или с памятью и по-прежнему давать сбой при недопустимой операции. Это для языков, в которых система типов недостаточно развита для точного определения допустимости операций для всех возможных операндов. Но если программа встречает операцию, которая не является типобезопасной, завершение программы часто является единственным вариантом.

Теперь рассмотрим аналогичный пример на C:

int x = 5; char y[] = "37"; char* z = x + y; printf("%c\n", *z);

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

В общем, безопасность типов и безопасность памяти идут рука об руку. Например, язык, поддерживающий арифметику указателя и преобразование числа в указатель (например, C), не является ни безопасным для памяти, ни типобезопасным, поскольку он позволяет обращаться к произвольной памяти, как если бы это была действительная память любого типа.

Для получения дополнительной информации см. Безопасность памяти.

Переменные уровни проверки типов

Некоторые языки позволяют применять разные уровни проверки к разным областям кода. Примеры включают:

  • use strictДиректива в JavaScript и Perl применяет сильную проверку.
  • declare(strict_types=1)В PHP на основе каждого файла позволяет только переменная точного типа объявления типа будут приняты, или TypeErrorбудут выброшены.
  • Option Strict OnВ VB.NET позволяет компилятору требуется преобразование между объектами.

Дополнительные инструменты, такие как lint и IBM Rational Purify, также могут использоваться для достижения более высокого уровня строгости.

Системы опционального типа

Было предложено, главным образом Гиладом Браха, сделать выбор системы типов независимым от выбора языка; что система типов должна быть модулем, который можно подключить к языку по мере необходимости. Он считает, что это выгодно, потому что то, что он называет обязательными системами типов, делает языки менее выразительными, а код - более хрупким. Требование, чтобы система типов не влияла на семантику языка, выполнить сложно.

Необязательный набор текста связан с постепенным набором текста, но отличается от него. В то время как обе дисциплины типизации могут использоваться для выполнения статического анализа кода ( статическая типизация ), дополнительные системы типов не обеспечивают безопасность типов во время выполнения ( динамическая типизация ).

Полиморфизм и типы

Основная статья: Полиморфизм (информатика)

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

Системы специализированного типа

Было создано множество систем типов, которые предназначены для использования в определенных средах с определенными типами данных или для внеполосного статического анализа программ. Часто они основаны на идеях формальной теории типов и доступны только как часть прототипных исследовательских систем.

В следующей таблице представлен обзор теоретических концепций типов, которые используются в специализированных системах типов. Имена M, N, O включают термины, а имена - типы. Обозначение (соответственно) описывает тип, который является результатом замены всех вхождений типовой переменной α (соответственно термопеременной x) в τ типом σ (соответственно терм N). σ , τ {\ displaystyle \ sigma, \ tau} τ [ α знак равно σ ] {\ Displaystyle \ тау [\ альфа: = \ сигма]} τ [ Икс знак равно N ] {\ Displaystyle \ тау [х: = N]}

Понятие типа Обозначение Имея в виду
Функция σ τ {\ displaystyle \ sigma \ to \ tau} Если M имеет тип, а N - тип σ, то приложение имеет тип τ. σ τ {\ displaystyle \ sigma \ to \ tau} M ( N ) {\ Displaystyle M (N)}
Продукт σ × τ {\ displaystyle \ sigma \ times \ tau} Если M имеет тип, то это пара такая, что N имеет тип σ, а O имеет тип τ. σ × τ {\ displaystyle \ sigma \ times \ tau} M знак равно ( N , О ) {\ Displaystyle M = (N, O)}
Сумма σ + τ {\ displaystyle \ sigma + \ tau} Если M имеет тип, то либо это первое внедрение, такое что N имеет тип σ, либо σ + τ {\ displaystyle \ sigma + \ tau} M знак равно ι 1 ( N ) {\ Displaystyle M = \ iota _ {1} (N)}

M знак равно ι 2 ( N ) {\ Displaystyle M = \ iota _ {2} (N)}- вторая инъекция такая, что N имеет тип τ.

Пересечение σ τ {\ displaystyle \ sigma \ cap \ tau} Если M имеет тип, то M имеет тип σ, а M имеет тип τ. σ τ {\ displaystyle \ sigma \ cap \ tau}
Союз σ τ {\ Displaystyle \ сигма \ чашка \ тау} Если M имеет тип, то M имеет тип σ или M имеет тип τ. σ τ {\ Displaystyle \ сигма \ чашка \ тау}
Записывать Икс : τ {\ Displaystyle \ langle х: \ тау \ rangle} Если M имеет тип, то M имеет член x, имеющий тип τ. Икс : τ {\ Displaystyle \ langle х: \ тау \ rangle}
Полиморфный α . τ {\ Displaystyle \ forall \ alpha. \ tau} Если M имеет тип, то M имеет тип для любого типа σ. α . τ {\ Displaystyle \ forall \ alpha. \ tau} τ [ α знак равно σ ] {\ Displaystyle \ тау [\ альфа: = \ сигма]}
Экзистенциальный α . τ {\ Displaystyle \ существует \ альфа. \ тау} Если M имеет тип, то M имеет тип для некоторого типа σ. α . τ {\ Displaystyle \ существует \ альфа. \ тау} τ [ α знак равно σ ] {\ Displaystyle \ тау [\ альфа: = \ сигма]}
Рекурсивный μ α . τ {\ Displaystyle \ му \ альфа. \ тау} Если M имеет тип, то M имеет тип. μ α . τ {\ Displaystyle \ му \ альфа. \ тау} τ [ α знак равно μ α . τ ] {\ Displaystyle \ тау [\ альфа: = \ му \ альфа. \ тау]}
Зависимая функция ( Икс : σ ) τ {\ Displaystyle (х: \ сигма) \ к \ тау} Если M имеет тип, а N - тип σ, тогда приложение имеет тип. ( Икс : σ ) τ {\ Displaystyle (х: \ сигма) \ к \ тау} M ( N ) {\ Displaystyle M (N)} τ [ Икс знак равно N ] {\ Displaystyle \ тау [х: = N]}
Зависимый продукт ( Икс : σ ) × τ {\ Displaystyle (х: \ сигма) \ раз \ тау} Если M имеет тип, то это пара такая, что N имеет тип σ, а O имеет тип. ( Икс : σ ) × τ {\ Displaystyle (х: \ сигма) \ раз \ тау} M знак равно ( N , О ) {\ Displaystyle M = (N, O)} τ [ Икс знак равно N ] {\ Displaystyle \ тау [х: = N]}
Зависимый перекресток ( Икс : σ ) τ {\ Displaystyle (х: \ сигма) \ кепка \ тау} Если M имеет тип, то M имеет тип σ, а M имеет тип. ( Икс : σ ) τ {\ Displaystyle (х: \ сигма) \ кепка \ тау} τ [ Икс знак равно M ] {\ Displaystyle \ тау [х: = М]}
Семейное пересечение Икс : σ τ {\ displaystyle \ bigcap _ {x: \ sigma} \ tau} Если M имеет тип, то M имеет тип для любого терма N типа σ. Икс : σ τ {\ displaystyle \ bigcap _ {x: \ sigma} \ tau} τ [ Икс знак равно N ] {\ Displaystyle \ тау [х: = N]}
Семейный союз Икс : σ τ {\ displaystyle \ bigcup _ {x: \ sigma} \ tau} Если M имеет тип, то M имеет тип для некоторого терма N типа σ. Икс : σ τ {\ displaystyle \ bigcup _ {x: \ sigma} \ tau} τ [ Икс знак равно N ] {\ Displaystyle \ тау [х: = N]}

Зависимые типы

Основная статья: Зависимый тип

Зависимые типы основаны на идее использования скаляров или значений для более точного описания типа некоторого другого значения. Например, это может быть тип матрицы. Затем мы можем определить правила набора текста, такие как следующее правило умножения матриц: м а т р я Икс ( 3 , 3 ) {\ Displaystyle \ mathrm {матрица} (3,3)} 3 × 3 {\ displaystyle 3 \ times 3}

м а т р я Икс м ты л т я п л у : м а т р я Икс ( k , м ) × м а т р я Икс ( м , п ) м а т р я Икс ( k , п ) {\ displaystyle \ mathrm {matrix} _ {\ mathrm {multiply}}: \ mathrm {matrix} (k, m) \ times \ mathrm {matrix} (m, n) \ to \ mathrm {matrix} (k, n)}

где k, m, n - произвольные положительные целые числа. Вариант ML под названием Dependent ML был создан на основе этой системы типов, но поскольку проверка типов для обычных зависимых типов неразрешима, не все программы, использующие их, можно проверить без каких-либо ограничений. Зависимый ML ограничивает вид равенства, который он может решить, арифметикой Пресбургера.

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

Линейные типы

Основная статья: линейный тип

Линейные типы, основанные на теории линейной логики и тесно связанные с типами уникальности, представляют собой типы, присвоенные значениям, обладающим тем свойством, что они всегда имеют одну и только одну ссылку на них. Они полезны для описания больших неизменяемых значений, таких как файлы, строки и т. Д., Потому что любая операция, которая одновременно разрушает линейный объект и создает аналогичный объект (например, ' str= str + "a"'), может быть оптимизирована «под капотом» во входящий место мутации. Обычно это невозможно, поскольку такие мутации могут вызывать побочные эффекты в частях программы, содержащих другие ссылки на объект, нарушая ссылочную прозрачность. Они также используются в прототипе операционной системы Singularity для межпроцессного взаимодействия, статически гарантируя, что процессы не могут совместно использовать объекты в общей памяти, чтобы предотвратить состояние гонки. Чистый язык (а Haskell -как языка) использует эту систему типа для того, чтобы получить большую скорость ( по сравнению с выполнением глубокой копии), оставаясь при этом в безопасности.

Типы пересечений

Основная статья: Тип пересечения

Типы пересечения - это типы, описывающие значения, которые принадлежат обоим из двух других заданных типов с перекрывающимися наборами значений. Например, в большинстве реализаций C знаковый символ имеет диапазон от -128 до 127, а символ без знака имеет диапазон от 0 до 255, поэтому тип пересечения этих двух типов будет иметь диапазон от 0 до 127. Такой тип пересечения можно безопасно передать в функции, ожидая либо подписанных или неподписанных символов, поскольку он совместим с обоими типами.

Типы пересечения полезны для описания типов перегруженных функций: например, если « → » - это тип функций, принимающих целочисленный аргумент и возвращающих целое число, а « → » - это тип функций, принимающих аргумент с плавающей запятой и возвращающих значение с плавающей запятой, тогда пересечение этих двух типов можно использовать для описания функций, которые выполняют одно или другое, в зависимости от того, какой тип ввода они даны. Такую функцию можно безопасно передать другой функции, ожидающей выполнения функции « → »; он просто не использовал бы функцию « → ». intintfloatfloatintintfloatfloat

В иерархии подклассов наиболее производным типом является пересечение типа и типа-предка (например, его родительского). Пересечение родственных типов пусто.

Язык Форсайта включает общую реализацию типов пересечений. Ограниченная форма - это типы уточнения.

Типы союзов

Основная статья: Союзный тип

Типы объединения - это типы, описывающие значения, принадлежащие одному из двух типов. Например, в C знаковый char имеет диапазон от -128 до 127, а беззнаковый char - диапазон от 0 до 255, поэтому объединение этих двух типов будет иметь общий «виртуальный» диапазон от -128 до 255, который может использоваться частично в зависимости от того, к какому члену объединения осуществляется доступ. Любая функция, обрабатывающая этот тип объединения, должна иметь дело с целыми числами в этом полном диапазоне. В более общем смысле, единственные допустимые операции с типом объединения - это операции, которые действительны для обоих типов, которые объединяются. Концепция «объединения» в языке C аналогична типам объединения, но не является типобезопасной, поскольку разрешает операции, допустимые для любого типа, а не для обоих. Типы объединения важны при анализе программ, где они используются для представления символьных значений, точная природа которых (например, значение или тип) неизвестна.

В иерархии подклассов объединение типа и типа-предка (например, его родительского) является типом-предком. Объединение одноуровневых типов является подтипом их общего предка (то есть все операции, разрешенные для их общего предка, разрешены для типа объединения, но они также могут иметь другие допустимые общие операции).

Экзистенциальные типы

Основная статья: Экзистенциальный квантификатор

Экзистенциальные типы часто используются в связи с типами записей для представления модулей и абстрактных типов данных из-за их способности отделять реализацию от интерфейса. Например, тип «T = ∃X {a: X; f: (X → int);}» описывает интерфейс модуля, который имеет член данных с именем a типа X и функцию с именем f, которая принимает параметр того же типа X и возвращает целое число. Это можно было реализовать по-разному; Например:

  • intT = {a: int; е: (интервал → интервал); }
  • floatT = {a: float; f: (float → int); }

Оба эти типа являются подтипами более общего экзистенциального типа T и соответствуют конкретным типам реализации, поэтому любое значение одного из этих типов является значением типа T. Учитывая значение «t» типа «T», мы знаем, что « тс (тот)»хорошо напечатанный, независимо от того, что абстрактный типа X есть. Это дает гибкость для выбора типов, подходящих для конкретной реализации, в то время как клиенты, использующие только значения типа интерфейса - экзистенциального типа - изолированы от этих вариантов.

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

  • intT = {a: int; е: (интервал → интервал); } как ∃X {a: X; f: (X → int); }

Хотя абстрактные типы данных и модули были реализованы в языках программирования в течение некоторого времени, только в 1988 году Джон К. Митчелл и Гордон Плоткин создали формальную теорию под лозунгом: «Абстрактные типы [данных] имеют экзистенциальный тип». Теория представляет собой типизированное лямбда-исчисление второго порядка, подобное Системе F, но с экзистенциальной, а не универсальной квантификацией.

Постепенный набор текста

Основная статья: Постепенный набор текста

Постепенная типизация - это система типов, в которой переменным может быть назначен тип либо во время компиляции (что является статической типизацией), либо во время выполнения (что является динамической типизацией), что позволяет разработчикам программного обеспечения выбирать любую парадигму типа изнутри. единый язык. В частности, постепенная типизация использует специальный тип с именем dynamic для представления статически неизвестных типов, а постепенная типизация заменяет понятие равенства типов новым отношением, называемым согласованностью, которое связывает динамический тип с каждым другим типом. Отношение согласованности симметрично, но не транзитивно.

Явное или неявное объявление и вывод

Дополнительная информация: Вывод типа

Многие системы статических типов, такие как системы C и Java, требуют объявления типов: программист должен явно связать каждую переменную с определенным типом. Другие, такие как Haskell, выполняют вывод типа : компилятор делает выводы о типах переменных на основе того, как программисты используют эти переменные. Например, учитывая функцию, которая добавляет и вместе, компилятор может сделать вывод, что и должно быть числа-так как сложение определяется только для чисел. Таким образом, любой вызов в другом месте программы, который указывает нечисловой тип (например, строку или список) в качестве аргумента, будет сигнализировать об ошибке. f(x, y)xyxyf

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

Вывод типа в общем случае возможен, если он вычислим в рассматриваемой системе типов. Более того, даже если логический вывод в целом не вычислим для данной системы типов, логический вывод часто возможен для большого подмножества реальных программ. Система типов Хаскелла, версия Хиндли – Милнера, является ограничением Системы Fω так называемыми полиморфными типами ранга 1, в которых вывод типа вычислим. Большинство компиляторов Haskell допускают полиморфизм произвольного ранга в качестве расширения, но это делает вывод типа невычислимым. (Проверка типов, однако, разрешима, и программы ранга 1 по-прежнему имеют вывод типа; полиморфные программы более высокого ранга отклоняются, если не даны явные аннотации типа.)

Проблемы с решением

Основная статья: Теория типов § Проблемы принятия решений

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

  • Учитывая среду типа, термин и тип, решите, может ли термин быть назначен тип в среде типов. Γ {\ displaystyle \ Gamma} е {\ displaystyle e} τ {\ Displaystyle \ тау} е {\ displaystyle e} τ {\ Displaystyle \ тау}
  • Учитывая термин, решите, существует ли среда типов и тип, чтобы термину можно было присвоить тип в среде типов. е {\ displaystyle e} Γ {\ displaystyle \ Gamma} τ {\ Displaystyle \ тау} е {\ displaystyle e} τ {\ Displaystyle \ тау} Γ {\ displaystyle \ Gamma}
  • Учитывая типовое окружение и тип, решите, существует ли термин, которому можно присвоить тип в типовой среде. Γ {\ displaystyle \ Gamma} τ {\ Displaystyle \ тау} е {\ displaystyle e} τ {\ Displaystyle \ тау}

Единая система типов

Некоторые языки, такие как C # или Scala, имеют единую систему типов. Это означает, что все типы C #, включая примитивные типы, наследуются от одного корневого объекта. Каждый тип в C # наследуется от класса Object. Некоторые языки, такие как Java и Raku, имеют корневой тип, но также имеют примитивные типы, которые не являются объектами. Java предоставляет типы объектов-оболочек, которые существуют вместе с примитивными типами, поэтому разработчики могут использовать либо типы объектов-оболочек, либо более простые не объектные примитивные типы. Raku автоматически преобразует примитивные типы в объекты при обращении к их методам.

Совместимость: эквивалентность и подтипы

Средство проверки типов для языка со статической типизацией должно проверять, что тип любого выражения соответствует типу, ожидаемому контекстом, в котором это выражение появляется. Например, в операторе присваивания формы предполагаемый тип выражения должен соответствовать объявленному или предполагаемому типу переменной. Это понятие согласованности, называемое совместимостью, характерно для каждого языка программирования. x := eex

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

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

Смотрите также

Примечания

использованная литература

дальнейшее чтение

внешние ссылки

Последняя правка сделана 2023-03-19 01:42:43
Содержание доступно по лицензии CC BY-SA 3.0 (если не указано иное).
Обратная связь: support@alphapedia.ru
Соглашение
О проекте