Zobecněný algebraický datový typ
Zobecněný algebraický datový typ ( GADT ) je jedním z typů algebraických datových typů , který se vyznačuje tím, že jeho konstruktory mohou vracet hodnoty, které nejsou jejich typu s ním spojené [1] . Navrženo pod vlivem prací o induktivních rodinách mezi výzkumníky závislých typů [2] .
Tyto typy jsou implementovány v několika programovacích jazycích, zejména v OCaml (od verze 4) [3] , Idris [4] , Agda [5] a Haskell , přičemž v posledně jmenovaném není součástí jazykového standardu, ale je implementován pouze v jednom z rozšíření kompilátoru GHC . Jazyk Haskell napodobuje induktivní rodinu a představuje je jako typy indexované jinými typy [5] .
Používají se v zobecněném programování , modelování abstraktní syntaxe programovacích jazyků vyššího řádu a objektovém modelování, zachování invariantů datových struktur , vyjadřování omezení ve vestavěných doménově specifických jazycích [6] .
Historie
Ranou verzi zobecněných algebraických datových typů popsali Lennart Augustson a Kent Peterson v roce 1994 a byla založena na porovnávání vzorů v dokazovateli teorému ALF [7] .
Moderní forma GADT byla představena nezávisle v roce 2003 Cheney a Hinze a předtím Xi , Chen a Chen jako rozšíření ML a Haskell algebraických datových typů [8] [9] . Ukázalo se, že představené generické typy jsou navzájem ekvivalentní a jsou podobné rodinám indukčních datových typů (nebo indukčním datovým typům) používaným v Coq v konstrukčním kalkulu [10] .
V roce 2006 byly vyvinuty rozšířené algebraické datové typy, které kombinují zobecněné algebraické datové typy s existenčními datovými typy a omezeními typových tříd zavedenými Perrym , Läuferem a Oderskim v polovině 90. let.
Odvozování typu v nepřítomnosti deklarací typu zadaných programátorem je algoritmicky
neřešitelný problém a funkce definované na zobecněných ADT nemusí obecně přijímat hlavní typy [ 11] [ 12] .
Rekonstrukce typu vyžaduje několik konstrukčních kompromisů a je předmětem výzkumu od roku 2011.
Haskell příklad
Následující příklad definuje generický typ Type, který představuje více typů [13] :
data Type :: * -> * kde
Char :: Type Char
Int :: Type Int
List :: Type a -> Type [ a ]
Pro tento typ můžete sestavit ad-hoc-polymorfní sumační funkci:
součet :: Typ a -> a -> Int
součet Char _ = 0
součet Int n = n
součet ( Seznam a ) xs = složka ( + ) 0 ( mapa ( součet a ) xs )
Což lze použít pro typy podporované Type, například pro typ [Int]:
součet ( List Int ) [ 1 , 2 , 4 ]
Poznámky
- ↑ Koopman, Plasmeijer, Swierstra, 2009 , pp. 178-179.
- ↑ Schmid, Kitzelmann, Plasmeijer, 2010 .
- ↑ Xavier Leroy. Stav OCaml, 2012 ( nepřístupný odkaz) . Workshop pro uživatele a vývojáře OCaml 4 (14. září 2012). Datum přístupu: 13. prosince 2014. Archivováno z originálu 2. ledna 2015.
- ↑ Příklad Idris . Získáno 13. prosince 2014. Archivováno z originálu 16. prosince 2014. (neurčitý)
- ↑ 1 2 Bove, Ana a Dybjer, Peter a Norell, Ulf (2009). „Stručný přehled Agda --- Funkční jazyk se závislými typy“ . Sborník příspěvků z 22. mezinárodní konference o dokazování vět v logice vyššího řádu . TPHOLs '09. Mnichov, Německo: Springer-Verlag. str. 73-78. DOI : 10.1007/978-3-642-03359-9_6 . Bove:2009:BOA:1616077.1616085 . Staženo 2013-12-06 .
- ↑ Peyton Jones, Washburn, Weirich, 2004 .
- ↑ Augustsson, Petersson, 1994 .
- ↑ Cheney a Hinze 2003 , str. 25.
- ↑ Xi, Chen, Chen, 2003 .
- ↑ Cheney a Hinze 2003 , str. 25-26.
- ↑ Peyton Jones, Washburn, Weirich, 2004 , str. 7.
- ↑ Schrijvers, Peyton Jones, Sulzmann, Vytiniotis, 2009 .
- ↑ Hagiya, M. a Wadler, P. Funkční a logické programování: 8. mezinárodní symposium, FLOPS 2006, Fuji-Susono, Japonsko, 24.–26. dubna 2006, sborník příspěvků. - Springer, 2006. - S. 17-18. — ISBN 9783540334385 .
Literatura
- Koopman, P.; Plasmeijer, R.; Swierstra, D. Pokročilé funkční programování: 6. mezinárodní škola, AFP 2008, Heijen, Nizozemsko, 19.-24. května 2008, Revidované přednášky. - Springer, 2009. - 331 s. — ISBN 9783642046513 .
- Peyton Jones, Simon; Washburn, Geoffrey; Weirich, Stephanie. Kolísavé typy: odvození typů pro zobecněné algebraické datové typy (anglicky) // Technical Report MS-CIS-05-25. — University of Pennsylvania, 2004.
- Cheney, James; Hinze, Ralph. Prvotřídní fantomové typy (anglicky) // Technical Report CUCIS TR2003-1901. — Cornell University, 2003.
- Xi, Hongwei; Chen, Chiyan; Chen, Gang. Chráněné rekurzivní konstruktory datových typů // Sborník příspěvků z 30. sympozia ACM SIGPLAN-SIGACT o principech programovacích jazyků (POPL'03). - ACM Press, 2003. - S. 224–235 . - doi : 10.1145/604131.604150 .
- Sheard, Tim; Pasalic, Emír. Metaprogramování s vestavěnou typovou rovností (anglicky) // Sborník ze čtvrtého mezinárodního workshopu o logických rámcích a metajazycích (LFM'04), Cork. - 2004. - doi : 10.1016/j.entcs.2007.11.012 .
- Schmid, U. a Kitzelmann, E. a Plasmeijer, R. Přístupy a aplikace indukčního programování: Třetí mezinárodní seminář, AAIP 2009, Edinburgh, Spojené království, 4. září 2009, Revised Papers. - Springer, 2010. - S. 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. Úplný a rozhoditelný typ inference pro GADT // Sborník z mezinárodní konference ACM o funkčním programování (ICFP'09), Edinburgh . — 2009.