Обобщённый алгебраический тип данных

Обобщённый алгебраический тип да́нных (англ. 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 году разработаны расширенные алгебраические типы данных, сочетающие обобщённые алгебраические типы данных с экзистенциальными типами данных и ограничениями класса типов, введёнными Перри (Perry), Ляуфером (Läufer) и Одерски в середине 1990-х годов.

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

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

Пример на Haskell

В следующем примере определяется обобщённый тип 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]

Примечания
  1. Koopman, Plasmeijer, Swierstra, 2009, pp. 178—179.
  2. Schmid, Kitzelmann, Plasmeijer, 2010.
  3. Xavier Leroy. The state of OCaml, 2012 (англ.) (недоступная ссылка). OCaml Users and Developers Workshop 4 (14 сентября 2012). Дата обращения: 13 декабря 2014. Архивировано 2 января 2015 года.
  4. Idris Example
  5. Bove, Ana and Dybjer, Peter and Norell, Ulf (2009). «A Brief Overview of Agda --- A Functional Language with Dependent Types» in TPHOLs '09. Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics: 73—78, Munich, Germany: Springer-Verlag. DOI:10.1007/978-3-642-03359-9_6. Bove:2009:BOA:1616077.1616085. Дата обращения: 2013-12-06.
  6. Peyton Jones, Washburn, Weirich, 2004.
  7. Augustsson, Petersson, 1994.
  8. Cheney, Hinze, 2003, p. 25.
  9. Xi, Chen, Chen, 2003.
  10. Cheney, Hinze, 2003, p. 25—26.
  11. Peyton Jones, Washburn, Weirich, 2004, p. 7.
  12. Schrijvers, Peyton Jones, Sulzmann, Vytiniotis, 2009.
  13. Hagiya, M. and Wadler, P. Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings. — Springer, 2006. — P. 17—18. — ISBN 9783540334385.

Литература
  • 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. Wobbly types: type inference for generalised algebraic data types (англ.) // Technical Report MS-CIS-05-25. — University of Pennsylvania, 2004.
  • Augustsson, Lennart; Petersson, Kent. Silly type families (англ.). — 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:10.1145/604131.604150.
  • 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:10.1016/j.entcs.2007.11.012.
  • 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. Simple Unification-based Type Inference for GADTs (англ.) // Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland. — 2006.
  • Schrijvers, Tom, Peyton Jones, Simon, Sulzmann, Martin, Vytiniotis, Dimitrios. Complete and Decidable Type Inference for GADTs (англ.) // Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh. — 2009.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.