В информатике класс типов — это конструкция системы типов , которая поддерживает полиморфизм ad hoc . Это достигается путем добавления ограничений к переменным типов в параметрически полиморфных типах. Такое ограничение обычно включает класс типов Tи переменную типов a и означает, что aможет быть инстанциировано только для типа, члены которого поддерживают перегруженные операции, связанные с T.
Классы типов были впервые реализованы в языке программирования Haskell после того, как были впервые предложены Филиппом Вадлером и Стивеном Блоттом в качестве расширения «eqtypes» в Standard ML , [1] [2] и изначально были задуманы как способ реализации перегруженных арифметических операторов и операторов равенства в принципиальной манере. [3] [2] В отличие от «eqtypes» Standard ML, перегрузка оператора равенства посредством использования классов типов в Haskell не требует обширной модификации интерфейса компилятора или базовой системы типов. [4]
Классы типов определяются путем указания набора имен функций или констант вместе с их соответствующими типами, которые должны существовать для каждого типа, принадлежащего классу. В Haskell типы могут быть параметризованы; класс типов, Eqпредназначенный для содержания типов, которые допускают равенство, будет объявлен следующим образом:
класс Eq a где ( == ) :: a -> a -> Bool ( /= ) :: a -> a -> Bool где a— один экземпляр класса типа Eq, и aопределяет сигнатуры функций для 2 функций (функций равенства и неравенства), каждая из которых принимает 2 аргумента типа aи возвращает логическое значение.
Переменная типа aимеет вид ( также известна как в последней версии Glasgow Haskell Compiler (GHC)), [5] что означает, что вид равенTypeEq
Eq :: Тип -> Ограничение Декларацию можно читать как утверждение, что «тип aпринадлежит классу типов, Eqесли для него определены функции с именами (==), и (/=), соответствующих типов». Затем программист может определить функцию elem(которая определяет, находится ли элемент в списке) следующим образом:
elem :: Eq a => a -> [ a ] -> Bool elem y [] = False elem y ( x : xs ) = ( x == y ) || элемент y хз Функция elemимеет тип a -> [a] -> Boolс контекстом Eq a, который ограничивает типы, которые aмогут варьироваться до тех, aкоторые принадлежат классу Eqтипов. (Haskell => можно назвать «ограничением класса».)
Любой тип tможет быть сделан членом заданного класса типов Cс помощью объявления экземпляра , которое определяет реализации всех Cметодов для конкретного типа t. Например, если tопределен новый тип данных, этот новый тип может быть сделан экземпляром Eq, предоставив функцию равенства над значениями типа tлюбым полезным способом. После этого функцию elemможно использовать на [t], то есть списках элементов типа t.
Классы типов отличаются от классов в объектно-ориентированных языках программирования. В частности, Eqне является типом: не существует такого понятия, как значение типа Eq.
Классы типов тесно связаны с параметрическим полиморфизмом . Например, тип, elemуказанный выше, был бы параметрически полиморфным типом, a -> [a] -> Boolесли бы не ограничение класса типов " Eq a =>".
Класс типа не обязательно должен принимать переменную типа kind Type , но может принимать переменную любого типа. Такие классы типов с более высокими видами иногда называются классами-конструкторами (конструкторы, о которых идет речь, являются конструкторами типов, такими как Maybe, а не конструкторами данных, такими как Just). Примером может служить Monadкласс:
класс Монада m, где return :: a -> m a ( >>= ) :: m a -> ( a -> m b ) -> m b То, что m применяется к переменной типа, указывает на то, что она имеет вид Type -> Type, т.е. она принимает тип и возвращает тип, вид которого Monadследующий:
Монада :: ( Тип -> Тип ) -> Ограничение Классы типов допускают множественные параметры типа, и поэтому классы типов можно рассматривать как отношения типов. [6] Например, в стандартной библиотеке GHC класс выражает общий неизменяемый интерфейс массива. В этом классе ограничение класса типа означает, что это тип массива, содержащий элементы типа . (Это ограничение полиморфизма используется для реализации неупакованных типов массивов, например.)IArrayIArray a eae
Как и мультиметоды , [ требуется ссылка ] многопараметрические классы типов поддерживают вызов различных реализаций метода в зависимости от типов множественных аргументов и, конечно, возвращают типы. Многопараметрические классы типов не требуют поиска метода для вызова при каждом вызове во время выполнения; [7] : минута 25:12 вместо этого вызываемый метод сначала компилируется и сохраняется в словаре экземпляра класса типа, как и в случае с однопараметрическими классами типов.
Код Haskell, использующий многопараметрические классы типов, непереносим, поскольку эта функция не является частью стандарта Haskell 98. Популярные реализации Haskell, GHC и Hugs , поддерживают многопараметрические классы типов.
В Haskell классы типов были усовершенствованы, чтобы позволить программисту объявлять функциональные зависимости между параметрами типов — концепция, вдохновленная теорией реляционных баз данных . [8] [9] То есть, программист может утверждать, что заданное назначение некоторого подмножества параметров типа однозначно определяет оставшиеся параметры типа. Например, общая монада m , которая несет параметр состояния типа, sудовлетворяет ограничению класса типа Monad.State s m. В этом ограничении есть функциональная зависимость m -> s. Это означает, что для заданной монады mтипа класса Monad.Stateтип состояния, доступный из которого, mоднозначно определен. Это помогает компилятору в выводе типов , а также помогает программисту в программировании, ориентированном на типы.
Саймон Пейтон Джонс возражал против введения функциональных зависимостей в Haskell по причине их сложности. [10]
Классы типов и неявные параметры очень похожи по своей природе, хотя и не совсем одинаковы. Полиморфная функция с ограничением класса типа, например:
сумма :: Число а => [ а ] -> а можно интуитивно рассматривать как функцию, которая неявно принимает экземпляр Num:
сумма_ :: Число_ а -> [ а ] -> а Экземпляр Num_ aпо сути является записью, содержащей определение экземпляра Num a. (Фактически именно так классы типов реализуются под капотом компилятора Glasgow Haskell.)
Однако есть важное отличие: неявные параметры более гибкие ; могут передаваться различные экземпляры Num Int. Напротив, классы типов обеспечивают так называемое свойство согласованности , которое требует, чтобы для любого заданного типа был только один уникальный выбор экземпляра. Свойство согласованности делает классы типов несколько антимодулярными, поэтому сиротские экземпляры (экземпляры, которые определены в модуле, который не содержит ни класс, ни тип интереса) настоятельно не приветствуются. Однако согласованность добавляет еще один уровень безопасности к языку, предоставляя гарантию того, что две непересекающиеся части одного и того же кода будут совместно использовать один и тот же экземпляр. [11]
Например, упорядоченный набор (типа Set a) требует полного упорядочения элементов (типа a) для функционирования. Это может быть подтверждено ограничением Ord a, которое определяет оператор сравнения для элементов. Однако может быть множество способов наложить полный порядок. Поскольку алгоритмы наборов, как правило, нетерпимы к изменениям в порядке после построения набора, передача несовместимого экземпляра функциям Ord a, которые работают с набором, может привести к неверным результатам (или сбоям). Таким образом, обеспечение согласованности Ord aв этом конкретном сценарии имеет решающее значение.
Экземпляры (или «словари») в классах типов Scala — это просто обычные значения в языке, а не совершенно отдельный вид сущности. [12] [13] Хотя эти экземпляры по умолчанию предоставляются путем поиска соответствующих экземпляров в области видимости для использования в качестве неявных параметров для явно объявленных неявных формальных параметров, то, что они являются обычными значениями, означает, что они могут быть предоставлены явно для разрешения неоднозначности. В результате классы типов Scala не удовлетворяют свойству согласованности и фактически являются синтаксическим сахаром для неявных параметров.
Это пример, взятый из документации Cats: [14]
// Класс типа для предоставления текстового представления trait Show [ A ] { def show ( f : A ): String } // Полиморфная функция, которая работает только при наличии неявного // экземпляра Show[A] def log [ A ]( a : A )( implicit s : Show [ A ]) = println ( s . show ( a )) // Экземпляр для String неявный val stringShow = new Show [ String ] { def show ( s : String ) = s } // Параметр stringShow был вставлен компилятором. scala > log ( "a string" ) a string Coq (версия 8.2 и выше) также поддерживает классы типов, выводя соответствующие экземпляры. [15] Последние версии Agda 2 также предоставляют похожую функцию, называемую «аргументами экземпляра». [16]
В Standard ML механизм «типов равенства» примерно соответствует встроенному классу типов Haskell Eq, но все операторы равенства автоматически выводятся компилятором. Контроль программиста над процессом ограничивается указанием того, какие компоненты типа в структуре являются типами равенства, а какие переменные типа в полиморфном диапазоне типов по типам равенства.
Модули и функторы SML и OCaml могут играть роль, похожую на роль классов типов Haskell, при этом принципиальное отличие заключается в роли вывода типов, что делает классы типов подходящими для ad hoc полиморфизма. [17] Объектно-ориентированное подмножество OCaml — это еще один подход, который в некоторой степени сопоставим с подходом классов типов.
Аналогичное понятие для перегруженных данных (реализованное в GHC ) — это семейство типов . [18]
В C++ , особенно в C++20 , есть поддержка классов типов с использованием Концепций (C++) . В качестве иллюстрации, вышеупомянутый пример класса типов Eq на Haskell можно записать как
template < typename T > concept Equal = required ( T a , T b ) { { a == b } -> std :: convertible_to < bool > ; { a != b } -> std :: convertible_to < bool > ; }; В Clean классы типов похожи на Haskell, но имеют немного другой синтаксис .
Rust поддерживает черты , которые являются ограниченной формой классов типов с когерентностью. [19]
В Mercury есть классы типов, хотя они не совсем такие же, как в Haskell. [ необходимы дополнительные пояснения ]
В Scala классы типов — это идиома программирования , которая может быть реализована с помощью существующих языковых возможностей, таких как неявные параметры, а не отдельная языковая возможность как таковая. Благодаря тому, как они реализованы в Scala, можно явно указать, какой экземпляр класса типа использовать для типа в определенном месте кода в случае неоднозначности. Однако это не обязательно является преимуществом, поскольку неоднозначные экземпляры классов типов могут быть подвержены ошибкам.
Помощник по доказательству Coq также поддерживает классы типов в последних версиях. В отличие от обычных языков программирования, в Coq любые законы класса типов (например, законы монад), указанные в определении класса типов, должны быть математически доказаны для каждого экземпляра класса типов перед их использованием.
Data.Kindпоявился в версии 8 компилятора Glasgow Haskell