إدريس (لغة برمجة)

تتشابه بنية لغة إدريس إلى حد كبير مع بنية لغة هاسكل. قد يبدو برنامج "مرحباً بالعالم" في إدريس على النحو التالي:

الوحدة الرئيسيةmain : IO () main = putStrLn "Hello, World!"

الاختلافات الوحيدة بين هذا البرنامج ونظيره في لغة هاسكل هي استخدام نقطة واحدة (بدلاً من نقطتين) في توقيع نوع الدالة الرئيسية، وحذف كلمة " where" في تعريف الوحدة . ^{[ 8 ]}

يدعم إدريس أنواع البيانات المُعرَّفة استقرائيًا والتعدد الشكلي البارامتري . ويمكن تعريف هذه الأنواع باستخدام الصيغة التقليدية الشبيهة بـ Haskell 98 :

بيانات الشجرة أ = عقدة ( الشجرة أ ) ( الشجرة أ ) | ورقة أ 

أو في صيغة تشبه نوع البيانات الجبرية المعممة (GADT) الأكثر عمومية :

بيانات الشجرة : النوع -> النوع حيث العقدة : الشجرة أ -> الشجرة أ -> الشجرة أ الورقة : أ -> الشجرة أ 

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

بيانات Vect : Nat -> Type -> Type حيث Nil : Vect 0 a (::) : ( x : a ) -> ( xs : Vect n a ) -> Vect ( n + 1 ) a 

يمكن استخدام هذا النوع على النحو التالي:

الإضافة الكلية : Vect n a -> Vect m a -> Vect ( n + m ) a أضف قيمة فارغة إلى ys = ys أضف ( x :: xs ) ys = x :: أضف xs ys 

تُلحق هذه الدالة appendمتجهًا من mعناصر من نوع معين aبمتجه آخر من nعناصر من نوع آخر a. وبما أن الأنواع الدقيقة لمتجهات الإدخال تعتمد على قيمة معينة، فمن الممكن التأكد أثناء الترجمة من أن المتجه الناتج سيحتوي بالضبط على ( n+ m) عنصرًا من النوع . تستدعي aالكلمة " " مدقق الشمولية الذي سيُبلغ عن خطأ إذا لم تُغطِّ الدالة جميع الحالات الممكنة أو إذا تعذَّر إثبات (تلقائيًا) أنها لا تدخل في حلقة لا نهائية .total

ومن الأمثلة الشائعة الأخرى الجمع الزوجي لمتجهين يتم تحديدهما بناءً على طولهما:

إجمالي إضافة الأزواج : العدد أ => المتجه ن أ -> المتجه ن أ -> المتجه ن أ pairAdd Nil Nil = Nil pairAdd ( x :: xs ) ( y :: ys ) = x + y :: pairAdd xs ys 

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

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

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

بما أن إدريس يحتوي على مساعد للبرهان، يمكن كتابة برامج إدريس لتمرير البراهين. إذا تم التعامل مع هذه البراهين ببساطة، فإنها تبقى موجودة أثناء التشغيل. يهدف إدريس إلى تجنب هذا المأزق عن طريق حذف المصطلحات غير المستخدمة بشكل جذري. ^{[ 9 ] [ 10 ]}

بشكل افتراضي، يقوم إدريس بإنشاء كود أصلي من خلال لغة C. أما الواجهة الخلفية الأخرى المدعومة رسميًا فتقوم بإنشاء كود جافا سكريبت .