كيفية جعل الدول غير الصالحة أكثر حتى لا توصف

منذ وقت ليس ببعيد ، تمت ترجمة مقالة في هبر حول كيفية استخدام أنواع البيانات الجبرية للتأكد من أن الحالات غير الصحيحة لا يمكن التعبير عنها. ننظر اليوم إلى طريقة أكثر عمومية وقابلة للتوسيع وآمنة للتعبير عن ما لا يمكن التعبير عنه ، وسوف يساعدنا هاسكل في ذلك.

باختصار ، تناقش هذه المقالة بعض الكيانات مع عنوان بريدي وعنوان بريد إلكتروني ، وكذلك مع الشرط الإضافي الذي يجب أن يكون هناك واحد على الأقل من هذه العناوين. كيف يقترح التعبير عن هذا الشرط على مستوى النوع؟ يقترح كتابة العناوين على النحو التالي:

type ContactInfo = | EmailOnly of EmailContactInfo | PostOnly of PostalContactInfo | EmailAndPost of EmailContactInfo * PostalContactInfo 

ما المشاكل التي يعاني منها هذا النهج؟

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

شارك

كيف تحل هذه المشكلة؟ دعونا نحاول التخيل. أولاً نقوم بتحليل وفصل فئة العنوان (على سبيل المثال ، البريد / البريد الإلكتروني / رقم المكتب في المكتب) والمحتويات المقابلة لهذه الفئة:

 data AddrType = Post | Email | Office 

لن نفكر في المحتوى حتى الآن ، لأنه لا يوجد شيء عنه في الشروط المرجعية لصلاحية قائمة العناوين.

إذا تحققنا من الحالة المقابلة في وقت تشغيل بعض مُنشئ بعض لغة OOP العادية ، فسنكتب فقط وظيفة مثل

 valid :: [AddrType] -> Bool valid xs = let hasNoDups = nub xs == xs --      hasPost = Post `elem` xs hasEmail = Email `elem` xs hasOffice = Office `elem` xs in hasNoDups && (hasPost || (hasEmail && hasOffice)) 

وسوف يلقي ببعض الإعدام إذا أعاد False .

هل يمكننا بدلاً من ذلك التحقق من حالة مماثلة بمساعدة عداد وقت عند الترجمة؟ اتضح أنه نعم ، يمكننا ، إذا كان نظام نوع اللغة معبرًا بما فيه الكفاية ، وبقية المقالة سنختار هذا النهج.

هنا ، ستساعدنا الأنواع التابعة كثيرًا ، وبما أن الطريقة الأكثر ملاءمة لكتابة رمز تم التحقق منه في هاسكل هي كتابته في Agde أو Idris أولاً ، فسنغير أحذيتنا ونكتب في Idris. بناء جملة idris قريب جدًا من Haskell: على سبيل المثال ، مع الوظيفة المذكورة أعلاه ، ما عليك سوى تغيير التوقيع قليلاً:

 valid : List AddrType -> Bool 

تذكر الآن أنه بالإضافة إلى فئات العناوين ، نحتاج أيضًا إلى محتوياتها ، ونرمز إلى اعتماد الحقول على فئة العنوان كـ GADT:

 data AddrFields : AddrType -> Type where PostFields : (city : String) -> (street : String) -> AddrFields Post EmailFields : (email : String) -> AddrFields Email OfficeFields : (floor : Int) -> (desk : Nat) -> AddrFields Office 

بمعنى ، إذا تم AddrFields t قيمة fields النوع AddrFields t ، فإننا نعلم أن t هي بعض AddrType AddrType وأن fields تحتوي على مجموعة من الحقول المقابلة لهذه الفئة المحددة.

 addrFields : AddrType -> Type addrFields Post = PostFields addrFields Email = EmailFields addrFields Office = OfficeFields 

ما العنوان الكامل في هذا النموذج؟ هذا زوج من فئة العنوان والحقول المقابلة:

 Addr : Type Addr = (t : AddrType ** AddrFields t) 

سيقول محبو نظرية النوع أن هذا نوع تابع وجودي: إذا تم إعطاؤنا بعض القيمة من النوع Addr ، فهذا يعني أن هناك قيمة t النوع AddrType ومجموعة مقابلة من حقول AddrFields t . بطبيعة الحال ، تكون عناوين فئة مختلفة من نفس النوع:

 someEmailAddr : Addr someEmailAddr = (Email ** EmailFields "that@feel.bro") someOfficeAddr : Addr someOfficeAddr = (Office ** OfficeFields (-2) 762) 

علاوة على ذلك ، إذا تم منح EmailFields Email لنا ، فإن فئة العنوان الوحيدة المناسبة هي Email ، حتى تتمكن من EmailFields ، EmailFields الموقت بنفسك:

 someEmailAddr : Addr someEmailAddr = (_ ** EmailFields "that@feel.bro") someOfficeAddr : Addr someOfficeAddr = (_ ** OfficeFields (-2) 762) 

نكتب وظيفة مساعدة تقدم قائمة مناظرة لفئات العناوين من قائمة العناوين ، ونعممها فورًا للعمل على ممر تعسفي:

 types : Functor f => f Addr -> f AddrType types = map fst 

هنا ، يتصرف نوع Addr الوجودي مثل زوجين مألوفين: على وجه الخصوص ، يمكنك أن تطلب المكون الأول AddrType (مهمة بعلامة النجمة: لماذا لا يمكنني طلب المكون الثاني؟).

ارفع

ننتقل الآن إلى جزء رئيسي من قصتنا. لذا ، لدينا List Addr بعناوين List Addr وبعض المسندات valid : List AddrType -> Bool ، والتي نريد ضمان تنفيذها لهذه القائمة على مستوى الأنواع. كيف نجمعهم؟ بالطبع ، نوع آخر!

 data ValidatedAddrList : List Addr -> Type where MkValidatedAddrList : (lst : List Addr) -> (prf : valid (types lst) = True) -> ValidatedAddrList lst 

الآن سنقوم بتحليل ما كتبناه هنا.

data ValidatedAddrList : List Addr -> Type where يعني أن النوع ValidatedAddrList معلماته ، في الواقع ، من خلال قائمة العناوين.

لنلق نظرة على توقيع مُنشئ MkValidatedAddrList الوحيد من هذا النوع: (lst : List Addr) -> (prf : valid (types lst) = True) -> ValidatedAddrList lst . أي أنها تأخذ بعض قائمة عناوين lst prf أخرى من النوع prf valid (types lst) = True . ماذا يعني هذا النوع؟ يعني ذلك أن القيمة الموجودة على يسار = تساوي القيمة على يمين = ، أي أنها valid (types lst) ، في الواقع ، هي True.

كيف يعمل؟ التوقيع = يشبه (x : A) -> (y : B) -> Type . هذا يعني أن = يأخذ قيمتين عشوائيتين x و y (ربما حتى من نوعين مختلفين A و B ، مما يعني أن عدم المساواة في idris غير متجانس ، وأنه غامض إلى حد ما من وجهة نظر نظرية النوع ، ولكن هذا موضوع لمناقشة أخرى). ثم ما يدل على المساواة؟ وبسبب حقيقة أن المنشئ الوحيد = - Refl بتوقيع يكاد يكون (x : A) -> x = x . أي ، إذا كانت لدينا قيمة من النوع x = y ، فإننا نعلم أنه تم بناؤه باستخدام Refl (لأنه لا يوجد Refl آخرون) ، مما يعني أن x تساوي y الواقع.

لاحظ أن هذا هو السبب في Haskell سوف نتظاهر دائمًا في أحسن الأحوال بأننا نثبت شيئًا ، لأن Haskell قد حدد أن يسكن أي نوع ، لذلك لا تعمل الحجة المذكورة أعلاه هناك: لأي x ، y مصطلح من النوع x = y يمكن إنشاؤه عبر undefined (أو من خلال العودية اللانهائية ، قل أنه بشكل عام هو نفسه من حيث نظرية النوع).

نلاحظ أيضًا أن المساواة هنا لا تعني بمعنى Haskell's Eq أو أي operator== في C ++ ، ولكنها أكثر صرامة إلى حد كبير: الهيكلية ، والتي ، تبسيطًا ، تعني أن القيمتين لها نفس الشكل . وهذا يعني أن خداعه ببساطة لا يعمل. لكن قضايا المساواة تنجذب تقليديا إلى مادة منفصلة.

لتعزيز فهمنا للمساواة ، نكتب اختبارات الوحدة للوظيفة valid :

 testPostValid : valid [Post] = True testPostValid = Refl testEmptyInvalid : valid [] = False testEmptyInvalid = Refl testDupsInvalid : valid [Post, Post] = False testDupsInvalid = Refl testPostEmailValid : valid [Post, Email] = True testPostEmailValid = Refl 

هذه الاختبارات جيدة من حيث أنك لا تحتاج حتى إلى تشغيلها ، ويكفي أن يقوم المشغل بفحصها. في الواقع ، لنستبدل True بـ False ، على سبيل المثال ، في أولها ونرى ما سيحدث:

 testPostValid : valid [Post] = False testPostValid = Refl 

يقسم Typsekher

كما هو متوقع. عظيم

تبسيط

الآن دعونا إعادة بناء قائمة ValidatedAddrList قليلاً.

أولاً ، إن نمط مقارنة قيمة معينة مع True شائع تمامًا ، لذلك هناك نوع خاص So في إدريس لهذا: يمكنك أن تأخذ So x كمرادف لـ x = True . لنصلح تعريف ValidatedAddrList :

 data ValidatedAddrList : List Addr -> Type where MkValidatedAddrList : (lst : List Addr) -> (prf : So (valid $ types lst)) -> ValidatedAddrList lst 

بالإضافة إلى ذلك ، So لديه وظيفة مساعدة ملائمة choose ، والتي في جوهرها ترفع التحقق إلى مستوى الأنواع:

 > :doc choose Data.So.choose : (b : Bool) -> Either (So b) (So (not b)) Perform a case analysis on a Boolean, providing clients with a So proof 

سيكون من المفيد لنا عندما نكتب وظائف تعديل هذا النوع.

ثانيًا ، في بعض الأحيان (خاصة في التطوير التفاعلي) يمكن prf العثور على قيمة prf المناسبة بمفردها. من أجل أنه في مثل هذه الحالات ، لم يكن من الضروري بنائه يدويًا ، هناك سكر نحوي مناظر:

 data ValidatedAddrList : List Addr -> Type where MkValidatedAddrList : (lst : List Addr) -> {auto prf : So (valid $ types lst)} -> ValidatedAddrList lst 

الأقواس المتعرجة تعني أن هذه حجة ضمنية بأن إدريس سيحاول الانسحاب من السياق ، ويعني auto أنه سيحاول أيضًا بناءه بنفسه.

إذن ماذا تعطينا قائمة ValidatedAddrList الجديدة هذه؟ ويعطي مثل هذه السلسلة من الاستدلال: val قيمة من النوع ValidatedAddrList lst . هذا يعني أن lst عبارة عن قائمة عناوين ، بالإضافة إلى ذلك ، تم إنشاء val باستخدام مُنشئ MkValidatedAddrList ، الذي مررنا به هذا lst وقيمة prf أخرى من النوع So (valid $ types lst) ، وهو valid (types lst) = True تقريبًا valid (types lst) = True . وحتى نتمكن من بناء prf ، نحتاج ، في الواقع ، لإثبات أن هذه المساواة prf .

والشيء الأجمل هو أن كل هذا يتم فحصه عن طريق الطبلة. نعم ، يجب أن يتم التحقق من الصلاحية في وقت التشغيل (لأنه يمكن قراءة العناوين من ملف أو من الشبكة) ، ولكن العداد يضمن أن يتم هذا التحقق: بدونه ، من المستحيل إنشاء ValidatedAddrList . على الأقل في ادريس. في هاسكل ، للأسف.

أدخل

للتحقق من حتمية التحقق ، سنحاول كتابة وظيفة لإضافة عنوان إلى القائمة. المحاولة الأولى:

 insert : (addr : Addr) -> ValidatedAddrList lst -> ValidatedAddrList (addr :: lst) insert addr (MkValidatedAddrList lst) = MkValidatedAddrList (addr :: lst) 

كلا ، المدقق الإملائي يعطي الأصابع (على الرغم من أنه غير قابل للقراءة للغاية ، فإن تكلفة valid معقدة للغاية):

كيف نحصل على نسخة من هذا So ؟ لا شيء غير choose المذكور أعلاه. المحاولة الثانية:

 insert : (addr : Addr) -> ValidatedAddrList lst -> ValidatedAddrList (addr :: lst) insert addr (MkValidatedAddrList lst) = case choose (valid $ types (addr :: lst)) of Left l => MkValidatedAddrList (addr :: lst) Right r => ?rhs 

تقريبا typechetsya. "تقريبًا" لأنه من غير الواضح ما الذي يجب استبداله rhs . بدلاً من ذلك ، من الواضح: في هذه الحالة ، يجب على الوظيفة الإبلاغ عن خطأ بطريقة أو بأخرى. لذلك ، تحتاج إلى تغيير التوقيع ولف القيمة المرتجعة ، على سبيل المثال ، في Maybe :

 insert : (addr : Addr) -> ValidatedAddrList lst -> Maybe (ValidatedAddrList (addr :: lst)) insert addr (MkValidatedAddrList lst) = case choose (valid $ types (addr :: lst)) of Left l => Just $ MkValidatedAddrList (addr :: lst) Right r => Nothing 

هذا مبلط ويعمل كما ينبغي.

ولكن الآن ظهرت المشكلة التالية غير الواضحة ، والتي كانت في الواقع في المقالة الأصلية. لا يتوقف نوع هذه الوظيفة عن كتابة مثل هذا التنفيذ:

 insert : (addr : Addr) -> ValidatedAddrList lst -> Maybe (ValidatedAddrList (addr :: lst)) insert addr (MkValidatedAddrList lst) = Nothing 

أي نقول دائمًا أنه لا يمكننا بناء قائمة عناوين جديدة. Typhechaetsya؟ نعم هل هذا صحيح؟ حسنا ، بالكاد. هل يمكن تجنب ذلك؟

اتضح أنه ممكن ، ولدينا كل الأدوات اللازمة لذلك. في حالة نجاح ذلك ، insert ValidatedAddrList ، والتي تحتوي على دليل على هذا النجاح. لذا أضف تناظرًا أنيقًا واطلب من الوظيفة أن ترجع أيضًا إلى دليل على الفشل!

 insert : (addr : Addr) -> ValidatedAddrList lst -> Either (So (not $ valid $ types (addr :: lst))) (ValidatedAddrList (addr :: lst)) insert addr (MkValidatedAddrList lst) = case choose (valid $ types (addr :: lst)) of Left l => Right $ MkValidatedAddrList (addr :: lst) Right r => Left r 

لا يمكننا الآن أخذ Nothing وإعادته دائمًا.

يمكنك أن تفعل الشيء نفسه لوظائف إزالة العنوان وما شابه ذلك.

دعونا نرى كيف يبدو كل شيء الآن في النهاية.

لنحاول إنشاء قائمة عناوين فارغة:

من المستحيل ، قائمة فارغة غير صالحة.

ماذا عن قائمة من العنوان البريدي فقط؟

حسنًا ، دعنا نحاول إدراج العنوان البريدي في القائمة التي تحتوي بالفعل على العنوان البريدي:

دعنا نحاول إدخال البريد الإلكتروني:

في النهاية ، يعمل كل شيء تمامًا كما هو متوقع.

Phew. اعتقدت أنها ستكون ثلاثة أسطر ، ولكن تبين أنها أطول قليلاً. لنستكشف إلى أي مدى يمكن أن نذهب في Haskell ، سنكون في المقالة التالية. في غضون ذلك ، قليلا

تأمل

ما هو في النهاية ربح مثل هذا القرار مقارنة بالقرار الوارد في المقالة ، والذي أشرنا إليه في البداية؟

1. مرة أخرى ، هو أكثر قابلية للتطوير. وظائف التحقق المعقدة أسهل في الكتابة.
2. إنه أكثر عزلة. لا يجب أن يعرف رمز العميل ما بداخل وظيفة التحقق من الصحة ، في حين أن نموذج ContactInfo من المقالة الأصلية يتطلب ربطه.
3. تتم كتابة منطق التحقق في شكل وظائف عادية ومألوفة ، بحيث يمكن التحقق منه على الفور من خلال القراءة المدروسة واختباره من خلال اختبارات وقت الترجمة ، بدلاً من اشتقاق معنى التحقق من نموذج نوع البيانات الذي يمثل نتيجة تم التحقق منها بالفعل.
4. يصبح من الممكن تحديد سلوك الوظائف التي تعمل مع نوع البيانات التي تهمنا بشكل أكثر دقة ، خاصة في حالة عدم اجتياز الاختبار. على سبيل المثال ، من المستحيل ببساطة كتابة insert المكتوب كنتيجة غير صحيحة . وبالمثل ، يمكن للمرء أن يكتب insertOrReplace و insertOrIgnore وما شابه ، والذي تم تحديد سلوكه بالكامل في النوع.

ما هو الربح مقارنة بحل OOP مثل هذا؟

 class ValidatedAddrListClass { public: ValidatedAddrListClass(std::vector<Addr> addrs) { if (!valid(addrs)) throw ValidationError {}; } }; 

1. الكود أكثر نمطيًا وأمانًا. في الحالة المذكورة أعلاه ، فإن الشيك هو إجراء يتم فحصه مرة واحدة ، والذي نسي حوله لاحقًا. كل شيء مبني على الصدق وفهم أنه إذا كان لديك ValidatedAddrListClass ، فإن تنفيذه قام بإجراء فحص هناك. لا يمكن اختيار حقيقة هذا الاختيار من الفصل كقيمة معينة. في حالة وجود قيمة من نوع ما ، يمكن نقل هذه القيمة بين أجزاء مختلفة من البرنامج ، وتستخدم لبناء قيم أكثر تعقيدًا (على سبيل المثال ، مرة أخرى ، رفض هذا الاختيار) ، والتحقيق (انظر الفقرة التالية) ، وعمومًا تفعل نفس الشيء الذي اعتدنا القيام به مع القيم.
2. يمكن استخدام عمليات التحقق هذه في مطابقة النمط (التابع). صحيح ، ليس في حالة هذه الوظيفة valid وليس في حالة إدريس ، فهي معقدة بشكل مؤلم ، وإدريس مملة بشكل مؤلم بحيث يمكن استخراج المعلومات المفيدة للأنماط من البنية valid . ومع ذلك ، يمكن إعادة كتابة الصالح بأسلوب أكثر ملاءمة لمطابقة الأنماط ، ولكن هذا يتجاوز نطاق هذه المقالة وليس بشكل عام تافهًا في حد ذاته.

ما هي عيوبه؟

أرى عيبًا أساسيًا واحدًا خطيرًا: فالصلاح valid لوظيفة غبية جدًا. تقوم بإرجاع جزء واحد فقط من المعلومات - سواء اجتازت البيانات التحقق من الصحة أم لا. في حالة الأنواع الأكثر ذكاءً ، يمكننا تحقيق شيء أكثر إثارة للاهتمام.

على سبيل المثال ، تخيل أن شرط تفرد العناوين قد اختفى من المعارف التقليدية. في هذه الحالة ، من الواضح أن إضافة عنوان جديد إلى قائمة العناوين الحالية لن يجعل القائمة غير صالحة ، لذلك يمكننا إثبات هذه النظرية عن طريق كتابة دالة من النوع So (valid $ types lst) -> So (valid $ types $ addr :: lst) ، واستخدمها ، على سبيل المثال ، لكتابة آمن للنوع دائمًا

 insert : (addr : Addr) -> ValidatedAddrList lst -> ValidatedAddrList (addr :: lst) 

ولكن ، للأسف ، النظريات مثل العودية والاستقراء ، ولا تحتوي مشكلتنا على أي هيكل استقرائي أنيق ، لذلك ، في رأيي ، فإن الكود مع البلوط البلولي الصالح ليس سيئًا أيضًا.