مرحبا يا هبر.
في اليوم الآخر ، في أحد مشاريع هوايتي ، نشأت المهمة في كتابة مستودع للمقاييس.
تم حل المهمة نفسها ببساطة شديدة ، ولكن مشكلتي في Haskell (خاصة في مشاريع الترفيه الخاصة بي) هي أنه من المستحيل تحمل المشكلة وحلها. من الضروري أن تقرر وتوسع وتُجرِز وتُجرِز ثم تتوسع أكثر. لذلك ، أردت أن اجعل تخزين المقاييس قابلاً للامتداد حتى لا أحدد مسبقًا ما ستكون عليه. هذا في حد ذاته موضوع لمقال منفصل ، واليوم سننظر في مكون صغير واحد: كتابة غلاف آمن للنوع لأنواع لم تكن معروفة من قبل. شيء مثل الكتابة الديناميكية ، ولكن مع ضمانات ثابتة بأننا لن نفعل هراء.
أعتقد أن المقالة لن تفتح أي شيء جديد على Haskellists ذوي الخبرة ، ولكن الآن سنضع على الأقل هذا العنصر خارج الصندوق ولن نلهيه في مقالات لاحقة. حسنًا ، أو قد لا تكون متواضعًا جدًا وتقول إنني أتيت بالفعل بنمط تصميم كامل.
لذلك ، أولا نحن صياغة المشكلة. يجب أن نكون قادرين على ربط بعض الكائنات بقيم أنواع غير معروفة سابقًا. أو بمعنى آخر ، من الضروري أن تعمل قيم الأنواع غير المعروفة سابقًا كمفاتيح في نوع من الخريطة.
بطبيعة الحال ، لسنا مجانين ولن نطلب دعم القيم من أي نوع. نطلب أن النوع (حتى لو كان غير معروف) يدعم المقارنة بمعنى الطلب. في مصطلحات Haskell ، هذا يعني أننا ندعم الأنواع التي تنفذ فئة Ord a .
لاحظ أننا يمكن أن نطلب الدعم لأخذ علامة التجزئة والتحقق من المساواة ، ولكن لعدد من الأسباب سيكون أكثر ملاءمة وضوحا أن نقتصر على المقارنة.
عندما يتعلق الأمر بتخزين القيم المعروفة بتطبيق نوع ما من الفصل ، عادة ما تستخدم الأنواع الوجودية في Haskell:
data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd
لذلك ، إذا حصلنا على كائن من النوع SomeOrd وقمنا بإجراء مطابقة للنمط له:
foo :: SomeOrd -> Bar foo (MkSomeOrd val) = ... (1) ...
ثم عند النقطة (1) لا نعرف نوع val ، لكننا نعرف (والأهم من ذلك ، أن جهاز ضبط الوقت يعرف أيضًا) أن val ينفذ فئة Ord الزمنية.
ومع ذلك ، إذا كانت وظائف الكتابة للفئة تتضمن وسيطين (أو أكثر) ، فإن استخدام مثل هذا السجل يكون ذا فائدة قليلة:
tryCompare :: SomeOrd -> SomeOrd -> Bool tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ?
لاستخدام أساليب Ord ، من الضروري أن تكون val و val2 نفس النوع ، لكن هذا لا يجب القيام به على الإطلاق! اتضح أن SomeOrd لدينا SomeOrd طائل منه. ماذا تفعل؟
على الرغم من حقيقة أن Haskell هي لغة مترجمة ذات محو من النوع العدواني (بعد التحويل البرمجي ، فهي ليست موجودة بشكل عام) ، لا يزال بإمكان المترجم إنشاء ممثلين لنوع وقت التشغيل إذا طلب منهم ذلك. ممثل دور النوع a هو قيمة النوع TypeRep a و طلب يتم الرد على إنشاء جيل من Typeable .
بالمناسبةبالمناسبة ، ليس من الضروري أن يكون نوع ما بالمعنى المعتاد ، أي أنه ينتمي إلى مجموعة متنوعة * . يمكن أن يكون أي نوع آخر من k ، والذي يسمح لك نظريًا بالقيام ببعض الأشياء الرائعة من خلال تخزين ممثلي وقت التشغيل من الأنواع المستفادة وما شابه ذلك ، لكنني لم أتمكن من معرفة ما هو بالضبط.
بالإضافة إلى ذلك ، إذا كان لدينا rep1 :: TypeRep a, rep2 :: TypeRep b من rep1 :: TypeRep a, rep2 :: TypeRep b ، فيمكننا مقارنتهما والتحقق مما إذا كانا يمثلان نفس النوع أم لا. علاوة على ذلك ، إذا كانوا يمثلون بالفعل نفس النوع ، فمن الواضح أنه يتزامن مع b . والأهم من ذلك ، ترجع وظيفة التحقق من تمثيلات النوع من أجل المساواة نتيجة يمكن أن تقنع مطبوع هذا:
eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b)
ما هذا الهراء المكتوب هنا؟
أولاً ، eqTypeRep هي دالة.
ثانياً ، إنه متعدد الأشكال ، ولكن ليس فقط حسب النوع ، ولكن أيضًا حسب أنواع مختلفة من هذه الأنواع. يشار إلى ذلك من خلال الجزء forall k1 k2 (a :: k1) (b :: k2) - وهذا يعني أن a و b لا يمكن أن يكونا فقط الأنواع العادية مثل Int أو [String] ، ولكن أيضًا ، على سبيل المثال ، المنشئات سيئة السمعة (انظر DataKinds ومحاولات أخرى لجعل هاسكل مصدقة). لكننا لسنا بحاجة إلى كل هذا.
ثالثًا ، يقبل عرضين لوقت التشغيل لأنواع مختلفة محتملة ، TypeRep a و TypeRep b .
رابعا ، تقوم بإرجاع قيمة نوع Maybe (a :~~: b) . الشيء الأكثر إثارة للاهتمام يحدث هنا.
إذا لم تتطابق الأنواع ، فسوف تُرجع الدالة Nothing المعتادة ، وكل شيء على ما يرام. إذا كانت الأنواع متطابقة ، فسوف تُرجع الدالة Just val ، حيث يكون val من النوع a :~~: b . دعونا نرى ما هو نوع:
الآن دعنا نتحدث. لنفترض أننا حصلنا على قيمة val من النوع a :~~: b . كيف يمكن بناءه؟ الطريقة الوحيدة هي مع مُنشئ HRefl ، وهذا المُنشئ يتطلب ذلك على جانبي الرمز :~~: يجب أن يكون هو نفسه. لذلك ، يتزامن مع b . علاوة على ذلك ، إذا كنا zapternnom- مباراة على val ، فإن taypcheker سوف تعرف عن ذلك أيضا. لذلك ، نعم ، تقوم دالة eqTypeRep بإرجاع دليل على أن نوعين مختلفين يحتمل أن eqTypeRep إذا كانا متساويين بالفعل.
ومع ذلك ، في الفقرة أعلاه ، كذبت. لا أحد يمنعنا من الكتابة في هاسكل شيء من هذا القبيل
wrong :: Int :~~: String wrong = wrong
أو
wrong :: Int :~~: String wrong = undefined
أو كسر النظام مع مجموعة من الطرق أقل وضوحا قليلا. هذا هو واحد من مظاهر المعروفة في دوائر ضيقة قائلا أن هاسكل غير متناسق مع المنطق. في اللغات ذات أنظمة الكتابة الأقوى ، لا يتم ختم هذه التعريفات.
هذا هو السبب في قطعة من الوثائق المذكورة أعلاه ، يتم ذكر قيمة الإنهاء . كلا الخيارين لتطبيق wrong أعلاه لا ينتج عن هذه القيمة النهائية للغاية ، مما يعطينا القليل من السبب والثقة: إذا تم إنهاء برنامجنا على Haskell (ولم يتم تشغيله إلى undefined ) ، فإن نتائجه تتوافق مع الأنواع المكتوبة. ومع ذلك ، هناك بعض التفاصيل المتعلقة بالكسل ، لكننا لن نفتح هذا الموضوع.
وبالمناسبة ، فإن المظهر الثاني لضعف Haskell في الكود أعلاه هو نوع وظيفة eqTypeRep . في اللغات الأقوى ، ستُرجع قيمة نوع أقوى ، وهذا لن يثبت فقط المساواة في الأنواع إذا كانت متساوية بالفعل ، ولكن سيثبت أيضًا عدم المساواة إذا كانت غير متساوية بالفعل. ومع ذلك ، فإن عدم تناسق منطق هاسكل يجعل هذه الوظائف عديمة الجدوى: من الأهمية بمكان أن تستخدم اللغة كدليل على النظريات ، وليس كلغة برمجة ، ولا تستخدم هاسكل كدليل.
حسنًا ، بما يكفي من نظرية السجل والنوع ، دعنا نعود إلى مقاييسنا. الآن فقط ارسم بومة تشير المناقشة أعلاه إلى أنه يكفي تخزين هذا النوع من الوجود أيضًا ، وهذا هو أفضل تمثيل للنوع ، وسيكون كل شيء على ما يرام.
هذا يقودنا إلى التنفيذ التالي لنوع المجمع:
data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn toDyn val = Dyn (typeOf val) val
نكتب الآن وظيفة تأخذ ما يلي:
- قيمتين من النوع
Dyn ؛ - وظيفة تنتج شيئا لقيمتين من أي نوع ،
بناءً فقط على الثوابت المذكورة عند إنشاء Dyn ( forall مسؤول عن ذلك) ،
والذي يسمى إذا كانت كل القيم مخزن Dyn من نفس النوع ؛ - والدالة الاحتياطية ، والتي تسمى بدلاً من الوظيفة السابقة ، إذا كانت الأنواع لا تزال مختلفة:
withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2
SomeTypeRep عبارة عن مجمّع وجودي عبر TypeRep a لأي.
الآن يمكننا تنفيذ ، على سبيل المثال ، فحص المساواة والمقارنة:
instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare
لقد SomeTypeRep هنا من حقيقة أن SomeTypeRep يمكن مقارنتها مع بعضها البعض ، لذلك تتم مقارنة الوظيفة الاحتياطية SomeTypeRep أيضًا.
القيام به.
الآن فقط من الخطيئة عدم التعميم: نلاحظ أنه في Dyn و toDyn و withDyns لا نستخدم Ord وجه التحديد ، وقد يكون هذا أي مجموعة أخرى من الثوابت ، لذلك يمكننا تمكين امتداد ConstraintKinds وتعميمه عن طريق تحديد Dyn محددة من القيود التي اللازمة في مهمتنا المحددة:
data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2
عندئذٍ سيكون Dyn Ord نوع Dyn Monoid ، على سبيل المثال ، سيتيح لك Dyn Monoid التعسفية والقيام بشيء أحادي.
دعنا نكتب الحالات التي نحتاجها Dyn جديد:
instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare
... هذا فقط لا يعمل. لا يعرف typecher أن Dyn Ord ينفذ أيضًا Eq ،
لذلك عليك نسخ التسلسل الهرمي بأكمله:
instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare
حسنا ، الآن بالتأكيد.
... ربما ، في Haskell الحديثة ، يمكنك إجراؤها بحيث يعرض المؤقت نفسه مثيلات النموذج
instance C_i (Dyn (C_1, ... C_n)) where ...
نظرًا لوجود شيء ما غير منطقي ، لكنني لم أفعل ذلك بعد ، سيتعين علي الجلوس لاختياره. ترقبوا.
وأيضًا ، إذا قمت بالتحديق بعناية ، يمكنك أن ترى أن Dyn لدينا تبدو بشكل Dyn للريبة مثل زوج تابع من النوع (ty : Type ** val : ty) من اللغات المشفرة. ولكن فقط باللغات المعروفة لي ، من المستحيل مطابقة النوع ، لأنه يتم تفسير المعلمة (والتي في هذه الحالة ، IMHO ، على نطاق واسع للغاية) ، ولكن هنا يبدو ممكنًا.
لكن الشيء الأكثر أهمية - الآن يمكنك الحصول على شيء مثل Map (Dyn Ord) SomeValue واستخدام أي قيم كمفاتيح ، طالما أنها نفسها تدعم المقارنة. على سبيل المثال ، يمكن استخدام المعرفات ذات الأوصاف المترية كمفاتيح ، ولكن هذا موضوع للمقال التالي.