Idris (limbaj de programare)
| Idris | |
| Idris | |
| Extensii fișiere | .idr, .lidr |
|---|---|
| Paradigmă | Funcțională |
| Proiectat de | Edwin Brady |
| Ultima versiune | 1.3.1[1]/ 23 octombrie 2018 |
| Influențat de | Agda, Clean,[2] Coq,[3] Epigram, Haskell,[3] ML,[3] Rust[2] |
| Sistem de operare | Cross-platform |
| Licență | BSD-3 |
| Prezență online | idris-lang.org |
Modifică date / text  | |
Idris este un limbaj de programare pur funcțional, cu scop general, cu tipuri dependente, evaluare leneșă strictă sau opțională și caracteristici precum o verificare a totalității.
Chiar înainte de utilizarea posibilă a teoriei interactive, Idris se concentrează pe programarea generală, cum ar fi Haskell pur funcțional și cu performanță suficientă. Sistemul de tip Idris este similar celui folosit de Agda și teorema-dovedind în el este similar cu Coq, inclusiv tactici. În comparație, Idris are o prioritate în gestionarea ușoară a efectelor secundare și a suportului pentru implementarea limbilor specifice domeniului încorporat.
Începând cu luna mai 2017, Idris se compilează la C (bazându-se pe un colector de gunoi personalizat care folosește algoritmul lui Cheney) și JavaScript (bazată pe browser și Node.js). Există, de asemenea, un număr de generatoare de cod terțe pentru alte platforme, inclusiv Java, JVM, CIL, OCaml și un backend parțial LLVM.[4]
Numele Idris provine de la personajul dragonului cântând în programul britanic de televiziune pentru copii Ivor the Engine din anii 1970.[5]
Caracteristici
modificareIdris combină o serie de caracteristici din limbile de programare funcționale relativ importante, cu caracteristici împrumutate de la asistenții de probă.
Programare funcțională
modificareSintaxa lui Idris arată multe asemănări cu cele ale lui Haskell. Un Program Hello, world! în Idris ar putea arăta astfel:
module Main
main : IO ()
main = putStrLn "Hello, World!"
Singurele diferențe dintre acest program și echivalentul lui Haskell sunt reprezentate de colonul unic (în loc de două) în semnarea principalei funcții și omiterea cuvântului "unde" în declarația modulului.
Tipuri de date inductive și parametrice
modificareLa fel ca majoritatea limbajelor de programare funcționale moderne, Idris susține o noțiune de tip de date definit inductiv și polimorfism parametric. Astfel de tipuri pot fi definite atât în sintaxa tradițională "Haskell98"
data Tree a = Node (Tree a) (Tree a) | Leaf a
sau în sintaxa GADT mai generală:
data Tree : Type -> Type where
Node : Tree a -> Tree a -> Tree a
Leaf : a -> Tree a
Tipuri dependente
modificareCu tipuri dependente, este posibil ca valorile să apară în tipuri; în mod efectiv, orice calcul de nivel de valoare poate fi efectuat în timpul verificării tipului. Următoarele definesc un tip de liste de lungime cunoscută static, denumite în mod tradițional "vectori":
data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a
Acest tip poate fi folosit după cum urmează:
total
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil ys = ys
append (x :: xs) ys = x :: append xs ys
Funcțiile adună un vector de elemente m de tip a unui vector de n elemente de tip a. Deoarece tipurile precise de vectori de intrare depind de o valoare, este posibil să fie sigur la timpul de compilare că vectorul rezultat va avea elemente (n + m) de tip a. Cuvântul "total" invocă verificatorul totalității, care va raporta o eroare în cazul în care funcția nu acoperă toate cazurile posibile sau nu se poate dovedi (automat) că nu intră într-o buclă infinită.
Un alt exemplu comun este adăugarea pe perechi a doi vectori parametrizați pe lungimea lor:
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 înseamnă că tipul a aparține clasei de tip Num. Rețineți că această funcție continuă să fie verificată cu succes în totalitate, chiar dacă nu există niciun caz care să se potrivească cu Nil într-un vector și un număr în celălalt. Deoarece ambii vectori sunt asigurați de sistemul de tip pentru a avea exact aceeași lungime, putem fi siguri la momentul compilării că acest caz nu va avea loc. Prin urmare, nu este necesar să se menționeze pentru ca funcția să fie totală.
Caracteristici de asistență doveditoare
modificareTipurile dependente sunt suficient de puternice pentru a codifica cele mai multe proprietăți ale programelor, iar un program Idris se poate dovedi invarianți în timpul compilării. Asta face Idris să devină asistent de probă.
Există două modalități standard de a interacționa cu asistenții dovezi: prin scrierea unei serii de invocări tactice (stil Coq) sau prin elaborarea interactivă a unui termen de probă (stil Epigram/Agda). Idris sprijină ambele moduri de interacțiune, deși setul de tactici disponibile nu este încă la fel de util ca cel al Coq.
Generarea de coduri
modificareDeoarece Idris conține un asistent de probă, programele Idris pot fi scrise pentru a face dovada în jur. Dacă sunt tratați naiv, aceste dovezi rămân în jur la timpul de execuție. Idris urmărește să evite această capcană prin ștergerea agresivă a termenilor neutilizați[6], cu rezultate promițătoare[7].
Implicit, Idris generează cod nativ prin C. Sunt disponibile și alte backend-uri pentru generarea JavaScript și Java.
Note
modificare- ^ „Idris 1.3.1 released”. Arhivat din original la . Accesat în .
- ^ a b „"Uniqueness Types"”. Accesat în .
- ^ a b c „Idris, a language with dependent types”. Accesat în .
- ^ „Code Generation Targets — Idris 1.1.1 documentation”. docs.idris-lang.org.
- ^ „Frequently Asked Questions”. Accesat în .
- ^ „Erasure By Usage Analysis — Idris 1.1.1 documentation”. idris.readthedocs.org.
- ^ „Benchmark results”. ziman.functor.sk.
Legături externe
modificare- Pagina de pornire Idris, inclusiv documentație, întrebări frecvente și exemple
- Idris at the Hackage repository
- Documentation for the Idris Language (tutorial, language reference, etc.)