Подтип

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

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

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

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

Истоки [ править ]

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

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

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

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

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

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

функция  max  ( x  как  число ,  y  как  число )  ,  если  x  <  y,  то  вернуть  y  иначе  вернуть  x конец

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

Подчинение [ править ]

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

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

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

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

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

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

Если есть два предиката, которые применяют критерии выбора для типа T и которые применяют дополнительные критерии для типа S , тогда могут быть определены наборы для этих двух типов:${\ Displaystyle P_ {T}}$${\ Displaystyle P_ {s}}$

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

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

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

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

${\ displaystyle Felinae = \ {кошка \ in Felidae \ mid \ ofSubfamily (кошка, felinaeSubfamilyName) \}}$

${\ displaystyle Felis = \ {кошка \ in Felinae \ mid \ ofGenus (кошка, felisGenusName) \}}$

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

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

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

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

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

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

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

Подтип ширины и глубины [ править ]

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

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

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

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

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

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

Типы функций [ править ]

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

${\ 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 : а п -ичный функция внутренне класс , который наследует FunctionN (-A1, ~A2, ..., -An + B) черта (которую можно рассматривать в качестве общего интерфейса в Java -как языков), где A1 , A2 ,…An - это типы параметров, а B - его возвращаемый тип; « - » перед типом означает, что тип контравариантен, а « + » означает ковариантный.

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

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

Отношение к наследованию [ править ]

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

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

Первый случай иллюстрируется независимыми типами, такими как Booleanи Float.

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

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

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

Принуждение [ править ]

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

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

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

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

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

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

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

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

Учебники

Статьи

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