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

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

Такие типы реализованы в нескольких языках программирования, в частности в языках OCaml (начиная с версии 4), Idris, Agda и Haskell, причём в последнем оно не входит в стандарт языка Haskell-98, а реализовано только в одном из расширений компилятора GHC. Язык Haskell имитирует индуктивное семейство (англ. inductive family), представляя их типами, индексированными другими типами.

История

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

Обобщённые АТД были введены в 2003 году независимо Чейни (Cheney) и Хинце (Hinze) и до этого Си (Xi), Ченом (Chen) и Ченом (Chen) как расширения алгебраических типов данных ML и Haskell. Введённые обобщённые АТД оказались эквивалентны друг другу и похожи на индуктивные семейства типов данных (или индуктивные типы данных), используемые в Coq в исчислении индуктивных конструкций.

В 2006 году Sulzmann, Wazny и Stuckey ввели расширенные алгебраические типы данных, сочетающие обобщённые АТД с экзистенциальными типами данных и ограничениями класса типов, введёнными Перри (Perry), Ляуфером (Läufer) и Одерски (Odersky) в середине 1990-х.

Вывод типов при отсутствии деклараций типов, заданных программистом, является алгоритмически неразрешимой задачей, а функции, определённые на обобщённых АТД, в общем случае могут не принимать основные типы(principal types).

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

Применения

Обобщённые АДТ применяются в обобщённом программировании, моделировании абстрактного синтаксиса высшего порядка (англ. higher-order abstract syntax) языков программирования и моделировании объектов, сохранении инвариантов структур данных, выражении ограничений во встроенных предметно-ориентированных языках.

Пример на 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]

Литература

• 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 [research.microsoft.com/en-us/um/people/simonpj/papers/gadt/MS-CIS-05-26.pdf Wobbly types: type inference for generalised algebraic data types] (англ.) // Technical Report MS-CIS-05-25. — University of Pennsylvania, 2004.
• Augustsson, Lennart; Petersson, Kent [web.cecs.pdx.edu/~sheard/papers/silly.pdf 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.
• Peyton Jones, Simon; Vytiniotis, Dimitrios; Weirich, Stephanie; Washburn, Geoffrey [research.microsoft.com/en-us/um/people/simonpj/papers/gadt/gadt-rigid-contexts.pdf 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 [research.microsoft.com/en-us/um/people/simonpj/papers/gadt/implication_constraints.pdf Complete and Decidable Type Inference for GADTs] (англ.) // Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh. — 2009.

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

Уже смеркалось, когда Денисов с Петей и эсаулом подъехали к караулке. В полутьме виднелись лошади в седлах, казаки, гусары, прилаживавшие шалашики на поляне и (чтобы не видели дыма французы) разводившие красневший огонь в лесном овраге. В сенях маленькой избушки казак, засучив рукава, рубил баранину. В самой избе были три офицера из партии Денисова, устроивавшие стол из двери. Петя снял, отдав сушить, свое мокрое платье и тотчас принялся содействовать офицерам в устройстве обеденного стола.
Через десять минут был готов стол, покрытый салфеткой. На столе была водка, ром в фляжке, белый хлеб и жареная баранина с солью.
Сидя вместе с офицерами за столом и разрывая руками, по которым текло сало, жирную душистую баранину, Петя находился в восторженном детском состоянии нежной любви ко всем людям и вследствие того уверенности в такой же любви к себе других людей.
– Так что же вы думаете, Василий Федорович, – обратился он к Денисову, – ничего, что я с вами останусь на денек? – И, не дожидаясь ответа, он сам отвечал себе: – Ведь мне велено узнать, ну вот я и узнаю… Только вы меня пустите в самую… в главную. Мне не нужно наград… А мне хочется… – Петя стиснул зубы и оглянулся, подергивая кверху поднятой головой и размахивая рукой.
– В самую главную… – повторил Денисов, улыбаясь.
– Только уж, пожалуйста, мне дайте команду совсем, чтобы я командовал, – продолжал Петя, – ну что вам стоит? Ах, вам ножик? – обратился он к офицеру, хотевшему отрезать баранины. И он подал свой складной ножик.
Офицер похвалил ножик.
– Возьмите, пожалуйста, себе. У меня много таких… – покраснев, сказал Петя. – Батюшки! Я и забыл совсем, – вдруг вскрикнул он. – У меня изюм чудесный, знаете, такой, без косточек. У нас маркитант новый – и такие прекрасные вещи. Я купил десять фунтов. Я привык что нибудь сладкое. Хотите?.. – И Петя побежал в сени к своему казаку, принес торбы, в которых было фунтов пять изюму. – Кушайте, господа, кушайте.
– А то не нужно ли вам кофейник? – обратился он к эсаулу. – Я у нашего маркитанта купил, чудесный! У него прекрасные вещи. И он честный очень. Это главное. Я вам пришлю непременно. А может быть еще, у вас вышли, обились кремни, – ведь это бывает. Я взял с собою, у меня вот тут… – он показал на торбы, – сто кремней. Я очень дешево купил. Возьмите, пожалуйста, сколько нужно, а то и все… – И вдруг, испугавшись, не заврался ли он, Петя остановился и покраснел.
Он стал вспоминать, не сделал ли он еще каких нибудь глупостей. И, перебирая воспоминания нынешнего дня, воспоминание о французе барабанщике представилось ему. «Нам то отлично, а ему каково? Куда его дели? Покормили ли его? Не обидели ли?» – подумал он. Но заметив, что он заврался о кремнях, он теперь боялся.
«Спросить бы можно, – думал он, – да скажут: сам мальчик и мальчика пожалел. Я им покажу завтра, какой я мальчик! Стыдно будет, если я спрошу? – думал Петя. – Ну, да все равно!» – и тотчас же, покраснев и испуганно глядя на офицеров, не будет ли в их лицах насмешки, он сказал:
– А можно позвать этого мальчика, что взяли в плен? дать ему чего нибудь поесть… может…
– Да, жалкий мальчишка, – сказал Денисов, видимо, не найдя ничего стыдного в этом напоминании. – Позвать его сюда. Vincent Bosse его зовут. Позвать.
– Я позову, – сказал Петя.
– Позови, позови. Жалкий мальчишка, – повторил Денисов.
Петя стоял у двери, когда Денисов сказал это. Петя пролез между офицерами и близко подошел к Денисову.
– Позвольте вас поцеловать, голубчик, – сказал он. – Ах, как отлично! как хорошо! – И, поцеловав Денисова, он побежал на двор.
– Bosse! Vincent! – прокричал Петя, остановясь у двери.
– Вам кого, сударь, надо? – сказал голос из темноты. Петя отвечал, что того мальчика француза, которого взяли нынче.
– А! Весеннего? – сказал казак.
Имя его Vincent уже переделали: казаки – в Весеннего, а мужики и солдаты – в Висеню. В обеих переделках это напоминание о весне сходилось с представлением о молоденьком мальчике.
– Он там у костра грелся. Эй, Висеня! Висеня! Весенний! – послышались в темноте передающиеся голоса и смех.
– А мальчонок шустрый, – сказал гусар, стоявший подле Пети. – Мы его покормили давеча. Страсть голодный был!
В темноте послышались шаги и, шлепая босыми ногами по грязи, барабанщик подошел к двери.
– Ah, c'est vous! – сказал Петя. – Voulez vous manger? N'ayez pas peur, on ne vous fera pas de mal, – прибавил он, робко и ласково дотрогиваясь до его руки. – Entrez, entrez. [Ах, это вы! Хотите есть? Не бойтесь, вам ничего не сделают. Войдите, войдите.]
– Merci, monsieur, [Благодарю, господин.] – отвечал барабанщик дрожащим, почти детским голосом и стал обтирать о порог свои грязные ноги. Пете многое хотелось сказать барабанщику, но он не смел. Он, переминаясь, стоял подле него в сенях. Потом в темноте взял его за руку и пожал ее.
– Entrez, entrez, – повторил он только нежным шепотом.
«Ах, что бы мне ему сделать!» – проговорил сам с собою Петя и, отворив дверь, пропустил мимо себя мальчика.
Когда барабанщик вошел в избушку, Петя сел подальше от него, считая для себя унизительным обращать на него внимание. Он только ощупывал в кармане деньги и был в сомненье, не стыдно ли будет дать их барабанщику.


От барабанщика, которому по приказанию Денисова дали водки, баранины и которого Денисов велел одеть в русский кафтан, с тем, чтобы, не отсылая с пленными, оставить его при партии, внимание Пети было отвлечено приездом Долохова. Петя в армии слышал много рассказов про необычайные храбрость и жестокость Долохова с французами, и потому с тех пор, как Долохов вошел в избу, Петя, не спуская глаз, смотрел на него и все больше подбадривался, подергивая поднятой головой, с тем чтобы не быть недостойным даже и такого общества, как Долохов.
Наружность Долохова странно поразила Петю своей простотой.
Денисов одевался в чекмень, носил бороду и на груди образ Николая чудотворца и в манере говорить, во всех приемах выказывал особенность своего положения. Долохов же, напротив, прежде, в Москве, носивший персидский костюм, теперь имел вид самого чопорного гвардейского офицера. Лицо его было чисто выбрито, одет он был в гвардейский ваточный сюртук с Георгием в петлице и в прямо надетой простой фуражке. Он снял в углу мокрую бурку и, подойдя к Денисову, не здороваясь ни с кем, тотчас же стал расспрашивать о деле. Денисов рассказывал ему про замыслы, которые имели на их транспорт большие отряды, и про присылку Пети, и про то, как он отвечал обоим генералам. Потом Денисов рассказал все, что он знал про положение французского отряда.