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

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

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

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

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

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

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

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

Основы [ править ]

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

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

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

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

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

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

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

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

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

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

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

Ошибки типа [ править ]

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

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

Проверка типа [ править ]

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

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

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

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

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

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

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

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

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

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

Информация о динамической проверке типа и времени выполнения [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 ;

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

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

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

Переменные уровни проверки типов [ править ]

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

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

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

Системы дополнительных типов [ править ]

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

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

Полиморфизм и типы [ править ]

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

Системы специализированных типов [ править ]

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

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

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

Зависимые типы [ править ]

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

Типы пересечений [ править ]

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

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

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

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

Типы союзов [ править ]

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

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

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

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

• intT = {a: int; f: (int → int); }
• floatT = {a: float; f: (float → int); }

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

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

• intT = {a: int; f: (int → int); } как ∃X {a: X; f: (X → int); }

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

Постепенный набор текста [ править ]

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

Явное или неявное объявление и вывод [ править ]

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

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

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

Проблемы с решением [ править ]

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

• Учитывая среду типа , термин и тип , решите, может ли термин быть назначен тип в среде типов.${\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, имеют единую систему типов. ^[25] Это означает, что все типы C #, включая примитивные типы, наследуются от одного корневого объекта. Каждый тип в C # наследуется от класса Object. Некоторые языки, такие как Java и Raku , имеют корневой тип, но также имеют примитивные типы, которые не являются объектами. ^[26] Java предоставляет типы объектов оболочки, которые существуют вместе с примитивными типами, так что разработчики могут использовать либо типы объектов оболочки, либо более простые не объектные примитивные типы. Raku автоматически преобразует примитивные типы в объекты при обращении к их методам. ^[27]

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

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

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

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

См. Также [ править ]

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

Примечания [ править ]

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

Дальнейшее чтение [ править ]

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

Внешние ссылки [ править ]

В Wikibook Ada Programming есть страница по темам: Типы

В Wikibook Haskell есть страница по теме: Объявления классов

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