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

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

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

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

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

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

Вивід типів за відсутності оголошень типів, заданих програмістом, є алгоритмічно нерозв'язною задачею, а функції, визначені на узагальнених АТД, у загальному випадку можуть не приймати .

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

Приклад на Haskell У цьому прикладі визначається узагальнений тип Type, у якому подано кілька типів: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]

Примітки

Література