| Idris | |
|---|---|
| Clasa de limba | Funcţional |
| Aparut in | 2007 [3] [4] [5] |
| Autor | Edwin Brady |
| Extensie de fișier | .idrsau.lidr |
| Eliberare | Idris 2 versiunea 0.5.1 [1] (20 septembrie 2021 ) |
| Tip sistem | suport de tip strict , static , dependent |
| A fost influențat | Agda , Coq , [2] Epigram , Haskell , [2] ML , [2] Rust |
| Licență | BSD-3 |
| Site-ul web | idris-lang.org |
Idris este un limbaj de programare pur , total funcțional , de uz general, cu o sintaxă asemănătoare Haskell și suport pentru tipuri dependente [6] . Sistemul de tip este similar cu sistemul de tip Agda .
Limbajul acceptă teste automate comparabile cu Coq , inclusiv suport pentru tactici, dar nu se concentrează asupra lor, ci este poziționat ca un limbaj de programare de uz general . Obiectivele creării sale: performanță „suficientă”, ușurință în gestionarea efectelor secundare și mijloace de implementare a limbajelor încorporabile specifice domeniului .
Implementat în Haskell , disponibil ca pachet Hackage [7] . Codul sursă Idris este compilat într-un set de reprezentări intermediare [8] , iar din acestea în cod C , care este executat folosind un colector de gunoi de copiere folosind algoritmul Cheney . De asemenea, implementată oficial este și capacitatea de a compila în cod JavaScript (inclusiv pentru Node.js ). Există implementări terțe ale generatoarelor de cod pentru Java , JVM , CIL , Erlang , PHP și (limitat) LLVM .
Limba este numită după dragonul cântăreț Idris din emisiunea TV britanică pentru copii din 1970 Ivor the Tank Engine [9] .
Limbajul combină caracteristicile principalelor limbaje de programare funcționale populare cu caracteristici împrumutate de la sistemele automate de dovezi, estompând efectiv linia dintre cele două clase de limbaje.
A doua versiune a limbajului (lansată în 2020, bazată pe „teoria tipului cantitativ” [10] ) diferă semnificativ de prima: a fost adăugat suport complet pentru tipurile liniare , codul este compilat implicit în Scheme , compilatorul de limbaj este scris în limbajul propriu-zis .
Sintaxa limbii (ca și cea a lui Agda ) este apropiată de cea a lui Haskell [11] . Salut , lume! pe Idris arată așa:
modul principal main : IO () main = putStrLn „Bună, lume!”Diferențele dintre acest program și echivalentul său Haskell sunt două puncte simple (în loc de duble) în semnătura funcției principale și absența cuvântului „unde” în declarația modulului.
La fel ca majoritatea limbajelor de programare funcționale moderne, limbajul acceptă tipuri de date recursive (definite prin inducție) și polimorfismul parametric . Astfel de tipuri pot fi definite ca în sintaxa tradițională „Haskell98”:
Arborele de date a = Nodul ( Arborele a ) ( Arborele a ) | frunză ași în sintaxa GADT mai generală :
date Arborele : Tip -> Tip unde Nod : Arborele a -> Arborele a -> Arborele a Frunză : a -> Arborele aPrin intermediul tipurilor dependente , este posibilă, în etapa verificării tipului, efectuarea de calcule care implică valorile care parametriză tipurile. Următorul cod definește o listă cu o lungime dată static, numită în mod tradițional vector :
date Vect : Nat -> Type -> Type unde Nil : Vect 0 a (::) : ( x : a ) -> ( xs : Vect na ) -> Vect ( n + 1 ) aAcest tip poate fi folosit astfel:
total append : Vect na -> Vect ma -> Vect ( n + m ) a anexează Nil ys = ys anexează ( x :: xs ) ys = x :: anexează xs ysFuncția adaugă un vector de melemente de tip ala un vector de nelemente de tip a. Deoarece tipul exact al vectorilor de intrare depinde de valorile care sunt cu siguranță cunoscute la momentul compilării, vectorul rezultat va conține exact (n + m)elemente de tipul a.
Cuvântul " total" invocă o verificare a completității analizei față de , care, pentru a evita intrarea într-o buclă infinită , va raporta o eroare dacă funcția nu acoperă toate cazurile posibile de , sau nu poate fi dovedită (automat).
Un alt exemplu: adăugarea în perechi a doi vectori parametrizați după lungimea lor:
total pairAdd : Num a => Vect na -> Vect na -> Vect na pairAdd Nil Nil = Nil pairAdd ( x :: xs ) ( y :: ys ) = x + y :: pairAdd xs ysNumînseamnă că tipul aaparține clasei de tip Num . Funcția trece cu succes verificarea de tip, cazul în care unul dintre vectori va avea valoarea Nil, în timp ce al doilea va fi un număr, nu se poate întâmpla. Sistemul de tip verifică în timpul compilării dacă lungimea ambilor vectori se va potrivi. Acest lucru simplifică textul funcției, care nu mai este necesar pentru a gestiona acest caz special.
Tipurile dependente sunt suficient de puternice pentru a descrie majoritatea proprietăților programelor, astfel încât un program Idris poate dovedi invarianți în timpul compilării. Acest lucru transformă limba într-un sistem de dovezi interactiv .
Idris suportă două moduri de lucru cu sistemul de demonstrare automată: prin scrierea de apeluri succesive la tactici ( stilul Coq , în timp ce setul de tactici disponibile nu este la fel de bogat ca în Coq, dar poate fi extins cu instrumente standard de metaprogramare ) sau pas cu pas -dezvoltare dovada pas ( stil Epigram si Agda ).