Подтипирование

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

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

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

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

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

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

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

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

Примеры

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

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

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

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

function max (x as Number, y as Number) is
    if x < y then
        return y
    else
        return x
end

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

Подчинение

В теории типов концепция включения используется для определения или оценки того, является ли тип подтипом типа T. S

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Схемы подтипирования

Теоретики типов проводят различие между номинальным подтипированием , при котором только типы, объявленные определенным образом, могут быть подтипами друг друга, и структурным подтипированием , при котором структура двух типов определяет, является ли один подтипом другого. Описанное выше объектно-ориентированное подтипирование на основе классов является номинальным; правило структурного подтипирования для объектно-ориентированного языка может гласить, что если объекты типа A могут обрабатывать все сообщения, которые могут обрабатывать объекты типа B (то есть, если они определяют все те же методы ), то 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 ₂ . Это можно резюмировать, используя следующее правило типизации :

$${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 : n -арная функция внутри является классом, который наследует ${\mathtt {Function_{N}({-A_{1}},{-A_{2}},\dots ,{-A_{n}},{+B})}}$ типаж (который можно рассматривать как общий интерфейс в Java -подобных языках), где ${\mathtt {A_{1},A_{2},\dots ,A_{n}}}$ типы параметров и ${\mathtt {B}}$ это тип возвращаемого значения; Знак «-» перед типом означает, что тип является контравариантным, а «+» означает ковариантный.

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

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

Связь с наследством

Подтипирование и наследование являются независимыми (ортогональными) отношениями. Они могут совпадать, но ни один из них не является частным случаем другого. Другими словами, между двумя типами 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. . наследству тип m в S — S → S. По Чтобы S был подтипом T, тип m в S должен быть подтипом типа m в T. другими словами: S → S ≤: T → T . При применении правила подтипирования функций снизу вверх это означает: S ≤: T и T ≤: S , что возможно только в том случае, если S и T одинаковы. Поскольку наследование является иррефлексивным отношением, S подтипом T. не может быть

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

Принуждение

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

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

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

См. также

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

Ссылки

Учебники

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

Статьи

Кук, Уильям Р.; Хилл, Уолтер; Каннинг, Питер С. (1990). Наследование не является подтипом . Учеб. 17-й симпозиум ACM SIGPLAN-SIGACT. по принципам языков программирования (POPL). стр. 125–135. CiteSeerX   10.1.1.102.8635 . дои : 10.1145/96709.96721 . ISBN  0-89791-343-4 .

• Рейнольдс, Джон К. Использование теории категорий для разработки неявных преобразований и универсальных операторов. В Н. Д. Джонсе, редакторе, «Труды Орхусского семинара по семантически-ориентированной генерации компиляторов», номер 94 в «Конспектах лекций по информатике». 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 сравниваются подтипы записей и объектов.