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

В теории типа , типа пересечения могут быть отнесены к значениям , которые могут быть назначены как тип и тип . Это значение может быть дан тип пересечения в качестве системы типа пересечения . ^[1] Обычно, если диапазоны значений двух типов перекрываются, то значению, принадлежащему пересечению двух диапазонов, может быть присвоен тип пересечения этих двух типов. Такое значение можно безопасно передавать в качестве аргумента функциям, ожидающим любого из двух типов. Например, в Java классовые реализует оба и${\ displaystyle \ sigma}$${\ Displaystyle \ тау}$${\ displaystyle \ sigma \ cap \ tau}$BooleanSerializableComparableинтерфейсы. Следовательно, объект типа Booleanможет быть безопасно передан функциям, ожидающим аргумент типа, Serializableи функциям, ожидающим аргумента типа Comparable.

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

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

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

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

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

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

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

class  Egg  {  частный  вид :  "Яйцо"  } class  Milk  {  частный  вид :  "Milk"  }// производит яйца class  Chicken  {  product ()  {  return  new  Egg ();  }  }// производит молоко класса  Cow  {  roduct ()  {  return  new  Milk ();  }  }// производит случайное число class  RandomNumberGenerator  {  произвести ()  {  return  Math . случайный ();  }  }// требуется функция  яйца eatEgg ( egg : Egg )  {  return  «Я съел яйцо». ; }// требуется функция  молока drinkMilk ( milk : Milk )  {  return  "Я выпил немного молока." ; }

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

// получая курицу, производит яйцо; дано корове, дает молоко let  animalToFood :  (( _ : Chicken )  =>  Egg )  &  (( _ : Cow )  =>  Milk )  =  function  ( animal : any )  {  return  animal . произвести ();  };

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

var  курица  =  новая  курица ();var  cow  =  новая  корова ();var  randomNumberGenerator  =  новый  RandomNumberGenerator ();консоль . журнал ( курица . продукция ());  //Яйцо { }консоль . журнал ( корова . производить ());  //Молоко { }консоль . журнал ( randomNumberGenerator . произвести ());  //0.2626353555444987консоль . журнал ( animalToFood ( курица ));  //Яйцо { }консоль . журнал ( animalToFood ( корова ));  //Молоко { }//console.log(animalToFood(randomNumberGenerator)); // ОШИБКА: аргумент типа 'RandomNumberGenerator' не может быть назначен параметру типа 'Cow'консоль . журнал ( eatEgg ( animalToFood ( курица )));  // Я съел яйцо.//console.log(eatEgg(animalToFood(cow))); // ОШИБКА: аргумент типа 'Milk' не может быть назначен параметру типа 'Egg'консоль . журнал ( drinkMilk ( animalToFood ( cow )));  // Я выпил молока.//console.log(drinkMilk(animalToFood(chicken))); // ОШИБКА: аргумент типа «Яйцо» нельзя присвоить параметру типа «Молоко»

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

• Строки 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.

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

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

Сравнение с шаблоном посетителя [ править ]

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

Ограничения [ править ]

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

Зависимый тип перекрестка [ править ]

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

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

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

черт  свидетель  {  типа  Т  Val  значение :  Т  {} }

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

объект  booleanWitness  расширяет  свидетеля  {  type  T  =  Boolean  val  value  =  true }

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

В качестве альтернативы, приведенный выше минималистичный пример можно описать с использованием зависимых типов записей . ^[10] По сравнению с зависимыми типами пересечений, зависимые типы записей представляют собой строго более специализированное теоретическое понятие типов. ^[6]

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

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

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

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