Ограниченная квантификация

В теории типов ограниченная квантификация (также ограниченный полиморфизм или ограниченная генеративность ) относится к универсальным или экзистенциальным квантификаторам , которые ограничены («ограничены») диапазоном только по подтипам определенного типа. Ограниченная квантификация представляет собой взаимодействие параметрического полиморфизма с подтипированием . Ограниченная квантификация традиционно изучалась в функциональной настройке System F _<: , но доступна в современных объектно-ориентированных языках, поддерживающих параметрический полиморфизм ( генерики ), таких как Java , C# и Scala .

Цель ограниченной квантификации — разрешить полиморфным функциям зависеть от некоторого конкретного поведения объектов вместо наследования типов . Она предполагает модель на основе записей для классов объектов, где каждый член класса является элементом записи, а все члены класса являются именованными функциями. Атрибуты объектов представлены как функции, которые не принимают аргументов и возвращают объект. Конкретное поведение тогда представляет собой некоторое имя функции вместе с типами аргументов и типом возвращаемого значения. Ограниченная квантификация рассматривает все объекты с такой функцией. Примером может служить полиморфная minфункция, которая рассматривает все объекты, которые сопоставимы друг с другом. ^{[ необходима цитата ]}

F -ограниченная квантификация или рекурсивно ограниченная квантификация , введенная в 1989 году, позволяет более точно типизировать функции, применяемые к рекурсивным типам. Рекурсивный тип — это тип, включающий функцию, которая использует его как тип для некоторого аргумента или его возвращаемого значения. ^[1]

Этот тип ограничения типа может быть выражен в Java с помощью универсального интерфейса. Следующий пример демонстрирует, как описывать типы, которые можно сравнивать друг с другом, и использовать это в качестве информации о типизации в полиморфных функциях . Test.minФункция использует простую ограниченную квантификацию и не гарантирует, что объекты будут взаимно сопоставимы, в отличие от Test.fMinфункции, которая использует F-ограниченную квантификацию.

В математической нотации типы двух функций следующие:

min: ∀ T, ∀ S ⊆ {compareTo: T → int}. S → S → S

fMin: ∀ T ⊆ Comparable[T]. T → T → T

где

Сравнимое[T] = {сравнитьС: T → int}

Интерфейс  Сопоставимый < T > {  int compareTo ( T other );  }открытый класс Integer реализует Comparable < Integer > {      @Override public int compareTo ( Integer other ) { // ... } }       Открытый класс String реализует Comparable < String > {      @Override public int compareTo ( String other ) { // ... }       }public class Test { public static void main ( String [] args ) { final String a = min ( "cat" , "dog" ); final Integer b = min ( 10 , 3 ); final Comparable c = min ( "cat" , 3 ); // Выдает ClassCastException во время выполнения final String str = fMin ( "cat" , "dog" ); final Integer i = fMin ( 10 , 3 ); // final Object o = fMin( "cat", 3); // Не компилируется } public static < S extends Comparable > S min ( S a , S b ) { if ( a . compareTo ( b ) <= 0 ) { return a ; } else { return b ; } } public static < T extends Comparable < T >> T fMin ( T a , T b ) { if ( a . comparableTo ( b ) <= 0 ) { return a ; } else { return b ; } }                                                                                               }

• Ковариантность и контравариантность (информатика)
• Любопытно повторяющийся шаблонный узор
• Подстановочный знак (Java)

• Карделли, Лука ; Вегнер, Питер (декабрь 1985 г.). «О понимании типов, абстракции данных и полиморфизма» (PDF) . ACM Computing Surveys . 17 (4): 471– 523. CiteSeerX  10.1.1.117.695 . doi :10.1145/6041.6042. ISSN  0360-0300. S2CID  2921816.
• Питер С. Каннинг, Уильям Р. Кук , Уолтер Л. Хилл, Джон К. Митчелл и Уильям Олтофф. "F-ограниченный полиморфизм для объектно-ориентированного программирования". На конференции по языкам функционального программирования и архитектуре компьютеров , 1989.
• Бенджамин К. Пирс "Типы пересечений и ограниченный полиморфизм". Конспект лекций по информатике 664 , 1993.
• Гилад Браха , Мартин Одерски , Дэвид Стаутэмайр и Филип Вадлер . «Сделаем будущее безопасным для прошлого: добавление универсальности к языку программирования Java». В Object-Oriented Programming: Systems, Languages, Applications (OOPSLA). ACM, октябрь 1998 г.
• Эндрю Кеннеди и Дон Сайм . «Проектирование и реализация универсальных шаблонов для среды выполнения .NET Common Language Runtime». В Programming Language Design and Implementation , 2001.
• Пирс, Бенджамин С. (2002). Типы и языки программирования . MIT Press. ISBN 978-0-262-16209-8., Глава 26: Ограниченная квантификация

• Ограниченный полиморфизм в репозитории шаблонов Портленда
• «F-ограниченный полиморфизм» в языке Сесила: спецификация и обоснование