सामान्यीकृत बीजीय डेटा प्रकार
कार्यात्मक प्रोग्रामिंग में, एक सामान्यीकृत बीजगणितीय डेटा प्रकार (जीएडीटी, प्रथम श्रेणी फैंटम प्रकार,[1] संरक्षित पुनरावर्ती डेटाटाइप,[2] या समानता-योग्य प्रकार [3]) पैरामीट्रिक बीजगणितीय डेटा प्रकारों का एक सामान्यीकरण है।
सिंहावलोकन
जीएडीटी में, प्रोडक्ट कंस्ट्रक्टर (हास्केल में डेटा कंस्ट्रक्टर कहा जाता है) अपने रिटर्न वैल्यू (प्रतिफल मान) के प्रकार इंस्टेंशियेशन (दृष्टांतिकरण) के रूप में एडीटी का एक स्पष्ट इंस्टेंशियेशन प्रदान कर सकते हैं। यह कार्यों को अधिक उन्नत प्रकार के व्यवहार के साथ परिभाषित करने की अनुमति देता है। हास्केल 2010 के डेटा कंस्ट्रक्टर के लिए, रिटर्न वैल्यू में कंस्ट्रक्टर के एप्लिकेशन पर एडीटी पैरामीटर्स के इंस्टेंशियशन द्वारा निहित प्रकार इंस्टेंशियशन होता है।
-- A parametric ADT that is not a GADT
data List a = Nil | Cons a (List a)
integers = Cons 12 (Cons 107 Nil) -- the type of integers is List Int
strings = Cons "boat" (Cons "dock" Nil) -- the type of strings is List String
-- A GADT
data Expr a where
EBool :: Bool -> Expr Bool
EInt :: Int -> Expr Int
EEqual :: Expr Int -> Expr Int -> Expr Bool
eval :: Expr a -> a
eval e = case e of
EBool a -> a
EInt a -> a
EEqual a b -> (eval a) == (eval b)
expr1 = EEqual (EInt 2) (EInt 3) -- the type of expr1 is Expr Bool
ret = eval expr1 -- ret is False
वे वर्तमान में जीएचसी कंपाइलर में एक गैर-मानक एक्सटेंशन के रूप में कार्यान्वित किए जाते हैं, जिनका उपयोग अन्य लोगों के अलावा, पग्स और डार्क्स द्वारा किया जाता है। ओकैमल संस्करण 4.00 से मूल रूप से जीएडीटी का समर्थन करता है।[4]
जीएचसी कार्यान्वयन अस्तित्वगत मात्रात्मक प्रकार के मापदंडों और स्थानीय बाधाओं के लिए समर्थन प्रदान करता है।
इतिहास
सामान्यीकृत बीजीय डेटा प्रकारों का प्रारंभिक संस्करण ऑगस्टसन और पीटरसन (1994) द्वारा वर्णित किया गया था और यह एएलएफ में पैटर्न मिलान पर आधारित था।
सामान्यीकृत बीजगणितीय डेटा प्रकार स्वतंत्र रूप से चेनी और हिंज (2003) द्वारा और उससे पहले शी, चेन और चेन (2003) द्वारा एमएल और हास्केल के बीजीय डेटा प्रकारों के विस्तार के रूप में पेश किए गए थे।[5] दोनों मूलतः एक-दूसरे के समतुल्य हैं। वे सीओक्यू के कैलकुलस ऑफ इंडक्टिव कंस्ट्रक्शन और अन्य आश्रित रूप से टाइप की गई भाषाओं में पाए जाने वाले डेटा प्रकारों (या इंडक्टिव डेटाटाइप्स) के इंडक्टिव वर्गों के समान हैं, आश्रित प्रकारों को मॉड्यूल करते हैं और सिवाय इसके कि उत्तरार्द्ध में एक अतिरिक्त सकारात्मकता प्रतिबंध है जो जीएडीटी में लागू नहीं होता है।[6]
Sulzmann, Wazny & Stuckey (2006) विस्तारित बीजगणितीय डेटा प्रकार पेश किए गए जो जीएडीटी को अस्तित्वगत प्रकार और प्रकार वर्ग बाधाओं के साथ जोड़ते हैं। किसी भी प्रोग्रामर द्वारा प्रदत्त प्रकार के एनोटेशन की अनुपस्थिति में प्रकार का अनुमान अनिर्णीत समस्या है[7] और जीएडीटी पर परिभाषित फ़ंक्शन सामान्य रूप से प्रमुख प्रकारों को स्वीकार नहीं करते हैं।[8] प्रकार के पुनर्निर्माण के लिए कई डिज़ाइन ट्रेड-ऑफ़ की आवश्यकता होती है और यह सक्रिय अनुसंधान का क्षेत्र है (Peyton Jones, Washburn & Weirich 2004; Peyton Jones et al. 2006. वसंत 2021 में, स्काला 3.0 जारी किया गया है।[9] स्काला (प्रोग्रामिंग भाषा) का यह प्रमुख अद्यतन GADTs लिखने की संभावना प्रस्तुत करता है[10] बीजगणितीय डेटा प्रकार के समान वाक्यविन्यास के साथ, जो मार्टिन ओडर्सकी के अनुसार अन्य प्रोग्रामिंग भाषा में नहीं है।[11]
अनुप्रयोग
जीएडीटी के अनुप्रयोगों में सामान्य प्रोग्रामिंग, मॉडलिंग प्रोग्रामिंग भाषाएं (उच्च-क्रम अमूर्त वाक्यविन्यास), डेटा संरचनाओं में अपरिवर्तनीय (कंप्यूटर विज्ञान) को बनाए रखना, एम्बेडेड डोमेन-विशिष्ट भाषाओं में बाधाओं को व्यक्त करना और मॉडलिंग ऑब्जेक्ट शामिल हैं।[12]
उच्च-क्रम अमूर्त वाक्यविन्यास
जीएडीटी का एक महत्वपूर्ण अनुप्रयोग उच्च-क्रम अमूर्त वाक्यविन्यास को एक प्रकार से सुरक्षित तरीके से एम्बेड करना है। यहां आधार प्रकार, ट्यूपल (कंप्यूटर विज्ञान) और एक निश्चित बिंदु कॉम्बिनेटर के मनमाने संग्रह के साथ सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस का एक एम्बेडिंग है:
data Lam :: * -> * where
Lift :: a -> Lam a -- ^ lifted value
Pair :: Lam a -> Lam b -> Lam (a, b) -- ^ product
Lam :: (Lam a -> Lam b) -> Lam (a -> b) -- ^ lambda abstraction
App :: Lam (a -> b) -> Lam a -> Lam b -- ^ function application
Fix :: Lam (a -> a) -> Lam a -- ^ fixed point
और एक प्रकार का सुरक्षित मूल्यांकन फ़ंक्शन:
eval :: Lam t -> t
eval (Lift v) = v
eval (Pair l r) = (eval l, eval r)
eval (Lam f) = \x -> eval (f (Lift x))
eval (App f x) = (eval f) (eval x)
eval (Fix f) = (eval f) (eval (Fix f))
फैक्टोरियल फ़ंक्शन को अब इस प्रकार लिखा जा सकता है:
fact = Fix (Lam (\f -> Lam (\y -> Lift (if eval y == 0 then 1 else eval y * (eval f) (eval y - 1)))))
eval(fact)(10)
हमें नियमित बीजगणितीय डेटा प्रकारों का उपयोग करने में समस्याओं का सामना करना पड़ता। प्रकार पैरामीटर को छोड़ने से उठाए गए आधार प्रकार अस्तित्वगत रूप से परिमाणित हो जाते, जिससे मूल्यांकनकर्ता को लिखना असंभव हो जाता। एक प्रकार के पैरामीटर के साथ हम अभी भी एक आधार प्रकार तक ही सीमित रहेंगे। इसके अलावा, ख़राब अभिव्यक्तियाँ जैसे App (Lam (\x -> Lam (\y -> App x y))) (Lift True) निर्माण करना संभव होता, जबकि वे GADT का उपयोग करके गलत टाइप किए गए हैं। एक सुगठित एनालॉग है App (Lam (\x -> Lam (\y -> App x y))) (Lift (\z -> True)). ऐसा इसलिए है क्योंकि का प्रकार x है Lam (a -> b), के प्रकार से अनुमान लगाया गया है Lam डेटा कंस्ट्रक्टर.
यह भी देखें
- प्रकार चर
टिप्पणियाँ
- ↑ Cheney & Hinze 2003.
- ↑ Xi, Chen & Chen 2003.
- ↑ Sheard & Pasalic 2004.
- ↑ "OCaml 4.00.1". ocaml.org.
- ↑ Cheney & Hinze 2003, p. 25.
- ↑ Cheney & Hinze 2003, pp. 25–26.
- ↑ Peyton Jones, Washburn & Weirich 2004, p. 7.
- ↑ Schrijvers et al. 2009, p. 1.
- ↑ Kmetiuk, Anatolii. "SCALA 3 IS HERE!🎉🎉🎉". scala-lang.org. École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland. Retrieved 19 May 2021.
- ↑ "SCALA 3 — BOOK ALGEBRAIC DATA TYPES". scala-lang.org. École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland. Retrieved 19 May 2021.
- ↑ Odersky, Martin. "A Tour of Scala 3 - Martin Odersky". youtube.com. Scala Days Conferences. Archived from the original on 2021-12-19. Retrieved 19 May 2021.
- ↑ Peyton Jones, Washburn & Weirich 2004, p. 3.
अग्रिम पठन
- Applications
- Augustsson, Lennart; Petersson, Kent (September 1994). "Silly type families" (PDF).
- Cheney, James; Hinze, Ralf (2003). "First-Class Phantom Types". Technical Report CUCIS TR2003-1901. Cornell University. hdl:1813/5614.
- Xi, Hongwei; Chen, Chiyan; Chen, Gang (2003). Guarded Recursive Datatype Constructors. pp. 224–235. CiteSeerX 10.1.1.59.4622. doi:10.1145/604131.604150. ISBN 978-1581136289. S2CID 15095297.
{{cite book}}:|journal=ignored (help) - Sheard, Tim; Pasalic, Emir (2004). "Meta-programming with built-in type equality". Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork. 199: 49–65. doi:10.1016/j.entcs.2007.11.012.
- Semantics
- Patricia Johann and Neil Ghani (2008). "Foundations for Structured Programming with GADTs".
- Arie Middelkoop, Atze Dijkstra and S. Doaitse Swierstra (2011). "A lean specification for GADTs: system F with first-class equality proofs". Higher-Order and Symbolic Computation.
- Type reconstruction
- Peyton Jones, Simon; Washburn, Geoffrey; Weirich, Stephanie (2004). "Wobbly types: type inference for generalised algebraic data types" (PDF). Technical Report MS-CIS-05-25. University of Pennsylvania.
- Peyton Jones, Simon; Vytiniotis, Dimitrios; Weirich, Stephanie; Washburn, Geoffrey (2006). "Simple Unification-based Type Inference for GADTs" (PDF). Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland.
- Sulzmann, Martin; Wazny, Jeremy; Stuckey, Peter J. (2006). "A Framework for Extended Algebraic Data Types". In Hagiya, M.; Wadler, P. (eds.). 8th International Symposium on Functional and Logic Programming (FLOPS 2006). Lecture Notes in Computer Science. Vol. 3945. pp. 46–64.
- Sulzmann, Martin; Schrijvers, Tom; Stuckey, Peter J. (2006). "Principal Type Inference for GHC-Style Multi-Parameter Type Classes". In Kobayashi, Naoki (ed.). Programming Languages and Systems: 4th Asian Symposium (APLAS 2006). Lecture Notes in Computer Science. Vol. 4279. pp. 26–43.
- Schrijvers, Tom; Peyton Jones, Simon; Sulzmann, Martin; Vytiniotis, Dimitrios (2009). "Complete and Decidable Type Inference for GADTs" (PDF). Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh: 341–352. doi:10.1145/1596550.1596599. ISBN 9781605583327. S2CID 11272015.
- Lin, Chuan-kai (2010). Practical Type Inference for the GADT Type System (PDF) (Doctoral Dissertation thesis). Portland State University.
- Other
- Andrew Kennedy and Claudio V. Russo. "Generalized algebraic data types and object-oriented programming". In Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications. ACM Press, 2005.
बाहरी संबंध
- Generalised Algebraic Datatype Page on the Haskell wiki
- Generalised Algebraic Data Types in the GHC Users' Guide
- Generalized Algebraic Data Types and Object-Oriented Programming
- GADTs – Haskell Prime – Trac
- Papers about type inference for GADTs, bibliography by Simon Peyton Jones
- Type inference with constraints, bibliography by Simon Peyton Jones
- Emulating GADTs in Java via the Yoneda lemma
