لغة البرمجة Idris هي لغة برمجة وظيفية نقية متعددة الأغراض تتميز بنوعية متعلقة بالتبعية، ويمكن تقييمها بأنها توفر عمليات التقييم الصارمة أو الكسولة الاختيارية، بالإضافة إلى ميزات مثل فحص الاكتمال. تميل Idris إلى التركيز على البرمجة متعددة الأغراض، مشابهة للغة Haskell الوظيفية بشكل كامل، وتحقق أداء كافٍ. يشبه نظام الأنواع في Idris تلك المستخدمة في Agda، ويمكن التعامل معه فيه بطريقة تشبه Coq، بما في ذلك التكتيكات. تتميز Idris عن غيرها بالتركيز على إدارة الآثار الجانبية بسهولة ودعم تنفيذ لغات تخصصية مضمنة.
تترجم Idris في الوقت الحالي إلى لغة C (مع الاعتماد على جامع المخلفات المخصص واستخدام خوارزمية Cheney) وJavaScript (سواء في المتصفح أو مع Node.js). بالإضافة إلى ذلك، هناك عدد من مولدات الكود الخارجية لمنصات أخرى، بما في ذلك Java، JVM، CIL، OCaml، ونظام معالجة اللغات المخفف LLVM.
تعود أصول اسم Idris إلى شخصية التنين المغني في برنامج الأطفال البريطاني Ivor the Engine في السبعينات.
تُعتبر Idris مفتوحة المصدر ومبنية على المجتمع، حيث بدأت في جامعة سانت أندروز. يمكن العثور على مزيد من المعلومات حولها على موقعها الرسمي (idris-lang.org) وصفحتها على ويكيبيديا (رابط ويكيبيديا)، حيث توفر هذه المصادر نظرة عامة وتفاصيل تقنية حول اللغة واستخداماتها المحتملة.