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

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

Такие типы реализованы в нескольких языках программирования, в частности в языках OCaml (начиная с версии 4)^[3], Idris^[4], Agda^[5] и Haskell, причём в последнем оно не входит в стандарт языка, а реализовано только в одном из расширений компилятора GHC. Язык Haskell имитирует индуктивное семейство (англ. inductive family — версия статьи «Индуктивное семейство» на английском языке inductive family), представляя их типами, индексированными другими типами^[5].

Применяются в обобщённом программировании, моделировании абстрактного синтаксиса высшего порядка (англ. higher-order abstract syntax — версия статьи «Абстрактный синтаксис высшего порядка» на английском языке 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 — версия статьи «Основной тип» на английском языке 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]

ПримечанияПравить

↑ Koopman, Plasmeijer, Swierstra, 2009, pp. 178—179.
↑ Schmid, Kitzelmann, Plasmeijer, 2010.
↑ Xavier Leroy. The state of OCaml, 2012 (англ.). OCaml Users and Developers Workshop 4 (14 сентября 2012). Дата обращения: 13 декабря 2014. Архивировано из оригинала 2 января 2015 года.
↑ Idris Example (неопр.). Дата обращения: 13 декабря 2014. Архивировано 16 декабря 2014 года.
↑ ¹ ² Bove, Ana and Dybjer, Peter and Norell, Ulf (2009). “A Brief Overview of Agda --- A Functional Language with Dependent Types”. Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics. TPHOLs '09. Munich, Germany: Springer-Verlag. pp. 73—78. DOI:10.1007/978-3-642-03359-9_6. Bove:2009:BOA:1616077.1616085. Дата обращения 2013-12-06.
↑ Peyton Jones, Washburn, Weirich, 2004.
↑ Augustsson, Petersson, 1994.
↑ Cheney, Hinze, 2003, p. 25.
↑ Xi, Chen, Chen, 2003.
↑ Cheney, Hinze, 2003, p. 25—26.
↑ Peyton Jones, Washburn, Weirich, 2004, p. 7.
↑ Schrijvers, Peyton Jones, Sulzmann, Vytiniotis, 2009.
↑ 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.

[_042c08f46ba0ab7c-1] Koopman, Plasmeijer, Swierstra, 2009, pp. 178—179.

[_1da63578c9a64b33-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 (неопр.). Дата обращения: 13 декабря 2014. Архивировано 16 декабря 2014 года.

[agda-5] ¹ ² Bove, Ana and Dybjer, Peter and Norell, Ulf (2009). “A Brief Overview of Agda --- A Functional Language with Dependent Types”. Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics. TPHOLs '09. Munich, Germany: Springer-Verlag. pp. 73—78. DOI:10.1007/978-3-642-03359-9_6. Bove:2009:BOA:1616077.1616085. Дата обращения 2013-12-06.

[_0d2de93b58ffc776-6] Peyton Jones, Washburn, Weirich, 2004.

[_724b0d657c0c30b9-7] Augustsson, Petersson, 1994.

[_ea4025a887727021-8] Cheney, Hinze, 2003, p. 25.

[_ba3f4ec0a51eca07-9] Xi, Chen, Chen, 2003.

[_ec5aa2f4cac73d69-10] Cheney, Hinze, 2003, p. 25—26.

[_64cac5d83a9fedb5-11] Peyton Jones, Washburn, Weirich, 2004, p. 7.

[_d3ce9a7be4f2f087-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.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]