Типовая система

Эта статья о системах типов в компьютерном программировании. Для формального изучения систем типов см. Теорию типов .

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

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

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

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

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

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

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

Примером простой системы типов является C. язык Части программы на языке C представляют собой определения функций . Одна функция вызывается другой функцией.

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

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

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

Компилятор C проверяет типы аргументов, передаваемых функции при ее вызове, по типам параметров, объявленных в определении функции. Если типы не совпадают, компилятор выдает ошибку или предупреждение во время компиляции.

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

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

Основы

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

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

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

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

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

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

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

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

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

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

Введите ошибки

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

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

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

Процесс проверки и обеспечения соблюдения ограничений типов — проверка типов — может происходить во время компиляции (статическая проверка) или во время выполнения (динамическая проверка).

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

Эти термины обычно не используются в строгом смысле.

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

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

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

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

if <complex test> then <do something> else <signal that there is a type error>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В Русте ​ dyn std::any::Any type обеспечивает динамическую типизацию 'static типы.

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

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

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

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

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

Статически типизированные языки, в которых отсутствует вывод типа (например, C и Java до версии 10 ), требуют, чтобы программисты объявляли типы, которые должен использовать метод или функция. Это может служить дополнительной документацией программы, которая является активной и динамической, а не статической. Это позволяет компилятору предотвратить рассинхронизацию и игнорирование программистами. Однако язык может быть статически типизирован без необходимости объявления типа (примеры включают Haskell , Scala , OCaml , F# , Swift и, в меньшей степени, 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);

В этом примере z будет указывать на адрес памяти, находящийся на пять символов дальше y, что эквивалентно трем символам после завершающего нулевого символа строки, на которую указывает y. Это память, к которой программа не имеет доступа. В терминах C это просто неопределенное поведение , и программа может делать что угодно; с помощью простого компилятора он может фактически напечатать любой байт, хранящийся после строки «37». Как показывает этот пример, C небезопасен для памяти. Поскольку предполагалось, что произвольные данные являются символами, этот язык также не является типобезопасным.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В следующей таблице представлен обзор концепций теории типов, которые используются в специализированных системах типов. Имена M, N, O варьируются по терминам и именам. $\sigma ,\tau$ диапазон по типам. Будут использоваться следующие обозначения:

• $M:\sigma$ означает, что $M$ имеет тип $\sigma$;
• $M(N)$ это применение $M$ на $N$;
• $\tau [\alpha :=\sigma ]$ (соответственно $\tau [x:=N]$) описывает тип, который получается в результате замены всех вхождений переменной типа α (соответственно терминальной переменной x ) в $\tau$ по типу σ (соответственно терм N ).

Понятие типа	Обозначения	Значение
Функция	$\sigma \to \tau$	Если $M:\sigma \to \tau$ и $N:\sigma$, затем $M(N):\tau$.
Продукт	$\sigma \times \tau$	Если $M:\sigma \times \tau$, затем $M=(N,O)$ это пара ул $N:\sigma$ и $O:\tau$.
Сумма	$\sigma +\tau$	Если $M:\sigma +\tau$, затем $M=\iota _{1}(N)$ это первая инъекция $N:\sigma$, или $M=\iota _{2}(N)$ это вторая инъекция $N:\tau$.
Пересечение	$\sigma \cap \tau$	Если $M:\sigma \cap \tau$, затем $M:\sigma$ и $M:\tau$.
Союз	$\sigma \cup \tau$	Если $M:\sigma \cup \tau$, затем $M:\sigma$ или $M:\tau$.
Записывать	$\langle x:\tau \rangle$	Если $M:\langle x:\tau \rangle$, то у M есть член $x:\tau$.
Полиморфный	$\forall {}\alpha .\tau$	Если $M:\forall {}\alpha .\tau$, затем $M:\tau [\alpha :=\sigma ]$ для любого типа σ .
Экзистенциальный	$\exists {}\alpha .\tau$	Если $M:\exists {}\alpha .\tau$, затем $M:\tau [\alpha :=\sigma ]$ для некоторого типа σ .
Рекурсивный	$\mu \alpha .\tau$	Если $M:\mu \alpha .\tau$, затем $M:\tau [\alpha :=\mu \alpha .\tau ]$.
Зависимая функция	$(x:\sigma )\to \tau$	Если $M:(x:\sigma )\to \tau$ и $N:\sigma$, затем $M(N):\tau [x:=N]$.
Зависимая пара	$(x:\sigma )\times \tau$	Если $M:(x:\sigma )\times \tau$, затем $M=(N,O)$ это пара ул $N:\sigma$ и $O:\tau [x:=N]$.
Зависимое пересечение	$(x:\sigma )\cap \tau$	Если $M:(x:\sigma )\cap \tau$, затем $M:\sigma$ и $M:\tau [x:=M]$.
Семейное пересечение	$\bigcap _{x:\sigma }\tau$	Если ${\textstyle M:\bigcap _{x:\sigma }\tau }$, затем $M:\tau [x:=N]$ на любой срок $N:\sigma$.
Семейный союз	$\bigcup _{x:\sigma }\tau$	Если ${\textstyle M:\bigcup _{x:\sigma }\tau }$, затем $M:\tau [x:=N]$ на какой-то срок $N:\sigma$.

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

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

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

$\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 для межпроцессного взаимодействия, статически гарантируя, что процессы не могут совместно использовать объекты в общей памяти, чтобы предотвратить условия гонки. Язык Clean ( язык, подобный Haskell ) использует эту систему типов, чтобы добиться большей скорости (по сравнению с выполнением глубокого копирования), оставаясь при этом безопасным.

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

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

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

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

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

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

Типы союзов

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

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

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

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

Основная статья: Квантор существования

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

• intT = {а: int; е: (целое → целое); }
• floatT = {а: поплавок; е: (плавающее → целое); }

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

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

• intT = {а: int; е: (целое → целое); } как ∃X { а: X; е: (Х → целое); }

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

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

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

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

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

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

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

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

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

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

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

Система типов, которая присваивает типы терминам в среде типов с использованием правил типизации , естественно связана с проблемами решения проблем , проверки типов типизации и обитания типов .

• Учитывая тип среды $\Gamma$, термин $e$и тип $\tau$, решите, является ли термин $e$ можно присвоить тип $\tau$ в среде типа.
• Учитывая срок $e$, решить, существует ли среда типов $\Gamma$ и тип $\tau$ такой, что термин $e$ можно присвоить тип $\tau$ в среде типа $\Gamma$.
• Учитывая тип среды $\Gamma$ и тип $\tau$, решить, существует ли термин $e$ которому можно присвоить тип $\tau$ в среде типа.

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

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

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

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

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

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

См. также

• Сравнение систем типов
• Ковариантность и контравариантность (информатика)
• Полиморфизм в объектно-ориентированном программировании
• Введите подпись
• Теория типов

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

• Карделли, Лука ; Вегнер, Питер (декабрь 1985 г.). «О понимании типов, абстракции данных и полиморфизме» (PDF) . Обзоры вычислительной техники ACM . 17 (4): 471–523. CiteSeerX   10.1.1.117.695 . дои : 10.1145/6041.6042 . S2CID   2921816 .
• Пирс, Бенджамин К. (2002). Типы и языки программирования . МТИ Пресс. ISBN  978-0-262-16209-8 .
• Карделли, Лука (2004). «Типовые системы» (PDF) . У Аллена Б. Такера (ред.). Справочник CRC по информатике и инженерии (2-е изд.). ЦРК Пресс. ISBN  978-1584883609 .
• Тратт, Лоуренс (июль 2009 г.). «5. Динамически типизированные языки» . Достижения в области компьютеров . Том. 77. Эльзевир. стр. 149–184. дои : 10.1016/S0065-2458(09)01205-4 . ISBN  978-0-12-374812-6 .

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

• СМИ, связанные с системами типов, на Викискладе?
• Смит, Крис (2011). «Что нужно знать перед обсуждением систем типов» .