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

Форма полиморфизма типа

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

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

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

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

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

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

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

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

Примеры

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

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

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

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

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

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

Подчинение

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

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

При обсуждении концепции подчинения набор значений типа обозначается путем написания его имени математическим курсивом: 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?». Если значение соответствует критериям, то функция возвращает значение. Если нет, то значение не выбирается, и ничего не возвращается. (Списковые включения являются формой этого шаблона, используемого во многих языках программирования.)

Если есть два предиката, один из которых применяет критерии выбора для типа 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{ and }}P_{s}(v)\}}$

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

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

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

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

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

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

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

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

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

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

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

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

Подтипирование и наследование являются независимыми (ортогональными) отношениями. Они могут совпадать, но ни одно из них не является частным случаем другого. Другими словами, между двумя типами 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 .

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

Принуждения

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

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

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

Примечания

1. Копстейк, Энн. Реализация типизированных структурных грамматик признаков. Том 110. Стэнфорд: публикации CSLI, 2002.
2. Карделли, Лука. Семантика множественного наследования. В G. Kahn, D. MacQueen, и G. Plotkin, редакторы, Semantics of Data Types, том 173 Lecture Notes in Computer Science, страницы 51–67. Springer-Verlag, 1984. Полная версия в Information and Computation, 76(2/3):138–164, 1988.
3. Cook, Hill & Canning 1990.
4. Пирс, гл. 15 примечания
5. Бенджамин К. Пирс, Типы и языки программирования , MIT Press, 2002, 15.1 "Subsumption", стр. 181-182
6. Барбара Лисков, Жанетт Винг, Поведенческое понятие подтипирования , ACM Transactions on Programming Languages ​​and Systems, том 16, выпуск 6 (ноябрь 1994 г.), стр. 1811–1841. Обновленная версия появилась как технический отчет CMU: Лисков, Барбара ; Винг, Жанетт (июль 1999 г.). "Поведенческое подтипирование с использованием инвариантов и ограничений" ( PS ) . Получено 05.10.2006 .

Ссылки

Учебники

• Бенджамин К. Пирс, Типы и языки программирования , MIT Press, 2002, ISBN 0-262-16209-1 , глава 15 (подтипирование типов записей), 19.3 (номинальные и структурные типы и подтипирование) и 23.2 (разновидности полиморфизма) 
• C. Szyperski, D. Gruntz, S. Murer, Component software: beyond object-oriented programming , 2nd ed., Pearson Education, 2002, ISBN 0-201-74572-0 , стр. 93–95 (высокоуровневая презентация, предназначенная для пользователей языка программирования) 

Статьи

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

• Рейнольдс, Джон К. Использование теории категорий для проектирования неявных преобразований и универсальных операторов. В ND Jones, редактор, Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation, номер 94 в Lecture Notes in Computer Science. Springer-Verlag, январь 1980 г. Также в Carl A. Gunter и John C. Mitchell, редакторы, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994 г.).

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

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