Yleistetty algebrallinen tietotyyppi
Yleistetty algebrallinen tietotyyppi ( GADT ) on yksi algebrallisten tietotyyppien tyypeistä , jolle on tunnusomaista se, että sen rakentajat voivat palauttaa arvoja, jotka eivät ole sen tyyppisiä siihen liittyviä [1] . Suunniteltu induktiivisia perheitä koskevien teosten vaikutuksesta riippuvaisten tyyppien tutkijoiden keskuudessa [2] .
Tällaisia tyyppejä on toteutettu useilla ohjelmointikielillä, erityisesti OCamlissa (versiosta 4 lähtien) [3] , Idrisissä [4] , Agdassa [5] ja Haskellissa , ja jälkimmäisessä se ei sisälly kielistandardiin, mutta on toteutettu vain yhdessä GHC . Haskell-kieli jäljittelee induktiivista perhettä ja edustaa niitä muiden tyyppien indeksoimana tyyppinä [5] .
Niitä käytetään yleistetyssä ohjelmoinnissa , ohjelmointikielten korkeamman asteen abstraktin syntaksin mallintamisessa ja objektimallintamisessa, tietorakenteiden invarianttien säilyttämisessä, rajoitusten ilmaisemisessa sisäänrakennetuissa verkkoaluekohtaisissa kielissä [6] .
Historia
Lennart Augustson ja Kent Peterson kuvasivat yleistettyjen algebrallisten tietotyyppien varhaisen version vuonna 1994, ja se perustui ALF -lauseen todistajaan [7] .
GADT :n modernin muodon esittelivät itsenäisesti vuonna 2003 Cheney ja Hinze ja sitä ennen Xi , Chen ja Chen ML- ja Haskell -algebrallisten tietotyyppien laajennuksina [8] [9] . Esitellyt geneeriset tyypit osoittautuivat toisiaan vastaaviksi ja ovat samanlaisia kuin Coqissa rakennuslaskennassa käytetyt induktiiviset tietotyyppiperheet (tai induktiiviset tietotyypit) [10] .
Vuonna 2006 kehitettiin laajennettuja algebrallisia tietotyyppejä, joissa yhdistettiin yleistetyt algebralliset tietotyypit eksistentiaalisiin tietotyyppeihin ja tyyppiluokkarajoituksiin , jotka Perry , Läufer ja Oderski esittelivät 1990-luvun puolivälissä.
Tyyppipäätelmä ohjelmoijan antamien tyyppimäärittelyjen puuttuessa on algoritmisesti
ratkaisematon ongelma , ja yleistetyillä ADT: illä määritetyt funktiot eivät välttämättä yleensä hyväksy päätyyppejä [ 11] [ 12] .
Tyyppiremontti vaatii useita suunnittelukompromissia ja on tutkimusaiheena vuodesta 2011 lähtien.
Haskell esimerkki
Seuraava esimerkki määrittelee yleistyypin Type, joka edustaa useita tyyppejä [13] :
tietotyyppi :: * -> * missä Char :: Type Char Int :: Type Int List :: Type a - > Type [ a ]
Tälle tyypille voit luoda ad-hoc-polymorfisen summausfunktion:
summa :: Tyyppi a -> a -> Int
summa Char _ = 0
summa Int n = n
summa ( Lista a ) xs = foldr ( + ) 0 ( kartta ( summa a ) xs )
Voidaan käyttää tyypeille, joita tukee Typeesimerkiksi tyyppi [Int]:
summa ( List Int ) [ 1 , 2 , 4 ]
Muistiinpanot
- ↑ Koopman, Plasmeijer, Swierstra, 2009 , s. 178-179.
- ↑ Schmid, Kitzelmann, Plasmeijer, 2010 .
- ↑ Xavier Leroy. OCamlin tila, 2012 ( linkki ei saatavilla) . OCaml-käyttäjien ja kehittäjien työpaja 4 (14. syyskuuta 2012). Käyttöpäivä: 13. joulukuuta 2014. Arkistoitu alkuperäisestä 2. tammikuuta 2015.
- ↑ Idris esimerkki . Haettu 13. joulukuuta 2014. Arkistoitu alkuperäisestä 16. joulukuuta 2014. (määrätön)
- ↑ 1 2 Bove, Ana ja Dybjer, Peter ja Norell, Ulf (2009). "Lyhyt katsaus Agdasta --- Toiminnallinen kieli riippuvilla tyypeillä" . 22. kansainvälisen konferenssin aineistoa Lauseen todistamisesta korkeamman järjestyksen logiikassa . TPHOLs '09. München, Saksa: Springer-Verlag. s. 73-78. DOI : 10.1007/978-3-642-03359-9_6 . Bove:2009:BOA:1616077.1616085 . Haettu 2013-12-06 .
- ↑ Peyton Jones, Washburn, Weirich, 2004 .
- ↑ Augustsson, Petersson, 1994 .
- ↑ Cheney ja Hinze 2003 , s. 25.
- ↑ Xi, Chen, Chen, 2003 .
- ↑ Cheney ja Hinze 2003 , s. 25-26.
- ↑ Peyton Jones, Washburn, Weirich, 2004 , s. 7.
- ↑ Schrijvers, Peyton Jones, Sulzmann, Vytiniotis, 2009 .
- ↑ Hagiya, M. ja Wadler, P. Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Fuji-Susono, Japani, 24.-26.4.2006, Proceedings. - Springer, 2006. - s. 17-18. — ISBN 9783540334385 .
Kirjallisuus
- Koopman, P.; Plasmeijer, R.; Swierstra, D. Advanced Functional Programming: 6th International School, AFP 2008, Heijen, Alankomaat, 19.-24.5.2008, tarkistetut luennot. - Springer, 2009. - 331 s. — ISBN 9783642046513 .
- Peyton Jones, Simon; Washburn, Geoffrey; Weirich, Stephanie. Heiluvat tyypit: tyyppipäätelmä yleistetyille algebrallisille tietotyypeille (englanniksi) // Tekninen raportti MS-CIS-05-25. - Pennsylvanian yliopisto, 2004.
- Cheney, James; Hinze, Ralph. Ensimmäisen luokan haamutyypit (englanniksi) // Tekninen raportti CUCIS TR2003-1901. - Cornellin yliopisto, 2003.
- Xi, Hongwei; Chen, Chiyan; Chen, Gang. Vartioidut rekursiiviset tietotyyppikonstruktorit // Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'03). - ACM Press, 2003. - S. 224–235 . - doi : 10.1145/604131.604150 .
- Sheard, Tim; Pasalic, Emir. Meta-ohjelmointi sisäänrakennetulla tyyppitasolla (englanti) // 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. ja Kitzelmann, E. ja Plasmeijer, R. Induktiivisen ohjelmoinnin lähestymistavat ja sovellukset: Kolmas kansainvälinen työpaja, AAIP 2009, Edinburgh, UK, 4. syyskuuta 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. Täydellinen ja päätettävissä oleva tyyppipäätelmä GADT:ille // Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh . – 2009.