Тип класса

Эта статья о системах полиморфного типа в информатике. О математическом классе типов порядка заданной мощности см. Глоссарий теории множеств § T .

Не путать с классом (компьютерное программирование) .

В информатике класс типов — это конструкция системы типов , поддерживающая специальный полиморфизм . Это достигается за счет добавления ограничений на переменные типа в параметрически полиморфных типах. Такое ограничение обычно включает класс типа T и переменная типа aи означает, что a может быть создан только тип, члены которого поддерживают перегруженные операции, связанные с T.

Классы типов были впервые реализованы на языке программирования Haskell после того, как их впервые предложили Филип Уодлер и Стивен Блотт в качестве расширения «eqtypes» в Standard ML . способ реализации перегруженных арифметических операций и операторов равенства . и изначально были задуманы как принципиальный В отличие от «eqtypes» Standard ML, перегрузка оператора равенства посредством использования классов типов в Haskell не требует обширной модификации интерфейса компилятора или базовой системы типов.

Обзор

Классы типов определяются путем указания набора имен функций или констант вместе с соответствующими типами, которые должны существовать для каждого типа, принадлежащего классу. В Haskell типы можно параметризовать; класс типа Eq предназначенный для содержания типов, допускающих равенство, будет объявлен следующим образом:

class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool

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

Переменная типа a имеет вид $*$ ( $*$ также известен как Type в последней версии GHC ), означает, что вид Eq является

Eq :: Type -> Constraint

Объявление можно прочитать как указание «типа a принадлежит классу типов Eq если есть функции с именем (==), и (/=), соответствующих типов, определенных на нем». Затем программист может определить функцию elem (который определяет, находится ли элемент в списке) следующим образом:

elem :: Eq a => a -> [a] -> Bool
elem y []     = False
elem y (x:xs) = (x == y) || elem y xs

Функция elem имеет тип a -> [a] -> Bool с контекстом Eq a, который ограничивает типы, которые a может варьироваться от тех a которые принадлежат к Eq тип класса. ( Примечание : Хаскель => можно назвать «ограничением класса».)

Программист может сделать любой тип t член данного класса типов C используя объявление экземпляра , которое определяет реализации всех C' методы для конкретного типа t. Например, если программист определяет новый тип данных t, они могут затем сделать этот новый тип экземпляром Eq предоставляя функцию равенства значений типа t любым способом, который они считают нужным. Как только они это сделают, они могут использовать функцию elem на [t], то есть списки элементов типа t.

Обратите внимание, что классы типов отличаются от классов объектно-ориентированных языков программирования. В частности, Eq не является типом: не существует такого понятия, как значение типа. Eq.

Классы типов тесно связаны с параметрическим полиморфизмом. Например, обратите внимание, что тип elem как указано выше, это будет параметрически полиморфный тип. a -> [a] -> Bool если бы не ограничение класса типа " Eq a =>".

Полиморфизм высшего рода

Класс типа не обязательно должен принимать переменную типа вида Type но могу взять любой. Эти классы типов более высоких типов иногда называются классами-конструкторами (конструкторы, о которых идет речь, являются конструкторами типов, такими как Maybe, а не конструкторы данных, такие как Just). Примером является Monad сорт:

class Monad m where
  return :: a -> m a
  (>>=)  :: m a -> (a -> m b) -> m b

Тот факт, что m применяется к переменной типа, указывает на то, что она имеет вид Type -> Type, то есть он принимает тип и возвращает тип, вид Monad таким образом:

Monad :: (Type -> Type) -> Constraint

Классы типов с несколькими параметрами

Классы типов допускают несколько параметров типа, поэтому классы типов можно рассматривать как отношения к типам. Например, в стандартной библиотеке GHC класс IArray выражает общий интерфейс неизменяемого массива. В этом классе ограничение класса типа IArray a e означает, что a это тип массива, который содержит элементы типа e. (Это ограничение на полиморфизм используется для реализации неупакованных , например, типов массивов.)

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

Код Haskell, использующий классы типов с несколькими параметрами, не является переносимым, поскольку эта функция не является частью стандарта Haskell 98. Популярные реализации Haskell, GHC и Hugs , поддерживают классы типов с несколькими параметрами.

Функциональные зависимости

В Haskell классы типов были усовершенствованы, чтобы позволить программисту объявлять функциональные зависимости между параметрами типа — концепция, вдохновленная теорией реляционных баз данных . То есть программист может утверждать, что данное присвоение некоторого подмножества параметров типа однозначно определяет остальные параметры типа. Например, общая монада m который несет параметр состояния типа s удовлетворяет ограничению класса типа Monad.State s m. В этом ограничении существует функциональная зависимость m -> s. Это означает, что для данной монады m типа класса Monad.State, тип состояния, доступный из m определяется однозначно. Это помогает компилятору в выводе типа , а также помогает программисту в типизированном программировании .

Саймон Пейтон-Джонс возражал против введения функциональных зависимостей в Haskell по причине сложности.

Классы типов и неявные параметры

Классы типов и неявные параметры очень похожи по своей природе, хотя и не совсем одинаковы. Полиморфная функция с ограничением класса типа, например:

sum :: Num a => [a] -> a

можно интуитивно рассматривать как функцию, которая неявно принимает экземпляр Num:

sum_ :: Num_ a -> [a] -> a

Экземпляр Num_ a по сути, это запись, содержащая определение экземпляра Num a. (Фактически именно так классы типов реализуются под капотом компилятора Glasgow Haskell.)

Однако есть принципиальная разница: неявные параметры более гибкие — вы можете передавать разные экземпляры. Num Int. Напротив, классы типов реализуют так называемое свойство согласованности , которое требует, чтобы для любого данного типа был только один уникальный выбор экземпляра. Свойство когерентности делает классы типов в некоторой степени антимодульными, поэтому настоятельно не рекомендуется использовать потерянные экземпляры (экземпляры, определенные в модуле, который не содержит ни класс, ни интересующий тип). С другой стороны, согласованность добавляет языку дополнительный уровень безопасности, давая программисту гарантию того, что две непересекающиеся части одного и того же кода будут использовать один и тот же экземпляр.

Например, упорядоченный набор (типа Set a) требует полного упорядочения элементов (типа a), чтобы функционировать. Об этом может свидетельствовать ограничение Ord a, который определяет оператор сравнения элементов. Однако существует множество способов навести полный порядок. Поскольку алгоритмы множеств обычно нетерпимы к изменениям порядка после создания набора, передача несовместимого экземпляра Ord a к функциям, которые работают на наборе, может привести к неверным результатам (или сбоям). Таким образом, обеспечение согласованности Ord a в этом конкретном сценарии имеет решающее значение.

Экземпляры (или «словари») в классах типов Scala — это просто обычные значения языка, а не совершенно отдельный вид сущностей. Хотя эти экземпляры по умолчанию предоставляются путем поиска соответствующих экземпляров в области видимости, которые будут использоваться в качестве неявных фактических параметров для явно объявленных неявных формальных параметров, тот факт, что они являются обычными значениями, означает, что они могут быть предоставлены явно, чтобы устранить неоднозначность. В результате классы типов Scala не удовлетворяют свойству связности и фактически являются синтаксическим сахаром для неявных параметров.

Это пример из группы Cats. документация:

// A type class to provide textual representation
trait Show[A] {
  def show(f: A): String
}

// A polymorphic function that works only when there is an implicit 
// instance of Show[A] available
def log[A](a: A)(implicit s: Show[A]) = println(s.show(a))

// An instance for String
implicit val stringShow = new Show[String] {
  def show(s: String) = s
}

// The parameter stringShow was inserted by the compiler.
scala> log("a string")
a string

Coq (версия 8.2 и более поздние) также поддерживает классы типов, выводя соответствующие экземпляры. Последние версии Agda 2 также предоставляют аналогичную функцию, называемую «аргументами экземпляра».

к

В Standard ML механизм «типов равенства» примерно соответствует встроенному классу типов Haskell. Eq, но все операторы равенства автоматически выводятся компилятором. Контроль над процессом со стороны программиста ограничивается указанием того, какие компоненты типов в структуре являются типами равенства, а переменные каких типов в диапазоне полиморфных типов превышают типы равенства.

Модули и функторы SML и OCaml могут играть роль, аналогичную роли классов типов Haskell, причем принципиальным отличием является роль вывода типа, что делает классы типов пригодными для специального полиморфизма. Объектно-ориентированное подмножество OCaml — это еще один подход, который в некоторой степени сравним с подходом к классам типов.

Связанные понятия

Аналогичным понятием для перегруженных данных (реализованным в GHC ) является семейство типов .

В C++, в частности, в C++20 имеется поддержка классов типов с использованием Concepts (C++) . В качестве иллюстрации приведенный выше пример класса типов Eq на Haskell можно записать как

template <typename T>
concept Equal =
      requires (T a, T b) {
            { a == b } -> std::convertible_to<bool>;
            { a != b } -> std::convertible_to<bool>;
};

Классы типов в Clean похожи на Haskell, но имеют немного другой синтаксис.

Rust поддерживает типажи , которые представляют собой ограниченную форму согласованных классов типов.

В Mercury есть классы типов, хотя они не совсем такие, как в Haskell.

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

Помощник по доказательству Coq также поддерживает классы типов в последних версиях. В отличие от обычных языков программирования, в Coq любые законы класса типов (например, законы монады), изложенные в определении класса типов, должны быть математически доказаны для каждого экземпляра класса типов перед их использованием.

См. также

• Полиморфизм (информатика) (другие виды полиморфизма)
• Язык программирования Haskell (язык, на котором впервые были разработаны классы типов)
• Перегрузка операторов (одно применение классов типов)
• Монада (функциональное программирование) ( Monad это пример класса типа)
• Концепции (C++) (начиная с C++20)
• Руст (язык программирования)

Ссылки

• Пейтон Джонс, Саймон; Джонс, Марк; Мейер, Эрик (май 1997 г.). «Тип-классы: исследование пространства дизайна» . Учеб. Семинар по Haskell ACM SIGPLAN . CiteSeerX   10.1.1.1085.8703 .

Внешние ссылки

• «5. Классы типов и перегрузка» . Небольшое введение в Haskell . Июнь 2000 г. Версия 98.
• Курс продвинутого функционального программирования в Утрехтском университете, 74 слайда лекций по классам продвинутого типа . 07.06.2005.
• Реализация и понимание классов типов . 13 ноября 2014 г.