تسهيلات لتوليد أنواع Haskell في Haskell ("من الدرجة الثانية Haskell")؟

Question

الاعتذار مقدمًا إذا كان هذا السؤال غامضًا بعض الشيء. إنها نتيجة لبعض أحلام اليقظة في عطلة نهاية الأسبوع.

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

لديك طريقة لطيفة للنظام للتعبير عن ذلك v1 و v2 هي عناصر مساحة المتجه V وذلك w هو عنصر مساحة المتجه W. يتيح لك نظام الكتابة كتابة برنامج يضيف v1 و v2, ، لكن لا v1 و w. رائعة! ولكن في الممارسة العملية ، قد ترغب في اللعب بمئات مساحات المتجهات المحتملة ، وبالتأكيد لا ترغب في إنشاء أنواع V1, V2, ..., V100 وأعلن عن مثيلات الفضاء المتجه typeclass! أو ربما تقرأ بعض البيانات من العالم الحقيقي مما يؤدي إلى الرموز a, b و c - قد ترغب في التعبير عن أن مساحة المتجه المجانية على هذه الرموز هي حقًا مساحة متجه!

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

يحرر: الآن اكتشفت للتو Fundeps. يجب أن أفكر قليلاً في كيفية ارتباطها بسؤالي (يتم تقدير التعليقات المنير فيما يتعلق بذلك).

Answer 1

قالب هاسكل يسمح هذا. ال صفحة ويكي لديه بعض الروابط المفيدة. خصوصا بولات دروس.

بناء جملة إعلان المستوى الأعلى هو الذي تريده. عن طريق كتابة:

mkFoo = [d| data Foo = Foo Int |]

تقوم بإنشاء قالب لصق هاسكل (مثل وظيفة وقت الترجمة) من شأنه أن يخلق إعلانًا data Foo = Foo Int فقط عن طريق إدخال الخط $(mkFoo).

على الرغم من أن هذا المثال الصغير ليس مفيدًا جدًا ، إلا أنه يمكنك تقديم حجة لـ MKFOO للتحكم في عدد الإعلانات المختلفة التي تريدها. الآن أ $(mkFoo 100) سوف تنتج 100 إعلانات بيانات جديدة لك. يمكنك أيضًا استخدام Th لإنشاء مثيلات فئة من النوع. لي التكييف الحزمة هو مشروع صغير جدًا يستخدم القالب Haskell للقيام بشيء مماثل.

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

Answer 2

هناك أيضًا بعض تقنيات البرمجة البسيطة على مستوى النوع في Haskell. يتبع مثال قانوني:

-- A family of types for the natural numbers
data Zero
data Succ n

-- A family of vectors parameterized over the naturals (using GADTs extension)
data Vector :: * -> * -> * where
    -- empty is a vector with length zero
    Empty :: Vector Zero a
    -- given a vector of length n and an a, produce a vector of length n+1
    Cons  :: a -> Vector n a -> Vector (Succ n) a

-- A type-level adder for natural numbers (using TypeFamilies extension)
type family Plus n m :: *
type instance Plus Zero n = n
type instance Plus (Succ m) n = Succ (Plus m n)

-- Typesafe concatenation of vectors:
concatV :: Vector n a -> Vector m a -> Vector (Plus n m) a
concatV Empty ys = ys
concatV (Cons x xs) ys = Cons x (concatV xs ys)

خذ لحظة لاتخاذ ذلك. أعتقد أنه من السحري إلى حد كبير أنه يعمل.

ومع ذلك ، فإن البرمجة على مستوى النوع في Haskell موجودة في الوادي الميزات-وهو ما يكفي فقط لجذب الانتباه إلى المبلغ الذي لا يمكنك فعله. اللغات المسمى بشكل يعتمد مثل agda, coq, ، و epigram خذ هذا النمط إلى الحد الأقصى والقوة الكاملة.

القالب Haskell يشبه إلى حد كبير نمط Lisp-Macro المعتاد لتوليد الكود. تكتب بعض التعليمات البرمجية لكتابة بعض التعليمات البرمجية ، ثم تقول "حسنًا ، أدخل هذا الرمز الذي تم إنشاؤه هنا". على عكس التقنية أعلاه ، يمكنك كتابة أي رمز محدد بحساب بهذه الطريقة ، لكنك لا تحصل concatV في الاعلى.

لذلك لديك بعض الخيارات لفعل ما تريد. أعتقد أن metaprogramming هي مساحة مثيرة للاهتمام حقًا ، ولا تزال في بعض النواحي صغارًا جدًا. استمتع بالاستكشاف. :-)