Обобщённый алгебраический тип да́нных (англ. generalized algebraic data type, GADT) — один из видов алгебраических типов данных, который характеризуется тем, что его конструкторы могут возвращать значения не своего типа, связанного с ним[1]. Сконструированы под влиянием работ об индуктивных семействах в среде исследователей зависимых типов[2].
Такие типы реализованы в нескольких языках программирования, в частности в языках OCaml (начиная с версии 4)[3], Idris[4], Agda[5] и Haskell, причём в последнем оно не входит в стандарт языка, а реализовано только в одном из расширений компилятора GHC. Язык Haskell имитирует индуктивное семейство (англ. inductive family), представляя их типами, индексированными другими типами[5].
Применяются в обобщённом программировании, моделировании абстрактного синтаксиса высшего порядка (англ. higher-order abstract syntax) языков программирования и моделировании объектов, сохранении инвариантов структур данных, выражении ограничений во встроенных предметно-ориентированных языках[6].
Ранняя версия обобщённых алгебраических типов данных была описана Леннартом Аугустсоном и Кентом Петерсоном в 1994 году и основывалась на сопоставлении с образцом в системе доказательства теорем ALF[7].
В современной форме GADT были введены в 2003 году независимо Чейни (Cheney) и Хинце (Hinze) и до этого Си (Xi), Ченом (Chen) и Ченом (Chen) как расширения алгебраических типов данных ML и Haskell[8][9]. Введённые обобщённые типы оказались эквивалентны друг другу и похожи на индуктивные семейства типов данных (или индуктивные типы данных), используемые в Coq в исчислении конструкций[10].
В 2006 году разработаны расширенные алгебраические типы данных, сочетающие обобщённые алгебраические типы данных с экзистенциальными типами данных[en] и ограничениями класса типов[en], введёнными Перри (Perry), Ляуфером (Läufer) и Одерски в середине 1990-х годов.
Вывод типов при отсутствии деклараций типов, заданных программистом, является алгоритмически неразрешимой задачей, а функции, определённые на обобщённых АТД, в общем случае могут не принимать основные типы (англ. principal type)[11][12].
Реконструкция типа требует при проектировании нескольких компромиссов и является по состоянию на 2011 год темой исследований.
В следующем примере определяется обобщённый тип Type
, в котором представлены несколько типов[13]:
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]
Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".
Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.
Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .