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


Обобщённый алгебраический тип да́нных (англ. 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-х годов.