Подтип - Subtyping

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

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

Функциональные языки программирования часто допускают выделение подтипов записи. Как следствие, просто типизированное лямбда-исчисление расширенный с помощью типов записей - это, пожалуй, простейшая теоретическая установка, в которой можно определить и изучить полезное понятие подтипов.^{[нужна цитата ]}. Поскольку итоговое исчисление позволяет членам иметь более одного типа, это уже не "простой" теория типов. Поскольку функциональные языки программирования по определению поддерживают функциональные литералы, которые также могут храниться в записях, типы записей с подтипами предоставляют некоторые возможности объектно-ориентированного программирования. Обычно языки функционального программирования также предоставляют некоторую, обычно ограниченную, форму параметрического полиморфизма. В теоретической обстановке желательно изучить взаимодействие двух функций; общая теоретическая установка система F_<:. Различные вычисления, которые пытаются уловить теоретические свойства объектно-ориентированного программирования, могут быть получены из системы F._<:.

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

Происхождение

Идея создания подтипов в языках программирования восходит к 1960-м годам; это было введено в Симула производные. Первые формальные трактовки подтипов были даны Джон С. Рейнольдс в 1980 году кто использовал теория категорий оформить неявные преобразования, и Лука Карделли (1985).^[2]

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

Примеры

Пример подтипов: где птица - это супертип, а все остальные - подтипы, как обозначено стрелкой в UML обозначение

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

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

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

функция Максимум (Икс так как Число, у так как Число) является    если Икс < у тогда        возвращаться у    еще        возвращаться Иксконец

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

Потребление

В теории типов понятие подчинение^[3] используется для определения или оценки того, является ли тип S это подтип типа Т.

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

При обсуждении концепции подчинения набор значений типа обозначается путем написания его имени математическим курсивом: Т. Тип, рассматриваемый как предикат домена, обозначается выделением его имени жирным шрифтом: Т. Условный символ <: означает "является подтипом", и :> означает «супертип».

• Тип Т включает S если набор значений Т который он определяет, является надмножеством множества S, так что каждый член S также является членом Т.
• Тип может быть отнесен к более чем одному типу: супертипы S пересекаться в S.
• Если S <: T (и поэтому S ⊆ Т), тогда Т, предикат, описывающий множество Т, должен быть частью предиката S (в том же домене), который определяет S.

• Если S включает Т, и Т включает S, то два типа равны (хотя они могут не быть одним и тем же типом, если система типов различает типы по имени).

Практическое правило: подтип, вероятно, будет «больше / шире / глубже» (его значения содержат больше информации) и «меньше / меньше» (набор значений меньше), чем один из его супертипов (который имеет более ограниченные информация, и набор значений которой является надмножеством значений подтипа).

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

Если есть два предиката, ${\displaystyle P_{T}}$ который применяет критерии выбора для типа Т, и ${\displaystyle P_{s}}$ который применяет дополнительные критерии для типа S, то можно определить наборы для двух типов:

${\displaystyle T=\{v\in D\mid \ P_{T}(v)\}}$

${\displaystyle S=\{v\in D\mid \ P_{T}(v){\text{ and }}P_{s}(v)\}}$

Предикат Т = ${\displaystyle P_{T}}$ применяется вместе с ${\displaystyle P_{s}}$ как часть составного предиката S определение S. Два предиката: соединенный, поэтому оба должны быть истинными, чтобы значение было выбрано. Предикат S = Т ${\displaystyle \land P_{s}}$ = ${\displaystyle P_{T}\land P_{s}}$ включает предикат Т, так S <: (подтипы) Т.

Например: существует подсемейство видов кошек под названием Felinae, который является частью семьи Кошачьих. Род Фелис, которому домашние кошки Felis catus принадлежит, является частью этого подсемейства.

${\displaystyle Felinae=\{cat\in Felidae\mid \ ofSubfamily(cat,felinaeSubfamilyName)\}}$

${\displaystyle Felis=\{cat\in Felinae\mid \ ofGenus(cat,felisGenusName)\}}$

Соединение предикатов здесь было выражено посредством применения второго предиката к области значений, соответствующих первому предикату. Рассматриваются как типы, Felis <: Felinae <: Felidae.

Если Т включает S (Т:> S) затем процедура, функция или выражение с заданным значением ${\displaystyle s\in S}$ как операнд (входной аргумент или терм), следовательно, сможет работать с этим значением как с одним из типов Т, потому что ${\displaystyle s\in T}$. В приведенном выше примере мы могли ожидать, что функция из подсемейства быть применимым к значениям всех трех типов Кошачьих, Felinae и Фелис.

Схемы подтипов

Теоретики типов проводят различие между номинальный подтип, в котором только типы, объявленные определенным образом, могут быть подтипами друг друга, и структурное подразделение, в котором структура двух типов определяет, является ли один подтипом другого. Описанное выше объектно-ориентированное подтипирование на основе классов является номинальным; правило структурного подтипа для объектно-ориентированного языка может сказать, что если объекты типа А может обрабатывать все сообщения, которые объекты типа B может справиться (то есть, если они все же определяют методы ), тогда А это подтип B независимо от того, наследует от другого. Это так называемое утка печатать распространено в объектно-ориентированных языках с динамической типизацией. Также хорошо известны разумные правила структурного выделения подтипов для типов, отличных от типов объектов.^{[нужна цитата ]}

Реализации языков программирования с подтипами делятся на два общих класса: включающий реализации, в которых представление любого значения типа А также представляет то же значение в типе B если А<:B, и принудительный реализации, в которых значение типа А возможно автоматически конвертируется в один из типов B. Подтипирование, вызванное созданием подклассов в объектно-ориентированном языке, обычно является инклюзивным; отношения подтипов, которые связывают целые числа и числа с плавающей запятой, которые представлены по-разному, обычно являются принудительными.

Почти во всех системах типов, которые определяют отношение подтипов, оно является рефлексивным (что означает А<:А для любого типа А) и транзитивный (это означает, что если А<:B и B<:C тогда А<:C). Это делает его Предварительный заказ по типам.

Типы записей

Подтип ширины и глубины

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

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

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

Второй метод, названный подтипирование по глубине, заменяет различные поля их подтипами. То есть поля подтипа являются подтипами полей супертипа. Поскольку любая операция, поддерживаемая для поля в супертипе, поддерживается для его подтипа, любая операция, выполнимая с супертипом записи, поддерживается подтипом записи. Подтип глубины имеет смысл только для неизменяемых записей: например, вы можете назначить 1,5 полю «x» реальной точки (запись с двумя реальными полями), но вы не можете сделать то же самое для поля «x» целая точка (которая, однако, является глубоким подтипом типа реальной точки), потому что 1.5 не является целым числом (см. Дисперсия ).

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

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

Типы функций

Если Т₁ → Т₂ является типом функции, тогда его подтипом является любой тип функции S₁ → S₂ со свойством, что Т₁ <: S₁ и S₂ <: Т₂. Это можно резюмировать, используя следующие правило набора:

${\displaystyle T_{1}\leq :S_{1}\quad S_{2}\leq :T_{2} \over S_{1}\rightarrow S_{2}\leq :T_{1}\rightarrow T_{2}}$

Тип аргумента S₁ → S₂ как говорят контравариантный потому что отношение подтипов для него обратное, тогда как возвращаемый тип ковариантный. Неформально это изменение происходит потому, что уточненный тип «более либерален» в отношении типов, которые он принимает, и «более консервативен» в типе, который он возвращает. Вот что именно работает в Scala: а п-ary функция - это внутренне класс, наследующий ФункцияN (-A1, -A2,…, -An, + B) черта (что можно рассматривать как общее интерфейс в Ява -подобные языки), где A1, A2, … An - это типы параметров, а B его возвращаемый тип; "-"перед типом означает, что тип контравариантен, а"+«означает ковариантный.

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

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

Отношение к наследству

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

1. S не является ни подтипом, ни производным типом Т
2. S является подтипом, но не производным типом Т
3. S не подтип, а производный тип Т
4. S является подтипом и производным типом Т

Первый случай проиллюстрирован независимыми типами, такими как Булево и Плавать.

Второй случай можно проиллюстрировать соотношением между Int32 и Int64. В большинстве объектно-ориентированных языков программирования Int64 не связаны по наследству с Int32. тем не мение Int32 можно рассматривать как подтип Int64 поскольку любое 32-битное целое число может быть преобразовано в 64-битное целое число.

Третий случай является следствием подтипирование входных контравариантностей. Предположим суперкласс типа Т имея метод м возвращает объект того же типа (т.е. тип м является Т → Т, также обратите внимание, что первый аргумент м is this / self) и тип производного класса S из Т. По наследству тип м в S является S → S. Для того чтобы S быть подтипом Т тип м в S должен быть подтипом типа м в Т, другими словами: S → S ≤: Т → Т. При применении правила подтипов функций снизу вверх это означает: S ≤: Т и Т ≤: S, что возможно только при S и Т одинаковые. Поскольку наследование - это иррефлексивное отношение, S не может быть подтипом Т.

Подтипирование и наследование совместимы, когда все унаследованные поля и методы производного типа имеют типы, которые являются подтипами соответствующих полей и методов унаследованного типа. ^[1].

Принуждение

В системах принудительного выделения подтипов подтипы определяются неявным преобразование типов функции от подтипа к супертипу. Для каждого отношения подтипов (S <: Т), функция принуждения принуждать: S → Т предоставляется, и любой объект s типа S рассматривается как объект принуждать_{S → Т}(s) типа Т. Функция принуждения может быть определена композицией: если S <: Т и Т <: U тогда s можно рассматривать как объект типа ты под составным принуждением (принуждать_{Т → U} ∘ принуждать_{S → Т}). В принуждение типа от вида к себе принуждать_{Т → Т} это функция идентичности я бы_Т

Функции принуждения для записей и несвязный союз подтипы могут определяться покомпонентно; в случае записей с расширенной шириной принуждение типа просто отбрасывает любые компоненты, которые не определены в супертипе. Приведение типов для типов функций может быть задано как f '(s) = принуждать_{S2 → Т2}(ж(принуждать_{Т1 → S1}(т))), отражающие контравариантность аргументов функции и ковариации возвращаемых значений.

Функция принуждения однозначно определяется с учетом подтипа и супертип. Таким образом, когда определены отношения нескольких подтипов, нужно быть внимательным, чтобы гарантировать, что все приведенные типы являются согласованными. Например, если целое число, такое как 2: int может быть приведено к числу с плавающей запятой (скажем, 2.0: плавать), то принуждение 2.1: плавать к 2: int, потому что составное принуждение принуждать_{плавать → плавать} данный принуждать_{int → плавать} ∘ принуждать_{плавать → int} тогда будет отличаться от принуждения личности я бы_{плавать}.

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

• Ковариация и контравариантность
• В круг-эллипс задача (для опасностей подтипов типов переменных на той же основе, что и типы значений)
• Программирование на основе классов
• Тип верха
• Тип уточнения
• Подтип поведения

Примечания

1. Cook, Hill & Canning 1990.
2. Пирс, гл. 15 заметок
3. Бенджамин С. Пирс, Типы и языки программирования, MIT Press, 2002, 15.1 «Поглощение», стр. 181–182
4. Барбара Лисков, Жаннетт Винг, Поведенческое понятие подтипов, Транзакции ACM по языкам и системам программирования, том 16, выпуск 6 (ноябрь 1994 г.), стр. 1811–1841. Обновленная версия появилась в виде технического отчета CMU: Лисков, Варвара; Крыло, Жаннетт (Июль 1999 г.). «Поведенческое подтипирование с использованием инвариантов и ограничений» (PS ). Получено 2006-10-05.

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

Учебники

• Бенджамин С. Пирс, Типы и языки программирования, MIT Press, 2002, ISBN  0-262-16209-1, глава 15 (подтипы типов записей), 19.3 (номинальные и структурные типы и подтипы) и 23.2 (разновидности полиморфизма)
• К. Шиперски, Д. Грунц, С. Мурер, Компонентное программное обеспечение: помимо объектно-ориентированного программирования, 2-е изд., Pearson Education, 2002, ISBN  0-201-74572-0, стр. 93–95 (презентация высокого уровня для пользователей языков программирования)

Статьи

• Карделли, Лука. Семантика множественного наследования. В G. Kahn, D. MacQueen и G. Plotkin, редакторах, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 51–67. Springer-Verlag, 1984. Полная версия в Information and Computing, 76 (2/3): 138–164, 1988.
• Кук, Уильям Р.; Хилл, Уолтер; Каннинг, Питер С. (1990). Наследование - это не подтип. Proc. 17-я конференция ACM SIGPLAN-SIGACT. по принципам языков программирования (POPL). С. 125–135. CiteSeerX  10.1.1.102.8635. Дои:10.1145/96709.96721. ISBN  0-89791-343-4.
• Рейнольдс, Джон С. Использование теории категорий для разработки неявных преобразований и общих операторов. В N. D. Jones, редактор, Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation, номер 94 в Lecture Notes in Computer Science. Springer-Verlag, январь 1980 г. Также в: Карл А. Гюнтер и Джон С. Митчелл, редакторы, «Теоретические аспекты объектно-ориентированного программирования: типы, семантика и дизайн языка» (MIT Press, 1994).

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

• Джон С. Рейнольдс, Теории языков программирования, Cambridge University Press, 1998 г., ISBN  0-521-59414-6, глава 16.
• Мартин Абади, Лука Карделли, Теория объектов, Springer, 1996, ISBN  0-387-94775-2. Раздел 8.6 противопоставляет подтипы записей и объектов.