Обобщённый алгебраический тип да́нных () — один из видов алгебраических типов данных, который характеризуется тем, что его конструкторы могут возвращать значения не своего типа, связанного с ним. Сконструированы под влиянием работ об индуктивных семействах в среде исследователей зависимых типов.
Такие типы реализованы в нескольких языках программирования, в частности в языках OCaml (начиная с версии 4), Idris, Agda и Haskell, причём в последнем оно не входит в стандарт языка, а реализовано только в одном из расширений компилятора GHC. Язык Haskell имитирует , представляя их типами, индексированными другими типами.
Применяются в обобщённом программировании, моделировании языков программирования и моделировании объектов, сохранении инвариантов структур данных, выражении ограничений во встроенных предметно-ориентированных языках.
История Ранняя версия обобщённых алгебраических типов данных была описана Леннартом Аугустсоном и Кентом Петерсоном в 1994 году и основывалась на сопоставлении с образцом в системе доказательства теорем ALF.
В современной форме GADT были введены в 2003 году независимо Чейни () и Хинце () и до этого Си (), Ченом () и Ченом () как расширения алгебраических типов данных ML и Haskell. Введённые обобщённые типы оказались эквивалентны друг другу и похожи на индуктивные семейства типов данных (или индуктивные типы данных), используемые в Coq в исчислении конструкций.
В 2006 году разработаны расширенные алгебраические типы данных, сочетающие обобщённые алгебраические типы данных с и ограничениями , введёнными Перри (), Ляуфером () и Одерски в середине 1990-х годов.
Вывод типов при отсутствии деклараций типов, заданных программистом, является алгоритмически неразрешимой задачей, а функции, определённые на обобщённых АТД, в общем случае могут не принимать .
Реконструкция типа требует при проектировании нескольких компромиссов и является по состоянию на 2011 год темой исследований.
Пример на Haskell В следующем примере определяется обобщённый тип Type, в котором представлены несколько типов:
data Type :: * -> * where Char :: Type Char Int :: Type Int List :: Type a -> Type [a]
Для этого типа можно составить ad-hoc-полиморфную функцию суммирования:
sum :: Type a -> a -> Int sum Char _ = 0 sum Int n = n sum (List a) xs = foldr (+) 0 (map (sum a) xs)
Которую можно применять для типов, поддерживаемых Type, например, для типа [Int]:
sum (List Int) [1, 2, 4]
Примечания
Литература
__NOTOC__ Категория:Функциональное программирование Категория:Типы данных Категория:Программирование с зависимыми типами Категория:Составные типы данных