شكوك حول سلوك نوع الوحدة في نظام الكتابة

Question

لدي شك حول نوع الوحدة في سياق نظرية النوع واستخدامها في سيناريوهات الحالات المختلفة.

لتبدأ، أ نوع الوحدة يمكن اعتباره نوع منتج فارغ، وهو الوحدة، مع مصطلح قيمة واحد فقط وهو الصف الفارغ، ().كما يوجد أ فريد خريطة من أي نوع إلى الوحدة.

الآن، يحدث أن استخدام نوع الوحدة يتجاوز هذا التعريف التافه، ويستخدم في الواقع في تعريف أنواع البيانات الجبرية، وهي مجموع أنواع المنتجات.على وجه التحديد، من الممكن تمثيل مفهوم نوع معدود باستخدام مجموع أنواع الوحدات، على سبيل المثال.في StandardML قد يكون لدينا:

datatype suit = HEARTS | CLUBS | DIAMONDS | SPADES

حيث تكون القلوب والأندية والألماس والبستوني أنواع منتجات فارغة، وبالتالي جميعها متماثلة في الوحدة.

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

Answer 1

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

لاحظ أن جانب مطابقة النمط متعامد:يمكنك التفكير في أنواع الوحدات الخمسة على أنها موجودة بشكل منفصل.في معظم نظريات النوع، يمكنك جمع مجموع أي نوعين، حتى النوعين المتساويين (اسميًا)، على سبيل المثال. Unit + Unit.سيظل مطلوبًا منك مطابقة النمط، وسيكون لديك حالتان:اليسار Unit والحق Unit.الجانب الاسمي غير مهم، على الرغم من أن العديد من لغات البرمجة ستستخدم الأسماء للتمييز بين الحالات المختلفة مثل هذه، بدلاً من مؤشرات الجمع (على وجه الخصوص، في اللغات التي يُسمح لك فيها فقط بأخذ مجاميع من الأنواع الاسمية المميزة، مثل معيار مل).