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

Концепция информатики

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

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

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

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

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

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

Основы

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Многие языки со статической проверкой типов предоставляют возможность обойти проверку типов. Некоторые языки позволяют программистам выбирать между статической и динамической безопасностью типов. Например, исторически в C# переменные объявляются статически, ^{[9] : 77, раздел 3.2,} но в C# 4.0 введено dynamicключевое слово, которое используется для объявления переменных, подлежащих динамической проверке во время выполнения. ^{[9] : 117, раздел 4.1} . Другие языки позволяют писать код, который не является типобезопасным; например, в C программисты могут свободно приводить значения между любыми двумя типами одинакового размера, фактически подрывая концепцию типа.

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

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

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

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

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

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

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

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

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

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

И наоборот, начиная с версии 4.0, язык C# предоставляет способ указать, что переменная не должна подвергаться статической проверке типа. Переменная типа dynamicне будет подвергаться статической проверке типа. Вместо этого программа полагается на информацию о типе времени выполнения, чтобы определить, как можно использовать переменную. ^{[12] [9] : 113–119}

В Rust type обеспечивает динамическую типизацию типов. ^[13]dyn std::any::Any'static

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

вар х:= 5; вар у := "37";вар z:= x + y;

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

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

интервал х = 5 ; char y [] = "37" ; символ * z = х + у ; printf ( "%c \n " , * z );            

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

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

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

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

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

• Директива use strictв JavaScript ^{[18] [19] [20]} и Perl применяет более строгую проверку.
• В PHP ^[21]declare(strict_types=1) для каждого файла допускается принимать только переменную точного типа объявления типа или выбрасывать a.TypeError
• In Option Strict OnVB.NET позволяет компилятору требовать преобразования между объектами .

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

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

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

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

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

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

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

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

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

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

1. Например, во время разработки может возникнуть дырявая абстракция , которая может указывать на необходимость дополнительной разработки типов. — «Вычисление правильно типизированной программы всегда завершается». — Б. Нордстрем, К. Петерссон и Дж. М. Смит ^[5] Систематическое изменение переменных во избежание захвата свободной переменной может привести к ошибке в функциональном языке программирования, где функции являются гражданами первого класса. ^[6] — Из статьи о лямбда-исчислении .
2. Также называется зависимым типом продукта , поскольку . ${\textstyle (x:\sigma )\to \tau =\prod _{x:\sigma }\tau }$
3. Также называется типом зависимой суммы , поскольку . ${\textstyle (x:\sigma )\times \tau =\sum _{x:\sigma }\tau }$

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

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

${\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 для межпроцессного взаимодействия, статически гарантируя, что процессы не могут совместно использовать объекты в общей памяти, чтобы предотвратить условия гонки. Язык 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 году Джон К. Митчелл и Гордон Плоткин создали формальную теорию под лозунгом: «Абстрактные типы [данных] имеют экзистенциальный тип». ^[25] Теория представляет собой типизированное лямбда-исчисление второго порядка , подобное Системе F , но с экзистенциальной, а не универсальной количественной оценкой.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• Портал компьютерного программирования

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

Примечания

1. Компьютерная линия Burroughs ALGOL определяла содержимое ячейки памяти по битам ее флага. Биты флагов определяют содержимое ячейки памяти. Инструкция, тип данных и функции определяются 3-битным кодом в дополнение к 48-битному содержимому. Только MCP (главная программа управления) могла записывать биты кода флага.

Рекомендации

1. Пирс 2002, с. 1: «Система типов — это понятный синтаксический метод доказательства отсутствия определенного поведения программы путем классификации фраз в соответствии с типами значений, которые они вычисляют».
2. Карделли 2004, с. 1: «Основная цель системы типов — предотвратить возникновение ошибок выполнения во время работы программы».
3. Пирс 2002, с. 208.
4. Сети, Р. (1996). Языки программирования: Концепции и конструкции (2-е изд.). Аддисон-Уэсли. п. 142. ИСБН 978-0-201-59065-4. ОСЛК  604732680.
5. Нордстрем, Б.; Петерссон, К.; Смит, Дж. М. (2001). «Теория типов Мартина-Лёфа». Алгебраические и логические структуры . Справочник по логике в информатике. Том. 5. Издательство Оксфордского университета. п. 2. ISBN 978-0-19-154627-3.
6. Тернер, Д.А. (12 июня 2012 г.). «Некоторые истории языков функционального программирования» (PDF) . приглашенная лекция на TFP12 в Университете Сент-Эндрюс . См. раздел об Алголе 60.
7. «... любая здравая, разрешимая система типов должна быть неполной» — Д. Реми (2017). п. 29, Реми, Дидье. «Системы типов для языков программирования» (PDF) . Архивировано из оригинала (PDF) 14 ноября 2017 года . Проверено 26 мая 2013 г.
8. Пирс 2002.
9. Скит, Джон (2019). C# в глубине (4-е изд.). Мэннинг. ISBN 978-1617294532.
10. Миглани, Гаурав (2018). «Динамическая диспетчеризация методов или полиморфизм времени выполнения в Java». Архивировано из оригинала 07 декабря 2020 г. Проверено 28 марта 2021 г.
11. Райт, Эндрю К. (1995). Практическая мягкая печать (доктор философии). Университет Райса. hdl : 1911/16900.
12. «динамический (Справочник по C#)». Библиотека MSDN . Майкрософт . Проверено 14 января 2014 г.
13. "std::any — Rust". doc.rust-lang.org . Проверено 7 июля 2021 г.
14. Мейер, Эрик; Дрейтон, Питер. «Статическая типизация, где это возможно, динамическая типизация, когда необходимо: конец холодной войны между языками программирования» (PDF) . Корпорация Майкрософт .
15. Лаучер, Аманда; Снавли, Пол (2012). «Типы против тестов». ИнфоВ.
16. Си, Хунвэй (1998). Зависимые типы в практическом программировании (PhD). Департамент математических наук Университета Карнеги-Меллона. CiteSeerX 10.1.1.41.548 . 
    Си, Хунвэй; Пфеннинг, Франк (1999). «Зависимые типы в практическом программировании». Материалы 26-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . АКМ. стр. 214–227. CiteSeerX  10.1.1.69.2042 . дои : 10.1145/292540.292560. ISBN 1581130953. S2CID  245490.
17. Visual Basic — это пример языка, безопасного как по типу, так и по памяти.
18. «4.2.2 Строгий вариант ECMAScript» . Спецификация языка ECMAScript® 2020 (11-е изд.). ЭКМА. Июнь 2020. ECMA-262.
19. «Строгий режим – JavaScript». МДН . Разработчик.mozilla.org. 03 июля 2013 г. Проверено 17 июля 2013 г.
20. «Строгий режим (JavaScript)» . MSDN . Майкрософт . Проверено 17 июля 2013 г.
21. «Строгая типизация». Руководство по PHP: Справочник по языку: Функции .
22. Брача, Г. «Подключаемые типы» (PDF) .
23. «Конечно. Это называется «постепенная типизация», и я бы назвал ее модной. ...» Существует ли язык, который позволяет как статическую, так и динамическую типизацию? . переполнение стека. 2012.
24. Копылов, Алексей (2003). «Зависимое пересечение: новый способ определения записей в теории типов». 18-й симпозиум IEEE по логике в информатике . LICS 2003. Компьютерное общество IEEE. стр. 86–95. CiteSeerX 10.1.1.89.4223 . дои : 10.1109/LICS.2003.1210048. 
25. Митчелл, Джон К.; Плоткин, Гордон Д. (июль 1988 г.). «Абстрактные типы имеют экзистенциальный тип» (PDF) . АКМ Транс. Программа. Ланг. Сист . 10 (3): 470–502. дои : 10.1145/44501.45065. S2CID  1222153.
26. Сик, Джереми (24 марта 2014 г.). «Что такое постепенное типирование?».
27. Сик, Джереми; Таха, Валид (сентябрь 2006 г.). Постепенная типизация для функциональных языков (PDF) . Схема и функциональное программирование 2006 . Чикагский университет . стр. 81–92.
28. Барендрегт, Хенк; Деккерс, Уил; Статман, Ричард (20 июня 2013 г.). Лямбда-исчисление с типами. Издательство Кембриджского университета. п. 66. ИСБН 978-0-521-76614-2.
29. «8.2.4 Унификация системы типов» . Спецификация языка C# (5-е изд.). ЭКМА. Декабрь 2017. ECMA-334.
30. «Родные типы». Документация по Perl 6 .
31. «Числа, § Автобокс» . Документация по Perl 6 .

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

• Карделли, Лука ; Вегнер, Питер (декабрь 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). «Что нужно знать перед обсуждением систем типов».