Azərbaycanca AzərbaycancaБеларускі БеларускіDansk DanskDeutsch DeutschEspañola EspañolaFrançais FrançaisIndonesia IndonesiaItaliana Italiana日本語 日本語Қазақ ҚазақLietuvos LietuvosNederlands NederlandsPortuguês PortuguêsРусский Русскийසිංහල සිංහලแบบไทย แบบไทยTürkçe TürkçeУкраїнська Українська中國人 中國人United State United StateAfrikaans Afrikaans
Підтримка
www.wikidata.uk-ua.nina.az

Узага льнений алгебри чний тип да них англ generalized algebraic data type GADT один з видів алгебричних типів даних яки

Узагальнений алгебричний тип даних

Узагальнений алгебричний тип даних

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

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

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

Історія

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

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

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

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

Реконструкція типу вимагає під час проєктування кількох компромісів та є станом на 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]

Примітки

  1. Koopman, Plasmeijer, Swierstra, 2009, с. 178—179.
  2. Schmid, Kitzelmann, Plasmeijer, 2010.
  3. Xavier Leroy (14 вересня 2012). (PDF). OCaml Users and Developers Workshop (англ.). с. 4. Архів оригіналу (PDF) за 2 січня 2015. Процитовано 13 грудня 2014.
  4. Idris Example. оригіналу за 16 грудня 2014. Процитовано 13 грудня 2014.
  5. https://dx.doi.org/10.1007/978-3-642-03359-9_6. Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics. TPHOLs '09. Munich, Germany: Springer-Verlag. 2009. с. 73—78. Процитовано 6 грудня 2013. {{}}: Пропущений або порожній |title= ()
  6. Peyton Jones, Washburn, Weirich, 2004.
  7. Augustsson, Petersson, 1994.
  8. Cheney, Hinze, 2003, с. 25.
  9. Xi, Chen, Chen, 2003.
  10. Cheney, Hinze, 2003, с. 25—26.
  11. Peyton Jones, Washburn, Weirich, 2004, с. 7.
  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. — .

Література

  • 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. — .
  • 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. — .
  • 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.

Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет

Uzaga lnenij algebri chnij tip da nih angl generalized algebraic data type GADT odin z vidiv algebrichnih tipiv danih yakij harakterizuyetsya tim sho jogo konstruktori mozhut povertati znachennya ne svogo tipu pov yazanogo z nim Stvoreni pid vplivom robit pro induktivni simejstva sered doslidnikiv zalezhnih tipiv Taki tipi realizovano v kilkoh movah programuvannya zokrema v movah OCaml pochinayuchi vid versiyi 4 Agda ta Haskell prichomu v ostannomu voni ne vhodyat do standartu movi a realizovani lishe v odnomu z rozshiren kompilyatora GHC Mova Haskell imituye en podayuchi yih tipami indeksovanimi inshimi tipami Zastosovuyutsya v uzagalnenomu programuvanni modelyuvanni en mov programuvannya ta modelyuvannya ob yektiv zberezhenni invariantiv struktur danih virazhenni obmezhen u vbudovanih predmetno oriyentovanih movah IstoriyaRannya versiya uzagalnenih algebrichnih tipiv danih yaku opisali Lennart Augustson i Kent Peterson 1994 roku gruntuvalasya na zistavlenni zi vzircem u sistemi dovedennya teorem ALF U suchasnij formi GADT vveli 2003 roku nezalezhno Chejni Cheney ta Ginc Hinze i do cogo Si Xi Chen Chen i Chenom Chen yak rozshirennya algebrichnih tipiv danih ML i Haskell Vvedeni uzagalneni tipi viyavilisya ekvivalentnimi odin odnomu i shozhi na induktivni simejstva tipiv danih abo induktivni tipi danih vikoristovuvani v Coq u chislenni konstrukcij 2006 roku rozrobleno rozshireni algebrichni tipi danih sho poyednuyut uzagalneni algebrichni tipi danih z en ta obmezhennyami en yaki vveli Perri Perry Lyaufer Laufer i Oderski v seredini 1990 h Vivid tipiv za vidsutnosti ogoloshen tipiv zadanih programistom ye algoritmichno nerozv yaznoyu zadacheyu a funkciyi viznacheni na uzagalnenih ATD u zagalnomu vipadku mozhut ne prijmati en Rekonstrukciya tipu vimagaye pid chas proyektuvannya kilkoh kompromisiv ta ye stanom na 2011 rik temoyu doslidzhen Priklad na HaskellU comu prikladi viznachayetsya uzagalnenij tip Type u yakomu podano kilka tipiv data Type gt where Char Type Char Int Type Int List Type a gt Type a Dlya cogo tipu mozhna sklasti ad hoc polimorfnu funkciyu pidsumovuvannya sum Type a gt a gt Int sum Char 0 sum Int n n sum List a xs foldr 0 map sum a xs Yaku mozhna zastosovuvati dlya tipiv yaki pidtrimuyutsya Type napriklad dlya tipu Int sum List Int 1 2 4 PrimitkiKoopman Plasmeijer Swierstra 2009 s 178 179 Schmid Kitzelmann Plasmeijer 2010 Xavier Leroy 14 veresnya 2012 PDF OCaml Users and Developers Workshop angl s 4 Arhiv originalu PDF za 2 sichnya 2015 Procitovano 13 grudnya 2014 Idris Example originalu za 16 grudnya 2014 Procitovano 13 grudnya 2014 https dx doi org 10 1007 978 3 642 03359 9 6 Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics TPHOLs 09 Munich Germany Springer Verlag 2009 s 73 78 Procitovano 6 grudnya 2013 a href wiki D0 A8 D0 B0 D0 B1 D0 BB D0 BE D0 BD Cite conference title Shablon Cite conference cite conference a Propushenij abo porozhnij title dovidka Peyton Jones Washburn Weirich 2004 Augustsson Petersson 1994 Cheney Hinze 2003 s 25 Xi Chen Chen 2003 Cheney Hinze 2003 s 25 26 Peyton Jones Washburn Weirich 2004 s 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 LiteraturaKoopman 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

Дата публікації:
Топ