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

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

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

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

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
• اسناد زبان ادریس (آموزش، مرجع زبان و غیره.)