نوع البيانات الجبرية المعممة

في البرمجة الوظيفية ، يعتبر نوع البيانات الجبرية المعمم ( GADT ، وهو أيضًا نوع الشبح من الدرجة الأولى ، ^{[ 1 ]} نوع البيانات المتكرر المحمي ، ^{[ 2 ]} أو النوع المؤهل للمساواة ^{[ 3 ]} ) تعميمًا لنوع البيانات الجبرية البارامترية (ADT).

في نوع البيانات المجردة المعممة (GADT)، يمكن لمنشئات المنتج (التي تُسمى منشئات البيانات في لغة هاسكل ) توفير تجسيد صريح لنوع البيانات المجردة (ADT) كتجسيد لنوع القيمة المُعادة. يتيح ذلك تعريف دوال ذات سلوك نوعي أكثر تقدماً. بالنسبة لمنشئ البيانات في هاسكل 2010، فإن القيمة المُعادة تحمل تجسيد النوع المُضمن في تجسيد معلمات نوع البيانات المجردة عند تطبيق المنشئ.

-- نوع بيانات تجريدي معياري ليس نوع بيانات تجريدي معمّم (GADT) قائمة البيانات a = Nil | Cons a ( قائمة البيانات a )integers :: List Int integers = Cons 12 ( Cons 107 Nil )strings :: List String strings = Cons "boat" ( Cons "dock" Nil )-- تعبير بيانات GADT حيث EBool :: Bool -> Expr Bool EInt :: Int -> Expr Int EEqual :: Expr Int -> Expr Int -> Expr Booleval :: Expr a -> a eval e = case e of EBool a -> a EInt a -> a EEqual a b -> ( eval a ) == ( eval b )expr1 :: Expr Bool expr1 = EEqual ( EInt 2 ) ( EInt 3 )ret = eval expr1 -- خطأ

يتم تطبيقها حاليًا في مُصرّف غلاسكو هاسكل (GHC) كامتداد غير قياسي، وتستخدمها، من بين أمور أخرى، Pugs و Darcs . يدعم OCaml GADT بشكل أصلي منذ الإصدار 4.00. ^{[ 4 ]}

يوفر تطبيق GHC الدعم لمعلمات النوع الكمية الوجودية وللقيود المحلية.

تم وصف نسخة مبكرة من أنواع البيانات الجبرية المعممة بواسطة Augustsson & Petersson (1994) واستندت إلى مطابقة الأنماط في ALF .

تم تقديم أنواع البيانات الجبرية المعممة بشكل مستقل من قبل تشيني وهينز (2003) ، وقبل ذلك من قبل شي، تشين وتشين (2003) كامتدادات لأنواع البيانات الجبرية في لغتي ML وهاسكل . ^{[ 5 ]} وهما متكافئان جوهريًا. وهما مشابهان لعائلات أنواع البيانات الاستقرائية (أو أنواع البيانات الاستقرائية ) الموجودة في حساب التفاضل والتكامل للإنشاءات الاستقرائية لروك ولغات أخرى ذات أنواع تابعة، باستثناء الأنواع التابعة، مع وجود قيد إضافي على الإيجابية في الأخيرة، وهو قيد غير مفروض في أنواع البيانات الجبرية المعممة. ^{[ 6 ]}

قدم سولزمان، وازني وستوكي (2006) أنواع البيانات الجبرية الموسعة التي تجمع بين أنواع البيانات الجبرية المعممة وأنواع البيانات الوجودية وقيود فئة النوع .

يُعد استنتاج النوع في غياب أي تعليق نوعي مُقدم من المبرمج غير قابل للتقرير ^{[ 7 ]} ، ولا تقبل الدوال المُعرّفة على أنواع البيانات الجبرية المعممة (GADTs) أنواعًا رئيسية بشكل عام. ^{[ 8 ]} يتطلب إعادة بناء النوع العديد من المفاضلات التصميمية، وهو مجال بحث نشط ( بيتون جونز، واشبورن ، وويريتش 2004 ؛ بيتون جونز وآخرون 2006 ).

في ربيع عام 2021، تم إصدار Scala 3.0. ^{[ 9 ]} وقد أتاح هذا التحديث الرئيسي لـ Scala إمكانية كتابة أنواع البيانات الجبرية المعممة ^{[ 10 ]} بنفس صيغة أنواع البيانات الجبرية، وهو ما لا يتوفر في لغات البرمجة الأخرى وفقًا لمارتن أوديرسكي . ^{[ 11 ]}

تشمل تطبيقات GADTs البرمجة العامة ، ونمذجة لغات البرمجة ( بناء الجملة المجرد عالي المستوى )، والحفاظ على الثوابت في هياكل البيانات ، والتعبير عن القيود في لغات المجال المضمنة ، ونمذجة الكائنات. ^{[ 12 ]}

بيانات Lam :: * -> * حيث Lift :: a -> Lam a -- ^ القيمة المرفوعة Pair :: Lam a -> Lam b -> Lam ( a , b ) -- ^ المنتج Lam :: ( Lam a -> Lam b ) -> Lam ( a -> b ) -- ^ تجريد lambda App :: Lam ( a -> b ) -> Lam a -> Lam b -- ^ تطبيق الدالة Fix :: Lam ( a -> a ) -> Lam a -- ^ النقطة الثابتة

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 )

• متغير نوعي

• صفحة أنواع البيانات الجبرية المعممة على ويكي هاسكل
• أنواع البيانات الجبرية المعممة في دليل مستخدمي GHC
• أنواع البيانات الجبرية المعممة والبرمجة كائنية التوجه
• GADTs  – Haskell Prime  – Trac مؤرشف بتاريخ 2019-04-04 في Wayback Machine
• أوراق بحثية حول استنتاج الأنواع لأنواع البيانات الجبرية المعممة ، قائمة المراجع بقلم سيمون بيتون جونز
• الاستدلال على الأنواع مع القيود ، قائمة المراجع بقلم سيمون بيتون جونز
• محاكاة أنواع البيانات الجبرية المعممة (GADTs) في جافا باستخدام مبرهنة يونيدا