Idris (limbaj de programare)

Idris
Idris
Extensii fișiere	.idr, .lidr
Paradigmă	Funcțională
Proiectat de	Edwin Brady
Ultima versiune	1.3.1[1]/ octombrie 23, 2018; acum 6 ani, 1 lună și 9 zile (2018-10-23)
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

Idris 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ă

Sintaxa 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

La 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

Cu 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

Tipurile 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

Deoarece 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

1. „Idris 1.3.1 released”. Arhivat din original la 23 octombrie 2018. Accesat în 23 octombrie 2018. 
2. ^ „"Uniqueness Types"”. Accesat în 20 noiembrie 2018. 
3. ^ „Idris, a language with dependent types”. Accesat în 26 octombrie 2014. 
4. „Code Generation Targets — Idris 1.1.1 documentation”. docs.idris-lang.org. 
5. „Frequently Asked Questions”. Accesat în 19 iulie 2015. 
6. „Erasure By Usage Analysis — Idris 1.1.1 documentation”. idris.readthedocs.org. 
7. „Benchmark results”. ziman.functor.sk. 

Legături externe

• 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.)