Tip de date algebrice generalizate
Un tip de date algebrice generalizate ( GADT ) este unul dintre tipurile de tipuri de date algebrice , care se caracterizează prin faptul că constructorii săi pot returna valori care nu sunt de tipul lor asociate [1] . Proiectat sub influența lucrărilor asupra familiilor inductive în rândul cercetătorilor de tipuri dependente [2] .
Astfel de tipuri sunt implementate în mai multe limbaje de programare, în special în OCaml (începând cu versiunea 4) [3] , Idris [4] , Agda [5] și Haskell , iar în acesta din urmă nu este inclus în standardul limbajului, dar este implementat în doar una din extensiile compilatorului GHC . Limba Haskell imită o familie inductivă , reprezentându-le ca tipuri indexate de alte tipuri [5] .
Ele sunt utilizate în programarea generalizată , modelarea sintaxei abstracte de ordin superior a limbajelor de programare și modelarea obiectelor, păstrând invarianții structurilor de date , exprimând constrângeri în limbaje încorporate specifice domeniului [6] .
Istorie
O versiune timpurie a tipurilor de date algebrice generalizate a fost descrisă de Lennart Augustson și Kent Peterson în 1994 și s-a bazat pe potrivirea modelelor în demonstratorul teoremei ALF [7] .
Forma modernă a GADT a fost introdusă independent în 2003 de către Cheney și Hinze și înainte de aceasta de către Xi , Chen și Chen ca extensii ale tipurilor de date algebrice ML și Haskell [8] [9] . Tipurile generice introduse s-au dovedit a fi echivalente între ele și sunt similare cu familiile de tipuri de date inductive (sau tipuri de date inductive) utilizate în Coq în calculul construcției [10] .
În 2006, au fost dezvoltate tipuri de date algebrice extinse, combinând tipuri de date algebrice generalizate cu tipurile de date existențiale și constrângeri de clase de tip introduse de Perry , Läufer și Oderski la mijlocul anilor 1990.
Inferența de tip în absența declarațiilor de tip date de programator este o problemă de nerezolvată din punct de vedere algoritmic
, iar funcțiile definite pe ADT-uri generalizate pot să nu accepte în general tipuri principale [ 11] [ 12] .
Reconstrucția tipului necesită mai multe compromisuri de proiectare și este un subiect de cercetare din 2011.
Exemplu Haskell
Următorul exemplu definește un tip generic Typecare reprezintă mai multe tipuri [13] :
date Type :: * -> * unde
Char :: Type Char
Int :: Type Int
List :: Type a -> Type [ a ]
Pentru acest tip, puteți compune o funcție de însumare
ad-hoc-polimorfă :
sum :: Type a -> a -> Int
sum Char _ = 0
sum Int n = n
sum ( Lista a ) xs = foldr ( + ) 0 ( map ( suma a ) xs )
Care poate fi folosit pentru tipurile acceptate de Type, de exemplu, pentru tipul [Int]:
suma ( List Int ) [ 1 , 2 , 4 ]
Note
- ↑ Koopman, Plasmeijer, Swierstra, 2009 , pp. 178-179.
- ↑ Schmid, Kitzelmann, Plasmeijer, 2010 .
- ↑ Xavier Leroy. Statul OCaml, 2012 ( link inaccesibil) . Atelierul 4 pentru utilizatori și dezvoltatori OCaml (14 septembrie 2012). Data accesului: 13 decembrie 2014. Arhivat din original la 2 ianuarie 2015.
- ↑ Exemplu Idris . Consultat la 13 decembrie 2014. Arhivat din original pe 16 decembrie 2014. (nedefinit)
- ↑ 1 2 Bove, Ana și Dybjer, Peter și Norell, Ulf (2009). „O scurtă prezentare a Agda --- Un limbaj funcțional cu tipuri dependente” . Proceedings of the 22 International Conference on Theorem Demoving in Higher Order Logics . TPHOLs '09. Munchen, Germania: Springer-Verlag. pp. 73-78. DOI : 10.1007/978-3-642-03359-9_6 . Bove:2009:BOA:1616077.1616085 . Accesat 2013-12-06 .
- ^ Peyton Jones, Washburn, Weirich, 2004 .
- ↑ Augustsson, Petersson, 1994 .
- ↑ Cheney și Hinze 2003 , p. 25.
- ↑ Xi, Chen, Chen, 2003 .
- ↑ Cheney și Hinze 2003 , p. 25-26.
- ↑ Peyton Jones, Washburn, Weirich, 2004 , p. 7.
- ↑ Schrijvers, Peyton Jones, Sulzmann, Vytiniotis, 2009 .
- ↑ Hagiya, M. și 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 .
Literatură
- Koopman, P.; Plasmeijer, R.; Swierstra, D. Advanced Functional Programming: 6th International School, AFP 2008, Heijen, Olanda, 19-24 mai 2008, Revised Lectures. - Springer, 2009. - 331 p. — ISBN 9783642046513 .
- Peyton Jones, Simon; Washburn, Geoffrey; Weirich, Stephanie. Tipuri wobbly: inferență de tip pentru tipuri de date algebrice generalizate (engleză) // Raport tehnic MS-CIS-05-25. - Universitatea din Pennsylvania, 2004.
- Cheney, James; Hinze, Ralph. Tipuri de fantome de primă clasă (engleză) // Raport tehnic CUCIS TR2003-1901. — Universitatea Cornell, 2003.
- Xi, Hongwei; Chen, Chiyan; Chen, Gang. Constructori de tipuri de date recursive protejate // 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-programare cu egalitate de tip încorporată (engleză) // Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-langages (LFM'04), Cork. - 2004. - doi : 10.1016/j.entcs.2007.11.012 .
- Schmid, U. și Kitzelmann, E. și Plasmeijer, R. Abordări și aplicații ale programării inductive: al treilea atelier internațional, AAIP 2009, Edinburgh, Marea Britanie, 4 septembrie 2009, lucrări revizuite. - Springer, 2010. - P. 114-115. — ISBN 9783642119309 .
- Peyton Jones, Simon; Vytiniotis, Dimitrios; Weirich, Stephanie; Washburn, Geoffrey. Inferență de tip simplă bazată pe unificare pentru GADT-uri // Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland . — 2006.
- Schrijvers, Tom, Peyton Jones, Simon, Sulzmann, Martin, Vytiniotis, Dimitrios. Inferență de tip completă și determinabilă pentru GADT-uri // Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh . — 2009.