Обобщённый алгебраический тип да́нных ( англ. generalized algebraic data type, GADT ) — один из видов алгебраических типов данных , который характеризуется тем, что его конструкторы могут возвращать значения не своего типа, связанного с ним . Сконструированы под влиянием работ об индуктивных семействах в среде исследователей зависимых типов .

Такие типы реализованы в нескольких языках программирования, в частности в языках OCaml (начиная с версии 4) , Idris , Agda и Haskell , причём в последнем оно не входит в стандарт языка, а реализовано только в одном из расширений компилятора GHC . Язык Haskell имитирует ( англ. ), представляя их типами, индексированными другими типами .

Применяются в обобщённом программировании , моделировании ( англ. ) языков программирования и моделировании объектов, сохранении инвариантов структур данных , выражении ограничений во встроенных предметно-ориентированных языках .

История

Ранняя версия обобщённых алгебраических типов данных была описана Леннартом Аугустсоном и Кентом Петерсоном в 1994 году и основывалась на сопоставлении с образцом в системе доказательства теорем ALF .

В современной форме GADT были введены в 2003 году независимо Чейни ( Cheney ) и Хинце ( Hinze ) и до этого Си ( Xi ), Ченом ( Chen ) и Ченом ( Chen ) как расширения алгебраических типов данных ML и Haskell . Введённые обобщённые типы оказались эквивалентны друг другу и похожи на индуктивные семейства типов данных (или индуктивные типы данных), используемые в Coq в исчислении конструкций .

В 2006 году разработаны расширенные алгебраические типы данных, сочетающие обобщённые алгебраические типы данных с и ограничениями , введёнными Перри ( Perry ), Ляуфером ( Läufer ) и Одерски в середине 1990-х годов.

Вывод типов при отсутствии деклараций типов, заданных программистом, является алгоритмически неразрешимой задачей , а функции, определённые на обобщённых АТД, в общем случае могут не принимать ( англ. ) .

Реконструкция типа требует при проектировании нескольких компромиссов и является по состоянию на 2011 год темой исследований.

Пример на Haskell

В следующем примере определяется обобщённый тип Type , в котором представлены несколько типов :

data Type :: * -> * where
    Char :: Type Char
    Int :: Type Int
    List :: Type a -> Type [a]

Для этого типа можно составить функцию суммирования:

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]

Примечания

Литература

• Koopman, P.; Plasmeijer, R.; Swierstra, D. Advanced Functional Programming: 6th International School, AFP 2008, Heijen, The Netherlands, May 19-24, 2008, Revised Lectures. — Springer, 2009. — 331 p. — ISBN 9783642046513 .
• Peyton Jones, Simon; Washburn, Geoffrey; Weirich, Stephanie. (англ.) // Technical Report MS-CIS-05-25. — University of Pennsylvania, 2004.
• Augustsson, Lennart; Petersson, Kent. (англ.) . — 1994.
• Cheney, James; Hinze, Ralf. First-Class Phantom Types (англ.) // Technical Report CUCIS TR2003-1901. — Cornell University, 2003.
• Xi, Hongwei; Chen, Chiyan; Chen, Gang. Guarded Recursive Datatype Constructors (англ.) // Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'03). — ACM Press, 2003. — P. 224–235 . — doi : .
• Sheard, Tim; Pasalic, Emir. Meta-programming with built-in type equality (англ.) // Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork. — 2004. — doi : .
• Schmid, U. and Kitzelmann, E. and Plasmeijer, R. Approaches and Applications of Inductive Programming: Third International Workshop, AAIP 2009, Edinburgh, UK, September 4, 2009, Revised Papers. — Springer, 2010. — P. 114—115. — ISBN 9783642119309 .
• Peyton Jones, Simon; Vytiniotis, Dimitrios; Weirich, Stephanie; Washburn, Geoffrey. (англ.) // Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland. — 2006.
• Schrijvers, Tom, Peyton Jones, Simon, Sulzmann, Martin, Vytiniotis, Dimitrios. (англ.) // Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh. — 2009.