ادریس (زبان برنامه‌نویسی)
| پارادایم برنامه‌نویسی | تابعی |
|---|---|
| طراحی شده توسط | ادوین بردی |
| ظهوریافته در | ۲۰۰۷[۱] |
| انتشار پایدار | 1.3.3[۲]
۲۴ مه ۲۰۲۰ |
| انتشار آزمایشی | ۰٫۵٫۱ (ادریس ۲)[۳]
۲۰ سپتامبر ۲۰۲۱ |
| سیستم‌عامل | چندسکویی |
| پروانه | بی‌اس‌دی |
.idr, .lidr | |
| وبگاه | |
| متأثر از | |
| 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)،کامپایل می‌شود.
جستارهای وابسته[ویرایش]
- برنامه‌نویسی عملکردی کل
منابع[ویرایش]
- ↑ Brady, Edwin (12 دسامبر 2007). "Index of /~eb/darcs/Idris". University of St Andrews School of Computer Science. Archived from the original on 2008-03-20.
- ↑ "Release 1.3.3". Retrieved 2020-05-25.
- ↑ "Idris 2 version 0.5.1 Released". www.idris-lang.org. Retrieved 2021-10-16.
- ↑ ۴٫۰ ۴٫۱ "Uniqueness Types". Idris 1.3.1 Documentation. Retrieved 2019-09-26.
- ↑ ۵٫۰ ۵٫۱ ۵٫۲ "Idris, a language with dependent types". Retrieved 2014-10-26.
- ↑ "Elaborator Reflection — Idris 1.3.2 documentation". Retrieved 27 April 2020.
- ↑ "Code Generation Targets — Idris 1.1.1 documentation". docs.idris-lang.org.
- ↑ "Frequently Asked Questions". Retrieved 2015-07-19.
- ↑ "Syntax Guide — Idris 1.3.2 documentation". Retrieved 27 April 2020.
- 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
- اسناد زبان ادریس (آموزش، مرجع زبان و غیره.)
