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

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

Обобщённый алгебраический тип да́нных (Шаблон:Lang-en) — один из видов алгебраических типов данных, который характеризуется тем, что его конструкторы могут возвращать значения не своего типа, связанного с нимШаблон:Sfn. Сконструированы под влиянием работ об индуктивных семействах в среде исследователей зависимых типовШаблон:Sfn.

Такие типы реализованы в нескольких языках программирования, в частности в языках OCaml (начиная с версии 4)[1], Idris[2], Agda[3] и Haskell, причём в последнем оно не входит в стандарт языка, а реализовано только в одном из расширений компилятора GHC. Язык Haskell имитирует Шаблон:Нп2, представляя их типами, индексированными другими типами[3].

Применяются в обобщённом программировании, моделировании Шаблон:Нп2 языков программирования и моделировании объектов, сохранении инвариантов структур данных, выражении ограничений во встроенных предметно-ориентированных языкахШаблон:Sfn.

История

Ранняя версия обобщённых алгебраических типов данных была описана Леннартом Аугустсоном и Кентом Петерсоном в 1994 году и основывалась на сопоставлении с образцом в системе доказательства теорем ALFШаблон:Sfn.

В современной форме GADT были введены в 2003 году независимо Чейни (Шаблон:Lang-en2) и Хинце (Шаблон:Lang-en2) и до этого Си (Шаблон:Lang-en2), Ченом (Шаблон:Lang-en2) и Ченом (Шаблон:Lang-en2) как расширения алгебраических типов данных ML и HaskellШаблон:SfnШаблон:Sfn. Введённые обобщённые типы оказались эквивалентны друг другу и похожи на индуктивные семейства типов данных (или индуктивные типы данных), используемые в Coq в исчислении конструкцийШаблон:Sfn.

В 2006 году разработаны расширенные алгебраические типы данных, сочетающие обобщённые алгебраические типы данных с Шаблон:Iw и ограничениями Шаблон:Iw, введёнными Перри (Шаблон:Lang-en2), Ляуфером (Шаблон:Lang-en2) и Одерски в середине 1990-х годов.

Вывод типов при отсутствии деклараций типов, заданных программистом, является алгоритмически неразрешимой задачей, а функции, определённые на обобщённых АТД, в общем случае могут не принимать Шаблон:Нп2Шаблон:SfnШаблон:Sfn.

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

Пример на Haskell

В следующем примере определяется обобщённый тип Type, в котором представлены несколько типов[4]: 

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. ↑ Шаблон:Cite web
  2. ↑ Шаблон:Cite web
  3. ↑ 3,0 3,1 Шаблон:Cite conference
  4. ↑ Шаблон:Книга
Источник — http://wikihandbk.com/ruwiki/index.php?title=Русская_Википедия:Обобщённый_алгебраический_тип_данных&oldid=10497253