Узагальнений алгебричний тип даних

Узага́льнений алгебри́чний тип да́них (англ. generalized algebraic data type, GADT) — один з видів алгебричних типів даних, який характеризується тим, що його конструктори можуть повертати значення не свого типу, пов'язаного з ним[1]. Створені під впливом робіт про індуктивні сімейства серед дослідників залежних типів[2].

Такі типи реалізовано в кількох мовах програмування, зокрема в мовах OCaml (починаючи від версії 4)[3], Idris[4], Agda[5] та Haskell, причому в останньому вони не входять до стандарту мови, а реалізовані лише в одному з розширень компілятора GHC. Мова Haskell імітує індуктивне сімейство[en], подаючи їх типами, індексованими іншими типами[5].

Застосовуються в узагальненому програмуванні, моделюванні абстрактного синтаксису вищого порядку[en] мов програмування та моделювання об'єктів, збереженні інваріантів структур даних, вираженні обмежень у вбудованих предметно-орієнтованих мовах[6].

Історія

Рання версія узагальнених алгебричних типів даних, яку описали Леннарт Аугустсон і Кент Петерсон 1994 року, ґрунтувалася на зіставленні зі взірцем у системі доведення теорем ALF[7].

У сучасній формі GADT ввели 2003 року незалежно Чейні (Cheney) та Гінц (Hinze) і до цього Сі (Xi), Чен (Chen) і Ченом (Chen) як розширення алгебричних типів даних ML і Haskell[8][9]. Введені узагальнені типи виявилися еквівалентними один одному і схожі на індуктивні сімейства типів даних (або індуктивні типи даних), використовувані в Coq у численні конструкцій [10] .

2006 року розроблено розширені алгебричні типи даних, що поєднують узагальнені алгебричні типи даних з екзистенційними типами даних[en] та обмеженнями класу типів[en], які ввели Перрі (Perry), Ляуфер (Läufer) і Одерски в середині 1990-х.

Вивід типів за відсутності оголошень типів, заданих програмістом, є алгоритмічно нерозв'язною задачею, а функції, визначені на узагальнених АТД, у загальному випадку можуть не приймати основних типів[en][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, с. 178—179.
  2. ↑ Schmid, Kitzelmann, Plasmeijer, 2010.
  3. ↑ Xavier Leroy (14 вересня 2012). The state of OCaml, 2012 (PDF). OCaml Users and Developers Workshop (англ.). с. 4. Архів оригіналу (PDF) за 2 січня 2015. Процитовано 13 грудня 2014. [Архівовано 2015-01-02 у Wayback Machine.]
  4. ↑ Idris Example. Архів оригіналу за 16 грудня 2014. Процитовано 13 грудня 2014. [Архівовано 2014-12-16 у Wayback Machine.]
  5. ↑ а б https://dx.doi.org/10.1007/978-3-642-03359-9_6. Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics. TPHOLs '09. Munich, Germany: Springer-Verlag. 2009. с. 73—78. Процитовано 6 грудня 2013. {{cite conference}}: Пропущений або порожній |title= (довідка)
  6. ↑ Peyton Jones, Washburn, Weirich, 2004.
  7. ↑ Augustsson, Petersson, 1994.
  8. ↑ Cheney, Hinze, 2003, с. 25.
  9. ↑ Xi, Chen, Chen, 2003.
  10. ↑ Cheney, Hinze, 2003, с. 25—26.
  11. ↑ Peyton Jones, Washburn, Weirich, 2004, с. 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.