Полиморфизм типов: Подтипирование

Введение

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

В теории языков программирования подтипирование (также называемое подтиповым полиморфизмом или полиморфизмом включения) является формой полиморфизма типа. Подтип — это тип данных, связанный с другим типом данных (супертипом) посредством некоторой концепции заменяемости, что означает, что элементы программы (обычно подпрограммы или функции), написанные для работы с элементами супертипа, также могут работать с элементами подтипа. Если S является подтипом T, то отношение подтипирования (обозначаемое как S <: T, S ⊑ T или S ≤: T) означает, что любой член типа S может безопасно использоваться в любом контексте, где ожидается член типа T. Точная семантика подтипирования здесь критически зависит от того, как конкретным формализмом типов или языком программирования определены понятия «безопасное использование» и «любой контекст». Типовая система языка программирования по сути определяет собственное отношение подтипирования, которое может быть тривиальным, если язык не поддерживает никаких (или очень мало) механизмов преобразования. Благодаря отношению подтипирования член может принадлежать более чем к одному типу. Следовательно, подтипирование является формой полиморфизма типа. В объектно-ориентированном программировании термин «полиморфизм» обычно используется для обозначения исключительно этого подтипового полиморфизма, в то время как методы параметрического полиморфизма рассматриваются как обобщённое программирование. Функциональные языки программирования часто допускают подтипирование записей. Следовательно, просто типизированный лямбда-исчисление, расширенное типами записей, является, пожалуй, самой простой теоретической средой, в которой можно определить и изучить полезное понятие подтипирования. Поскольку полученное исчисление позволяет членам иметь более одного типа, оно больше не является «простой» теорией типов. Поскольку функциональные языки программирования по определению поддерживают литералы функций, которые также могут храниться в записях, типы записей с подтипированием предоставляют некоторые возможности объектно-ориентированного программирования. Как правило, функциональные языки программирования также предоставляют некоторую, обычно ограниченную, форму параметрического полиморфизма. В теоретическом контексте желательно изучать взаимодействие этих двух возможностей; распространённой теоретической средой является система F<:. Различные исчисления, стремящиеся отразить теоретические свойства объектно-ориентированного программирования, могут быть получены из системы F<:. Понятие подтипирования связано с лингвистическими понятиями гипонимии и голонимии. Оно также связано с концепцией ограниченной квантификации в математической логике (см. Логика с упорядоченной сортировкой). Подтипирование не следует путать с понятием (класса или объекта) наследования в объектно-ориентированных языках; подтипирование — это отношение между типами (интерфейсами в объектно-ориентированном жаргоне), в то время как наследование — это отношение между реализациями, возникающее из языковой возможности, позволяющей создавать новые объекты на основе существующих. В ряде объектно-ориентированных языков подтипирование называется наследованием интерфейса, а наследование — наследованием реализации.

In programming language theory, subtyping (also called subtype polymorphism or inclusion polymorphism) is a form of type polymorphism. A subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements (typically subroutines or functions), written to operate on elements of the supertype, can also operate on elements of the subtype. If S is a subtype of T, the subtyping relation (written as 1=S <: T, 1=S ⊑ T, or 1=S ≤: T ) means that any term of type S can safely be used in any context where a term of type T is expected. The precise semantics of subtyping here crucially depends on the particulars of how "safely be used" and "any context" are defined by a given type formalism or programming language. The type system of a programming language essentially defines its own subtyping relation, which may well be trivial, should the language support no (or very little) conversion mechanisms. Due to the subtyping relation, a term may belong to more than one type. Subtyping is therefore a form of type polymorphism. In object oriented programming the term 'polymorphism' is commonly used to refer solely to this subtype polymorphism, while the techniques of parametric polymorphism would be considered generic programming. Functional programming languages often allow the subtyping of records. Consequently, simply typed lambda calculus extended with record types is perhaps the simplest theoretical setting in which a useful notion of subtyping may be defined and studied. Because the resulting calculus allows terms to have more than one type, it is no longer a "simple" type theory. Since functional programming languages, by definition, support function literals, which can also be stored in records, records types with subtyping provide some of the features of object oriented programming. Typically, functional programming languages also provide some, usually restricted, form of parametric polymorphism. In a theoretical setting, it is desirable to study the interaction of the two features; a common theoretical setting is system F<:. Various calculi that attempt to capture the theoretical properties of object oriented programming may be derived from system F<:. The concept of subtyping is related to the linguistic notions of hyponymy and holonymy. It is also related to the concept of bounded quantification in mathematical logic (see Order sorted logic). Subtyping should not be confused with the notion of (class or object) inheritance from object oriented languages; subtyping is a relation between types (interfaces in object oriented parlance) whereas inheritance is a relation between implementations stemming from a language feature that allows new objects to be created from existing ones. In a number of object oriented languages, subtyping is called interface inheritance, with inheritance referred to as implementation inheritance.

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

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

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

Теоретики типов различают номинальное подтипирование, в котором подтипами друг друга могут быть только типы, объявленные определённым образом, и структурное подтипирование, в котором структура двух типов определяет, является ли один из них подтипом другого. Описанное выше подтипирование на основе классов является номинальным; правило структурного подтипирования для объектно-ориентированного языка может гласить, что если объекты типа A могут обрабатывать все сообщения, которые могут обрабатывать объекты типа B (то есть, если они определяют все те же методы), то A является подтипом B, независимо от того, наследует ли один из них другой. Это так называемое "утиное типирование" (duck typing) распространено в динамически типизированных объектно-ориентированных языках. Также хорошо известны правила структурного подтипирования для типов, отличных от объектных. Реализации языков программирования с подтипированием делятся на два основных класса: инклюзивные, в которых представление любого значения типа A также представляет то же значение как тип B, если A <: B, и коэрсивные, в которых значение типа A может быть автоматически преобразовано в тип B. Подтипирование, обусловленное наследованием классов в объектно-ориентированном языке, обычно является инклюзивным; отношения подтипирования, связывающие целые числа и числа с плавающей точкой, которые представлены по-разному, обычно являются коэрсивными. Почти во всех системах типов, определяющих отношение подтипов, оно рефлексивно (то есть A <: A для любого типа A) и транзитивно (то есть, если A <: B и B <: C, то A <: C). Это делает его предзаказом на типы.

Широта и глубина подтипирования

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

Типы функций

Если `T1 → T2` – тип функции, то подтипом его является любая функция типа `S1 → S2` с условием, что `T1 <: S1` и `S2 <: T2`. Это можно представить следующим правилом типизации:

Тип параметра функции `S1 → S2` называется контравариантным, поскольку отношение подтипирования для него обращено, в то время как тип возвращаемого значения является ковариантным. Неформально, это обращение происходит потому, что уточненный тип "более лоялен" к типам, которые он принимает, и "более строг" к типу, который он возвращает. Именно так это работает в Scala: функция с n аргументами внутренне является классом, наследующим трейт (который можно рассматривать как общий интерфейс в языках, подобных Java), где – типы параметров, а – тип возвращаемого значения; знак "−" перед типом указывает на то, что тип контравариантен, а знак "+" – на ковариантность. В языках, допускающих побочные эффекты, как большинство объектно-ориентированных языков, подтипирования обычно недостаточно для гарантии безопасного использования функции в контексте другой. Работа Лискова в этой области была посвящена поведенческому подтипированию, которое, помимо безопасности системы типов, обсуждаемой в этой статье, также требует, чтобы подтипы сохраняли все инварианты, гарантированные супертипами в рамках некоторого контракта. Это определение подтипирования, как правило, неразрешимо, поэтому его нельзя проверить с помощью проверки типов. Подтипирование изменяемых ссылок аналогично обработке значений параметров и возвращаемых значений. Записываемые ссылки (или приемники) являются контравариантными, как значения параметров; читаемые ссылки (или источники) – ковариантными, как возвращаемые значения. Изменяемые ссылки, выступающие и в роли источников, и в роли приемников, являются инвариантными.