مادة لتعلم gadt

Question

بدأت أقرأ عن Gadt في Haskell Wiki لكنني لم أشعر بالراحة تمامًا في فهمه. هل تنصح بفصل كتاب محدد أو منشور مدونة يشرح GADT للمبتدئين في هاسكل؟

Answer 1

لقد صنعت Apfelmus فيديو تعليمي لـ Gadts والتي قد تكون مفيدة.

Answer 2

أنا أحب المثال في دليل GHC. الأمر بسيط ، ويوضح بعض النقاط الرئيسية:

• تتيح لك Gadts استخدام نظام نوع Haskell لتصميم نظام النوع للغة التي تقوم بتنفيذها ("لغة الكائن")

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

• نمط مطابقة مُنشئ GADT يسبب تحسين النوع. eval لديه النوع Term a -> a عموما ، ولكن الجانب الأيمن ل eval (Lit i) لديه النوع Int, ، لأن المنشئ الأيسر كان له نوع Term Int.

• لا يهتم نظام Haskell بأنواعها التي تعطيها مُنشئو GADT. يمكننا بسهولة جعل كل مُنشئ data Term a أعط نتيجة النوع Term a, ، أو Term Bool, ، و ال data التعريف لا يزال يمر. لكننا لن نتمكن من الكتابة eval :: Term a -> a. يمكنك اختيار "أنواع العلامات" GADT للنموذج لك المشكلة ، بحيث تكون الوظائف المفيدة التي تريد كتابتها جيدة.

Answer 3

روابط أخرى:

• http://www.haskell.org/haskellwiki/generalised_algebraic_datatype
• http://www.comlab.ox.ac.uk/people/ralf.hinze/talks/fop.pdf

Answer 4

هاسكل ويكي أدوات للدمى هو أفضل تفسير رأيته.

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

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