استخدام العالم الحقيقي لـ GADT
https://stackoverflow.com/questions/3859200
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russianسؤال
كيف يمكنني الاستفادة من نوع البيانات الجبرية المعممة؟
المثال الوارد في هاسكل ويكيبوك أقصر من أن يعطيني نظرة ثاقبة الإمكانيات الحقيقية لـ GADT.
المحلول
لقد وجدت "Monad" (من حزمة "MonadPrompt") أداة مفيدة للغاية في عدة أماكن (إلى جانب برنامج "Monad" المكافئ من الحزمة "التشغيلية" يجب استخدامها) ، فهو يتيح لك جعل اللغات المضمنة رخيصة للغاية ومرونة للغاية. كان هناك مقال جيد في قراء موناد العدد 15 تسمى "المغامرات في ثلاثة موناد" التي كان لها مقدمة جيدة للموناد السريع جنبا إلى جنب مع بعض أدوات واقعية.
نصائح أخرى
تعتبر Gadts تقريبية ضعيفة للعائلات الاستقرائية من اللغات المكتوبة بشكل متميّز - لذلك لنبدأ هناك بدلاً من ذلك.
العائلات الاستقرائية هي طريقة مقدمة نوع البيانات الأساسية بلغة مكتوبة بشكل متميز. على سبيل المثال ، في AGDA تحدد الأرقام الطبيعية مثل هذا
data Nat : Set where
zero : Nat
succ : Nat -> Nat
هذا ليس خياليًا جدًا ، إنه في الأساس نفس الشيء مثل تعريف Haskell
data Nat = Zero | Succ Nat
وبالفعل في بناء جملة GADT ، يكون شكل Haskell أكثر تشابهًا
{-# LANGUAGE GADTs #-}
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
لذلك ، في البداية ، قد تعتقد أن Gadts مجرد بناء جملة إضافي. هذا هو مجرد غيض من الجبل الجليدي رغم ذلك.
لدى AGDA القدرة على تمثيل جميع أنواع الأنواع غير المألوفة والغريبة على مبرمج Haskell. واحد بسيط هو نوع المجموعات المحدودة. هذه يكتب مكتوب مثل Fin 3 ويمثل تعيين من الأرقام {0, 1, 2}. على نفس المنوال، Fin 5 يمثل مجموعة الأرقام {0,1,2,3,4}.
هذا يجب أن يكون غريبا جدا في هذه المرحلة. أولاً ، نشير إلى نوع يحتوي على رقم عادي كمعلمة "نوع". ثانياً ، ليس من الواضح ما يعنيه Fin n لتمثيل المجموعة {0,1...n}. في AGDA الحقيقي ، كنا نفعل شيئًا أكثر قوة ، لكن من المفيد أن نقول أنه يمكننا تحديد أ contains وظيفة
contains : Nat -> Fin n -> Bool
contains i f = ?
الآن هذا غريب مرة أخرى لأن التعريف "الطبيعي" لـ contains سيكون شيئًا مثل i < n, ، لكن n هي قيمة موجودة فقط في النوع Fin n ولا ينبغي أن نكون قادرين على عبور هذا الانقسام بسهولة. على الرغم من أنه اتضح أن التعريف ليس واضحًا تقريبًا ، إلا أن هذه هي القوة التي تتمتع بها العائلات الاستقرائية بالضبط في اللغات المكتوبة بشكل متميّز - فهي تقدم القيم التي تعتمد على أنواعها وأنواعها التي تعتمد على قيمها.
يمكننا دراسة ما يدور حوله Fin هذا يعطيها تلك الخاصية من خلال النظر في تعريفها.
data Fin : Nat -> Set where
zerof : (n : Nat) -> Fin (succ n)
succf : (n : Nat) -> (i : Fin n) -> Fin (succ n)
هذا يتطلب القليل من العمل لفهمه ، لذلك ، يتيح مثالًا محاولة إنشاء قيمة من النوع Fin 2. هناك بعض الطرق للقيام بذلك (في الواقع ، سنجد أن هناك بالضبط 2)
zerof 1 : Fin 2
zerof 2 : Fin 3 -- nope!
zerof 0 : Fin 1 -- nope!
succf 1 (zerof 0) : Fin 2
هذا يتيح لنا أن نرى أن هناك نسخان ويوضح أيضًا القليل من كيفية حدوث حساب النوع. على وجه الخصوص ، (n : Nat) بت في نوع zerof يعكس الفعلي القيمة n حتى النوع الذي يسمح لنا بالتشكيل Fin (n+1) لأي n : Nat. بعد ذلك نستخدم التطبيقات المتكررة succf لزيادة لدينا Fin القيم إلى فهرس الأسرة من النوع الصحيح (الرقم الطبيعي الذي يفهرس Fin).
ما الذي يوفر هذه القدرات؟ بكل صدق ، هناك العديد من الاختلافات بين الأسرة الاستقرائية التي تم كتابتها بشكل متميز و ADT العادي ، ولكن يمكننا التركيز على الخيار الدقيق الأكثر صلة بفهم أدوات التفاهم.
في Gadts والعائلات الاستقرائية ، تحصل على فرصة لتحديد بالضبط نوع من بنائك. قد يكون هذا مملاً
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
أو ، إذا كان لدينا نوع أكثر مرونة وفهرسة ، فيمكننا اختيار أنواع عائدات مختلفة وأكثر إثارة للاهتمام
data Typed t where
TyInt :: Int -> Typed Int
TyChar :: Char -> Typed Char
TyUnit :: Typed ()
TyProd :: Typed a -> Typed b -> Typed (a, b)
...
على وجه الخصوص ، نحن نستخدم القدرة على تعديل نوع الإرجاع بناءً على خاص مُنشئ القيمة المستخدمة. يتيح لنا ذلك عكس بعض معلومات القيمة في النوع وإنتاج أكثر تحديدًا (ليلي).
إذن ماذا يمكننا أن نفعل معهم؟ حسنًا ، مع القليل من شحوم الكوع يمكننا ينتج Fin في هاسكل. بإيجاز يتطلب أن نحدد فكرة الطبيعية في الأنواع
data Z
data S a = S a
> undefined :: S (S (S Z)) -- 3
... ثم gadt لتعكس القيم في هذه الأنواع ...
data Nat where
Zero :: Nat Z
Succ :: Nat n -> Nat (S n)
... ثم يمكننا استخدام هذه للبناء Fin مثلما فعلنا في Agda ...
data Fin n where
ZeroF :: Nat n -> Fin (S n)
SuccF :: Nat n -> Fin n -> Fin (S n)
وأخيرا يمكننا بناء قيمتين بالضبط من Fin (S (S Z))
*Fin> :t ZeroF (Succ Zero)
ZeroF (Succ Zero) :: Fin (S (S Z))
*Fin> :t SuccF (Succ Zero) (ZeroF Zero)
SuccF (Succ Zero) (ZeroF Zero) :: Fin (S (S Z))
لكن لاحظنا أننا فقدنا الكثير من الراحة على العائلات الاستقرائية. على سبيل المثال ، لا يمكننا استخدام حرفيات رقمية منتظمة في أنواعنا (على الرغم من أن هذا مجرد خدعة في AGDA على أي حال) ، نحتاج إلى إنشاء "نوع NAT" و "Value Nat" واستخدام GADT لربطهم معًا ، وقد وجدنا أيضًا ، في الوقت المناسب ، أنه على الرغم من أن الرياضيات ذات المستوى النوعي مؤلم في AGDA ، يمكن القيام به. في هاسكل ، إنه أمر مؤلم بشكل لا يصدق وغالبًا ما لا يمكن.
على سبيل المثال ، من الممكن تحديد أ weaken الفكرة في أجدا Fin يكتب
weaken : (n <= m) -> Fin n -> Fin m
weaken = ...
حيث نقدم القيمة الأولى المثيرة للاهتمام للغاية ، دليل على ذلك n <= m الذي يسمح لنا بتضمين "قيمة أقل من n"في مجموعة" القيم أقل من m"يمكننا أن نفعل الشيء نفسه في هاسكل ، من الناحية الفنية ، ولكنه يتطلب إساءة استخدام شديدة لمقدمة الطبقة النوعية.
لذلك ، تشبه Gadts العائلات الاستقرائية بلغات مكتوبة بشكل أعتمد والتي تكون أضعف وأكثر جاذبية. لماذا نريدهم في هاسكل في المقام الأول؟
في الأساس لأن جميع الثوابت التي لا تتطلب من القوة الكاملة للعائلات الاستقرائية التعبير واختيار التنازلات الخاصة بين التعبير ، والتنفيذ في هاسكل ، والاستدلال على النوع.
بعض الأمثلة على تعبيرات Gadts المفيدة أشجار اللون الأحمر الأسود الذي لا يمكن أن يكون له خاصية اللون الأحمر الأسود أو حساب حساب Lambda المغطى ببساطة بمثابة تعجب من نظام Haskell من نوع Haskell.
في الممارسة العملية ، غالبًا ما ترى استخدام Gadts لسياقها الوجودي الضمني. على سبيل المثال ، النوع
data Foo where
Bar :: a -> Foo
يخفي ضمنيًا a نوع المتغير باستخدام الكمية الوجودية
> :t Bar 4 :: Foo
بطريقة تكون مريحة في بعض الأحيان. إذا نظرت بعناية ، فإن مثال HOAS من Wikipedia يستخدم هذا لـ a اكتب المعلمة في App البناء. للتعبير عن هذا البيان بدون Gadts سيكون فوضى في السياقات الوجودية ، لكن بناء جملة GADT يجعله طبيعيًا.
يمكن أن تمنحك Gadts ضمانات فرضية من النوع الأقوى من ADTs العادية. على سبيل المثال ، يمكنك فرض شجرة ثنائية على أن تكون متوازنة على مستوى النظام ، كما في هذا التنفيذ من 2-3 أشجار:
{-# LANGUAGE GADTs #-}
data Zero
data Succ s = Succ s
data Node s a where
Leaf2 :: a -> Node Zero a
Leaf3 :: a -> a -> Node Zero a
Node2 :: Node s a -> a -> Node s a -> Node (Succ s) a
Node3 :: Node s a -> a -> Node s a -> a -> Node s a -> Node (Succ s) a
كل عقدة لها عمق مشفر من النوع حيث توجد جميع أوراقها. الشجرة هي إما شجرة فارغة ، أو قيمة مفردة ، أو عقدة من العمق غير المحدد ، مرة أخرى باستخدام gadts.
data BTree a where
Root0 :: BTree a
Root1 :: a -> BTree a
RootN :: Node s a -> BTree a
يضمن لك نظام النوع أنه يمكن بناء العقد المتوازنة فقط. هذا يعني أنه عند تنفيذ العمليات مثل insert على مثل هذه الأشجار ، فإن نوع الكود الخاص بك يختبئ فقط إذا كانت النتيجة دائمًا شجرة متوازنة.
أنا أحب المثال في دليل GHC. إنه عرض سريع لفكرة GADT الأساسية: يمكنك تضمين نظام النوع للغة التي تتلاعب بها في نظام نوع Haskell. هذا يتيح لوظائف Haskell الخاصة بك افتراضها ، وتجبرهم على الحفاظ عليها ، أن أشجار بناء الجملة تتوافق مع البرامج التي تم تحديدها جيدًا.
عندما نحدد Term, ، لا يهم الأنواع التي نختارها. يمكننا الكتابة
data Term a where
...
IsZero :: Term Char -> Term Char
أو
...
IsZero :: Term a -> Term b
وتعريف Term سوف لا يزال يمر.
إنه مرة واحدة فقط نريد حساب على Term, ، كما هو الحال في التعريف eval, أن الأنواع مهمة. نحن بحاجة إلى
...
IsZero :: Term Int -> Term Bool
لأننا بحاجة إلى دعوتنا العودية إلى eval لإرجاع Int, ، ونريد أن نعود بدوره Bool.
هذا إجابة قصيرة ، لكن استشر Haskell Wikibook. إنه يسير لك على الرغم من وجود شجرة تعبير مملوكة جيدًا ، وهو مثال قانوني إلى حد ما: http://en.wikibooks.org/wiki/haskell/gadt
تستخدم Gadts أيضًا لتنفيذ المساواة بين النوع: http://hackage.haskell.org/package/type-equality. لا يمكنني العثور على الورقة المناسبة للإشارة إلى هذه السلسلة - وقد شقت هذه التقنية طريقها جيدًا إلى الفولكلور الآن. ومع ذلك ، يتم استخدامه بشكل جيد ، في أشياء Oleg المكتوبة. انظر ، على سبيل المثال القسم على التجميع المكتوبة في gadts. http://okmij.org/ftp/tagless-final/#tc-gadt
