ادریس (زبان برنامه‌نویسی)

ادریس

پارادایم برنامه‌نویسی	تابعی
طراحی شده توسط	ادوین بردی
ظهوریافته در	۲۰۰۷ (۲۰۰۷-}})
انتشار پایدار	1.3.3 / ۲۴ مه ۲۰۲۰ (۲۰۲۰-24}})
انتشار آزمایشی	۰٫۵٫۱ (ادریس ۲) / ۲۰ سپتامبر ۲۰۲۱ (۲۰۲۱-20}})
سیستم‌عامل	چندسکویی
پروانه	بی‌اس‌دی
پسوند(های) نام پرونده	.idr, .lidr
وبگاه	idris-lang.org
متأثر از
Agda, Clean, Coq, Epigram, F#, Haskell, ML, Rust

ادریس (به انگلیسی: Idris) یک زبان برنامه‌نویسی کاملاً کاربردی با نوع‌های وابسته، ارزیابی کندرو اختیاری و ویژگی‌هایی مانند بررسی کل است. ادریس ممکن است به عنوان یک دستیار اثبات استفاده شود، اما به گونه ای طراحی شده‌است که یک زبان برنامه‌نویسی همه‌منظوره مشابه زبان هسکل باشد.

سیستم نوع زبان ادریس، شبیه به آگدا است، و اثبات‌ها شبیه به زبان برنامه‌نویسی Coq می‌باشند، از جمله تاکتیک‌هایی (توابع/رویه‌های اثبات قضیه) که از طریق بازتابنده‌های با جزییات صورت می‌پذیرند. در مقایسه با زبان‌های Agda و Coq، ادریس مدیریت عوارض جانبی و پشتیبانی از زبان‌های اختصاصی دامنه را در اولویت قرار می‌دهد. ادریس به زبان‌های سی(C) (با تکیه بر یک جمع‌آوری زباله کپی سفارشی با استفاده از الگوریتم چنی) و جاوااسکریپت (هم مبتنی بر مرورگر و هم مبتنی بر Node.js) کامپایل می‌شود. تولیدکنندگان کد شخص ثالث برای پلتفرم‌های دیگر، از جمله ماشین مجازی جاوا، زبان میانی مشترک، و ال‌ال‌وی‌ام نیز وجود دارند.

نام ادریس برگرفته از اسم یک اژدهای آوازخوان از برنامه تلویزیونی کودکان بریتانیا در دهه ۱۹۷۰ به نام Ivor the Engine است.

ویژگی‌ها

ادریس تعدادی از ویژگی‌های زبان‌های برنامه‌نویسی عملکردی نسبتاً رایج را با ویژگی‌هایی برگرفته شده از دستیارهای اثبات ترکیب می‌کند.

برنامه‌نویسی تابعی

نحو در زبان ادریس، شباهت‌های زیادی با نحو زبان هسکل دارد. یک برنامه «سلام، دنیا!» در ادریس ممکن است به شکل زیر باشد:

module Main

main : IO ()
main = putStrLn "Hello, World!"

تنها تفاوت بین این برنامه و معادل هسکل آن، علامت تک (به جای دوتایی) دو نقطه در امضای نوع تابع اصلی و حذف کلمه " where " در اعلان ماژول می‌باشد.

نوع داده‌های استقرایی و پارامتری

زبان ادریس از انواع داده‌های تعریف شده به صورت استقرایی وچندشکلی پارامتریک پشتیبانی می‌کند. چنین انواع داده‌ای را می‌توان هر دو در نحو مانند Haskell98 تعریف کرد:

data Tree a = Node (Tree a) (Tree a) | Leaf a

یا در نحوی جامع تر مانند GADT:

data Tree : Type -> Type where
  Node : Tree a -> Tree a -> Tree a
  Leaf : a -> Tree a

نوع‌های وابسته

با نوع‌های وابسته، امکان دارد مقادیر در انواع ظاهر شوند. در عمل، می‌توان

بررسی نوع انجام داد. موارد زیر نوعی لیست را تعریف می‌کند که طول آنها قبل از اجرای برنامه مشخص است که به‌طور سنتی بردار نامیده می‌شوند:

data Vect : Nat -> Type -> Type where
 Nil : Vect 0 a
 (::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a

این نوع، می‌تواند به صورت زیر استفاده شود:

total
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil    ys = ys
append (x :: xs) ys = x :: append xs ys

تابع append برداری متشکل از m عنصر از نوع a را، به برداری دارای n عنصر از نوع a, می‌افزاید. از آنجایی که نوع دقیق بردارهای ورودی، وابسته به یک مقدار مشخص است، می‌توان اطمینان حاصل نمود که در زمان کامپایل، بردار حاصل دقیقاً دارای m+n مولفه از نوع a است. کلمه "total"، بررسی کننده کلیت را فرا خوانی می‌کند. بررسی کننده کلیت، در صورتی که تابع، تمامی حالت‌های ممکن را پشتیبانی نکند یا نتوان (به‌طور خودکار) نشان داد که تابع وارد یک حلقه بی‌نهایت می‌شود، خطا را گزارش می‌کند. یک مثال بارز دیگر، جمع دو بردار است که طبق طولشان، پارامتری شده‌اند:

total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil    Nil    = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys

"Num a"، نشان دهنده این است که نوع a، متعلق به کلاس از نوع Num است. توجه داشته باشید که این تابع، حتی اگر هیچ موردی مطابق با حالتی که Nil در یک بردار و یک عدد، در بردار دیگر داشته باشیم، باز هم بررسی‌های نوع را با موفقیت انجام می‌دهد. از آنجایی که سیستم نوع می‌تواند ثابت کند که بردارها دارای طول یکسان هستند، پس می‌توانیم اطمینان داشته باشیم که در زمان کامپایل، چنین حالتی هرگز پیش نمی‌آید و نیازی نیست که این حالت را در تعریف تابع، لحاظ کنیم.

ویژگی‌های دستیار اثبات

نوع‌های وابسته، این قابلیت را دارند تا بیشتر ویژگی‌های برنامه را رمزگذاری کنند. همچنین یک برنامه ادریس وجود ثابت‌ها در زمان کامپایل را نشان دهد. این ویژگی زبان ادریس، آن را به یک دستیار اثبات تبدیل می‌کند.

دو راه استاندارد برای تعامل با دستیارهای اثبات وجود دارد: می‌توان یک سری تاکتیک‌های فراخوانی برایشان نوشت (مشابه با رویکرد زبان Coq)، یا می‌توان با ساخت یک عبارت اثباتی به صورت تعاملی (مشابه با رویکرد زبان Agda)، این کار را انجام داد. زبان ادریس، از هر دو روش پشتیبانی می‌کند، هرچند مجموعه تاکتیک‌های موجود، هنوز به اندازه Coq، کارآمد نیستند.

تولید کد

از آنجایی که ادریس، شامل یک دستیار اثبات است، برنامه‌های ادریس می‌توانند برای انتقال ثبات‌های مختلف به سیستم‌های مختلف استفاده شوند. اگر از این قابلیت به درستی استفاده نشود، این اثبات‌ها هنگام اجرای برنامه کنار هم باقی می‌مانند و مشکلاتی ایجاد می‌کنند. ادریس سعی می‌کند با حذف عبارت‌های استفاده نشده، از بروز این مشکل، جلوگیری کند.

به صورت پیش فرض، ادریس کد طبیعی را با استفاده از سی تولید می‌کند. سایر بکندهای پشتیبانی شده، این کار را با استفاده از جاوا اسکریپت انجام می‌دهند.

ادریس ۲

ادریس ۲ یک نسخه جدید خود میزبان از زبان ادریس است که سیستم نوع خطی را به‌طور کامل، و بر اساس «نظریه نوع کمی»، ادغام می‌کند. این زبان در حال حاضر، به زبان‌های سی(C) و اسکیما (Scheme)،کامپایل می‌شود.

جستارهای وابسته

• برنامه‌نویسی عملکردی کل

منابع

1. Brady, Edwin (۱۲ دسامبر ۲۰۰۷). "Index of /~eb/darcs/Idris". University of St Andrews School of Computer Science. Archived from the original on 2008-03-20.

پیوند به بیرون

• صفحهٔ اصلی ادریس، شامل مستندات، سوالات متداول و مثال‌ها
• ادریس در Hackage repository
• اسناد زبان ادریس (آموزش، مرجع زبان و غیره.)