Тип пересечения

В теории типов тип пересечения может быть присвоен значениям, которым можно присвоить как тип, так и тип пересечения. $\sigma$ и тип $\tau$. Этому значению может быть присвоен тип пересечения. $\sigma \cap \tau$ в системе типа перекрестка . Как правило, если диапазоны значений двух типов перекрываются, то значению, принадлежащему пересечению двух диапазонов, может быть присвоен тип пересечения этих двух типов. Такое значение можно безопасно передать в качестве аргумента функциям, ожидающим любой из двух типов. Например, в Java класс Boolean реализует как Serializable и Comparable интерфейсы. Поэтому объект типа Boolean можно безопасно передавать функциям, ожидающим аргумент типа Serializable и функциям, ожидающим аргумент типа Comparable.

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

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

Современные языки программирования, включая Ceylon , Flow, Java , Scala , TypeScript и Whiley (см. сравнение языков с типами пересечений ), используют типы пересечений для объединения спецификаций интерфейса и выражения специального полиморфизма . В дополнение к параметрическому полиморфизму типы пересечений могут использоваться, чтобы избежать загрязнения иерархии классов из- за сквозных проблем и сократить шаблонный код , как показано в примере TypeScript ниже.

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

Пример TypeScript

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

Следующий программный код определяет классы Chicken, Cow, и RandomNumberGenerator что у каждого есть метод produce возврат объекта любого типа Egg, Milk, или number. Кроме того, функции eatEgg и drinkMilk требуются аргументы типа Egg и Milk, соответственно.

class Egg { private kind: "Egg" }
class Milk { private kind: "Milk" }

// produces eggs
class Chicken { produce() { return new Egg(); } }

// produces milk
class Cow { produce() { return new Milk(); } }

// produces a random number
class RandomNumberGenerator { produce() { return Math.random(); } }

// requires an egg
function eatEgg(egg: Egg) {
    return "I ate an egg.";
}

// requires milk
function drinkMilk(milk: Milk) {
    return "I drank some milk.";
}

Следующий программный код определяет специальную полиморфную функцию animalToFood который вызывает функцию-член produce данного объекта animal. Функция animalToFood имеет аннотации двух типов, а именно ((_: Chicken) => Egg) и ((_: Cow) => Milk), подключенный через конструктор типа пересечения &. Конкретно, animalToFood при применении к аргументу типа Chicken возвращает объект типа type Eggи при применении к аргументу типа Cow возвращает объект типа type Milk. В идеале, animalToFood не должно быть применимо к любому объекту, имеющему (возможно, случайно) produce метод.

// given a chicken, produces an egg; given a cow, produces milk
let animalToFood: ((_: Chicken) => Egg) & ((_: Cow) => Milk) =
    function (animal: any) {
        return animal.produce();
    };

Наконец, следующий программный код демонстрирует безопасное использование приведенных выше определений.

var chicken = new Chicken();
var cow = new Cow();
var randomNumberGenerator = new RandomNumberGenerator();

console.log(chicken.produce()); // Egg { }
console.log(cow.produce()); // Milk { }
console.log(randomNumberGenerator.produce()); //0.2626353555444987

console.log(animalToFood(chicken)); // Egg { }
console.log(animalToFood(cow)); // Milk { }
//console.log(animalToFood(randomNumberGenerator)); // ERROR: Argument of type 'RandomNumberGenerator' is not assignable to parameter of type 'Cow'

console.log(eatEgg(animalToFood(chicken))); // I ate an egg.
//console.log(eatEgg(animalToFood(cow))); // ERROR: Argument of type 'Milk' is not assignable to parameter of type 'Egg'
console.log(drinkMilk(animalToFood(cow))); // I drank some milk.
//console.log(drinkMilk(animalToFood(chicken))); // ERROR: Argument of type 'Egg' is not assignable to parameter of type 'Milk'

Приведенный выше программный код имеет следующие свойства:

• Строки 1–3 создают объекты. chicken, cow, и randomNumberGenerator соответствующего типа.
• Строки 5–7 выводят для ранее созданных объектов соответствующие результаты (представленные в виде комментариев) при вызове. produce.
• Строка 9 (соответственно 10) демонстрирует безопасное использование метода. animalToFood применяется к chicken (соответственно cow).
• Если строка 11 не закомментирована, это приведет к ошибке типа во время компиляции. Хотя реализация ​ animalToFood мог бы вызвать produce метод randomNumberGenerator, аннотация типа animalToFood запрещает это. Это соответствует предполагаемому смыслу animalToFood.
• Строка 13 (соответственно 15) показывает, что применение animalToFood к chicken (соответственно cow) приводит к объекту типа Egg (соответственно Milk).
• Строка 14 (соответственно 16) показывает, что применение animalToFood к cow (соответственно chicken) не приводит к созданию объекта типа Egg (соответственно Milk). Следовательно, если строка 14 (соответственно 16) не закомментирована, это приведет к ошибке типа во время компиляции.

Сравнение с наследованием

Приведенный выше минималистский пример можно реализовать с помощью наследования , например, путем наследования классов Chicken и Cow из базового класса Animal. Однако в более крупных условиях это может оказаться невыгодным. Введение новых классов в иерархию классов не обязательно оправдано из-за сквозных проблем , а может быть и совершенно невозможно, например, при использовании внешней библиотеки. Можно представить, что приведенный выше пример можно расширить следующими классами:

• класс Horse у которого нет produce метод;
• класс Sheep у которого есть produce возврат метода Wool;
• класс Pig у которого есть produce метод, который можно использовать только один раз, возвращая Meat.

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

Сравнение с утиным набором текста

Приведенный выше минималистский пример уже показывает, что утиная типизация менее подходит для реализации данного сценария. В то время как класс RandomNumberGenerator содержит produce метод, объект randomNumberGenerator не должно быть веским аргументом в пользу animalToFood. Приведенный выше пример можно реализовать с помощью утиной печати, например, введя новое поле. argumentForAnimalToFood на занятия Chicken и Cow означающий, что объекты соответствующего типа являются действительными аргументами для animalToFood. Однако это не только увеличит размер соответствующих классов (особенно с введением большего количества методов, подобных animalToFood), но также является нелокальным подходом по отношению к animalToFood.

Сравнение с перегрузкой функций

Приведенный выше пример можно реализовать с помощью перегрузки функции , например, реализовав два метода. animalToFood(animal: Chicken): Egg и animalToFood(animal: Cow): Milk. В TypeScript такое решение практически идентично приведенному примеру. Другие языки программирования, такие как Java , требуют отдельных реализаций перегруженного метода. Это может привести либо к дублированию кода , либо к шаблонному коду .

Сравнение с шаблоном посещений

Приведенный выше пример можно реализовать с помощью шаблона посетителя . Для этого потребуется, чтобы каждый класс животных реализовал accept метод, принимающий объект, реализующий интерфейс AnimalVisitor (добавление нелокального шаблонного кода ). Функция animalToFood будет реализовано как visit способ реализации AnimalVisitor. К сожалению, связь между типом входа ( Chicken или Cow) и тип результата ( Egg или Milk) было бы трудно представить.

Ограничения

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

Зависимый тип пересечения

Зависимый тип пересечения , обозначаемый $(x:\sigma )\cap \tau$, является зависимым типом , в котором тип $\tau$ может зависеть от термина переменная $x$. В частности, если термин $M$ имеет зависимый тип пересечения $(x:\sigma )\cap \tau$, то срок $M$ имеет оба типа $\sigma$ и тип $\tau [x:=M]$, где $\tau [x:=M]$ это тип, который получается в результате замены всех вхождений термина переменная $x$ в $\tau$ по сроку $M$.

Пример Scala

Scala поддерживает объявления типов. как члены объекта. Это позволяет типу члена объекта зависеть от значения другого члена, что называется типом, зависящим от пути . Например, следующий текст программы определяет особенность Scala. Witness, который можно использовать для реализации шаблона Singleton .

trait Witness {
  type T
  val value: T {}
}

Вышеуказанная черта Witness заявляет член T, которому можно присвоить тип в качестве значения, а члену value, которому можно присвоить значение типа T. Следующий текст программы определяет объект booleanWitness как пример вышеуказанной черты Witness. Объект booleanWitness определяет тип T как Boolean и ценность value как true. Например, выполнение System.out.println(booleanWitness.value) принты true на консоли.

object booleanWitness extends Witness {
  type T = Boolean
  val value = true
}

Позволять $\langle {\textsf {x}}:\sigma \rangle$ быть типом (в частности, типом записи ) объектов, имеющих член ${\textsf {x}}$ типа $\sigma$. В приведенном выше примере объект booleanWitness может быть назначен зависимый тип пересечения $(x:\langle {\textsf {T}}:{\text{Type}}\rangle )\cap \langle {\textsf {value}}:x.{\textsf {T}}\rangle$. Аргументация следующая. Объект booleanWitness имеет члена T которому присвоен тип Boolean как его ценность. С Boolean это тип, объект booleanWitness имеет тип $\langle {\textsf {T}}:{\text{Type}}\rangle$. Кроме того, объект booleanWitness имеет члена value которому присвоено значение true типа Boolean. Поскольку значение booleanWitness.T является Boolean, объект booleanWitness имеет тип $\langle {\textsf {value}}:{\textsf {booleanWitness.T}}\rangle$. В целом объект booleanWitness имеет тип пересечения $\langle {\textsf {T}}:{\text{Type}}\rangle \cap \langle {\textsf {value}}:{\textsf {booleanWitness.T}}\rangle$. Поэтому, представляя ссылку на себя как зависимость, объект booleanWitness имеет зависимый тип пересечения $(x:\langle {\textsf {T}}:{\text{Type}}\rangle )\cap \langle {\textsf {value}}:x.{\textsf {T}}\rangle$.

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

Пересечение типового семейства

Пересечение семейства типов , обозначаемое ${\textstyle \bigcap _{x:\sigma }\tau }$, является зависимым типом , в котором тип $\tau$ может зависеть от термина переменная $x$. В частности, если термин $M$ имеет тип ${\textstyle \bigcap _{x:\sigma }\tau }$, то для каждого члена $N$ типа $\sigma$, термин $M$ имеет тип $\tau [x:=N]$. Это понятие еще называют неявным типом Пи , отмечая, что аргумент $N$ не сохраняется на уровне срока.

Сравнение языков по типам пересечений

Язык	Активно развивается	Парадигма(ы)	Статус	Функции
С#	Да	Функциональный Императив Объектно-ориентированный	В стадии обсуждения	Кроме того, параметры универсального типа могут иметь ограничения, которые требуют, чтобы их (мономорфизированные) аргументы типа реализовывали несколько интерфейсов, после чего тип времени выполнения, представленный параметром универсального типа, становится типом пересечения всех перечисленных интерфейсов.
Цейлон	Нет	Объектно-ориентированный	Поддерживается	Тип уточнения Состав интерфейса Подтипирование по ширине
Ф#	Да	Функциональный Императив Объектно-ориентированный	В стадии обсуждения	?
Поток	Да	Функциональный Императив Объектно-ориентированный Сценарии	Поддерживается	Тип уточнения Состав интерфейса
Форсайт	Нет	Императив	Поддерживается	Пересечение типов функций Подтипы дистрибутивных, ко- и контравариантных функций
Ява	Да	Императив Объектно-ориентированный	Поддерживается	Тип уточнения Состав интерфейса Подтипирование по ширине
PHP	Да	Функциональный Императив Объектно-ориентированный Сценарии	Поддерживается	Тип уточнения Состав интерфейса
Скала	Да	Функциональный Императив Объектно-ориентированный	Поддерживается	Тип уточнения Линейная композиция Подтипирование по ширине
Машинопись	Да	Функциональный Императив Объектно-ориентированный Сценарии	Поддерживается	Пересечение произвольного типа Состав интерфейса Подтипирование по ширине и глубине
Пока	Да	Функциональный Императив	Поддерживается	?