# Idris (llenguatge de programació)

Idris és un llenguatge de programació funcional amb tipus dependents de valors, desenvolupat a la Universitat escocesa de Saint Andrews sota la direcció d'Edwin Brady. per a aplicacions de propòsit general amb la possibilitat de verificació estàtica incorporada.
El sistema de tipus és similar al del llenguatge Agda, amb una sintaxi molt semblant al Haskell però amb semàntica estricta (avaluació primerenca), designant l'avaluació tardana als tipus (tipus Lazy a).
Els tipus hi són objectes de primer ordre, permetent barrejar objectes i tipus als paràmetres i resultats.
Aquest llenguatge permet incorporar tipus com a proposicions i funcions com a proves, per certificar les propietats de la funcionalitat aportada, seguint la teoria de la Correspondència Curry-Howard entre programes i proves, incorporant propietats dels sistemes d'ajuda a la comprovació (Proof assistants) també anomenats comprovadors de Teoremes com ara Coq, Agda o bé Isabelle.

## Programa Hola món

El compilador està fet en Haskell. Cal tenir-ne instal·lat el compilador GHC i descarregar-lo del rebost Hackage (cabal install idris). Funciona tant com a compilador, com a intèrpret (avaluador d'expressions) si no s'especifica el fitxer per compilar.
Avaluador en línia a tryidris.org Arxivat 2014-07-15 a Wayback Machine..

## Característiques

Per una informació actualitzada, consulteu la documentació en forma de guia.

### Avaluació estricta per defecte

L'avaluació tardana s'obté amb el tipus (Lazy a) i si s'especifica el tipus del resultat igual al tipus del paràmetre del Lazy, se'n força l'avaluació de manera automàtica:

### El tipus _|_

El tipus _|_ (anomenat tipus buit) és un tipus que no té cap constructor. No té valors.
Serveix per provar que una proposta és impossible.

### Diferències amb el Haskell

* Idris parteix d'una sintaxi similar al Haskell però amb avaluació estricta, precisant l'avaluació tardana al tipus amb el constructor de tipus Lazy
* Els identificadors no admeten caràcters Unicode si no que queden restringits a l'alfabet anglès pertanyent al conjunt ASCII.
* Els operadors (::) i (:) intercanvien el significat. En un selector case, (=>) separa patrons i expressions.
* Els paràmetres formals de les funcions es poden etiquetar
* S'ha canviat el nom de
   * les signatures, abans classes com al Haskell, ara cal dir-ne interface
   * les implementacions, abans instance com al Haskell, ara són implementation
* Idris admet múltiples implementacions d'un mateix interface distingides per un nom. El Haskell requeria fer-ne tipus derivats amb newtype per cada implementació addicional.
* les variables índexs dels interface incorporen informació de kind (tipus del tipus)
* notació dels Functors Aplicatius
* Als blocs do (sintaxi dels blocs monàdics)
   * en context d'expressions, el prefix '!' a una variable o bé expressió, l'avalua com a efecte, imitant la sintaxi del ML Estàndard
   * return està desaconsellat en favor de pure
* Les estructures infinites es defineixen amb la clàusula codata, convertint el tipus T als components en (Inf T) que s'avalua de manera tardana (Lazy)
* No hi ha derivació automàtica d'implementacions com al Haskell, ara per ara.

## Exemples
### Efectes simples - Encapsulament d'actualitzacions destructives

* Per diferenciar els efectes hi ha etiquetes (noms en majúscula precedits per l'apòstrof).
* runPure es fa servir com runST del Haskell; runPureInit permet inicialitzar els efectes.

### Excepcions

La mònada (IOExcept excep resultat) ofereix un tractament d'excepcions sense baixar al nivell baix de l'efecte [EXCEPTION excep].

### Funcions parcials amb precondició certificada. El tipus Tal_que

Es tracta d'incorporar una certificació estàtica (en temps de compilació) que s'ha fet una comprovació dinàmica de la precondició.
El tipus (So expr_booleana) traduïble per (Tal_que precondició) permet especificar relacions o restriccions de valor entre els paràmetres formals prèviament etiquetats.
Per certificar la prova dinàmica, cal que la rutina que fa la crida, avaluï amb la funció choose la mateixa precondició sobre els paràmetres actuals, oferint el resultat probatori en la variant Left que caldrà adjuntar com a paràmetre (el de tipus So Bool) a la crida.
Compilació i execució al Linux:

### Un tipus com a proposició

Del codi de Data.List una prova inductiva de la comprovació de pertinença a una llista:

## Referències

* ↑ Pàgina inicial de l'Idris
* ↑ Edwin Brady
* ↑ Language features(anglès) Característiques del llenguatge
* ↑ Inria - The Coq Proof Assistant(anglès)
* ↑ Univ. de Chalmers - Agda(anglès)
* ↑ Univ. de Cambridge - Isabelle generic proof assistant(anglès)
* ↑ paquet Idris al Hackage
* ↑ The Idris Tutorial(anglès)
* ↑ Reference - syntax guide(anglès)
* ↑ Named implementations(anglès)

## Enllaços externs

* Pàgina inicial de l'Idris: www.idris-lang.org
* Biblioteques en Idris: Biblioteques