Idris (llenguatge de programació)
| Tipus | llenguatge de programació purament funcional, llenguatge de programació, dependently typed programming language (en)  i proof assistant (en)  |
|---|---|
| Data de creació | 2007 |
| Paradigma de programació | programació funcional, purely functional programming (en) i total functional programming (en) |
| Darrera versió estable | 1.3.3 () |
| Llenguatge de programació | Haskell |
| Influenciat per | Haskell, Agda, Coq, Clean i Epigram |
| Extensió dels fitxers | idr i lidr |
| Codi font | Codi font |
| Llicència | llicència BSD |
| Pàgina web | idris-lang.org |
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.[1][2] 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).[3]
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,[4] Agda[5] o bé Isabelle.[6]
Programa Hola món
[modifica]module Main main : IO () main = putStrLn "Hello, World!" El compilador està fet en Haskell. Cal tenir-ne instal·lat el compilador GHC i descarregar-lo del rebost Hackage[7] (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
[modifica]Per una informació actualitzada, consulteu la documentació en forma de guia.[8][9]
Avaluació estricta per defecte
[modifica]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:
data Lazy : Type -> Type where Delay : (val : a) -> Lazy a Force : Lazy a -> a -- la següent funció retorna automàticament el resultat de l'avaluació del paràmetre que s'ofereixi com a resultat. boolCase : Bool -> Lazy a -> Lazy a -> a; boolCase True t e = t; boolCase False t e = e; El tipus _|_
[modifica]El tipus _|_ (anomenat tipus buit) és un tipus que no té cap constructor. No té valors.
Serveix per provar que una proposta és impossible.
- 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.[10] 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)
interface Functor (f : Type -> Type) where map : (m : a -> b) -> f a -> f b - notació dels Functors Aplicatius
[| f a1 … an |] ≡ pure f <*> a1 <*> … <*> an - 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)
codata Stream : Type -> Type where (::) : (element : a) -> Stream a -> Stream a - No hi ha derivació automàtica d'implementacions com al Haskell, ara per ara.
Exemples
[modifica]Efectes simples - Encapsulament d'actualitzacions destructives
[modifica]- 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.
module Main import Effects import Effect.StdIO import Effect.State provaEstats : Eff Int ['RefA ::: STATE Int, 'RefB ::: STATE Int] -- efectes etiquetats provaEstats = do x <- 'RefA :- get y <- 'RefB :- get let z = x * 2 + y 'RefB :- put z z' <- 'RefB :- get return z' calculEncapsulat : Int -> Int calculEncapsulat x = runPureInit ['RefA := x, 'RefB := 5] provaEstats efecteConsola : Eff () [STDIO] efecteConsola = do let y = calculEncapsulat 2 putStrLn (show y) main : IO () main = run efecteConsola idris -p effects -o prova prova.idr ./prova Excepcions
[modifica]La mònada (IOExcept excep resultat) ofereix un tractament d'excepcions sense baixar al nivell baix de l'efecte [EXCEPTION excep].
import Control.IOExcept import Control.Catchable data MyErr = Excep1 -- cal instanciar-ne la classe Show per poder tractar una excepció. implementation Show MyErr where show Excep1 = "Excep1" accioAmbExcepcions : IOExcept MyErr String accioAmbExcepcions = throw Excep1 gestor : MyErr -> IOExcept MyErr String gestor err = pure $ show err cassador : IOExcept MyErr String cassador = catch accioAmbExcepcions gestor main : IO () main = do r <- runIOExcept cassador case r of Left err => putStrLn $ "no caçada: " ++ show err ++ "!" Right str => putStrLn $ "caçada: " ++ str Funcions parcials amb precondició certificada. El tipus Tal_que
[modifica]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.
module Main -- DynamicSafeDiv.idr {- Del mòdul Prelude.Bool data So : Bool -> Type where Oh : So True instance Uninhabited (So False) where uninhabited Oh impossible -- Del mòdul Prelude.Either choose : (b : Bool) -> Either (So b) (So (not b)) -} noZero : (Eq a, Num a) => a -> Bool noZero x = x /= 0 -- divisió segura: l'expressió del Tal_que sobre paràmetres formals -- ha de coincidir amb l'expressió del "choose" sobre paràmetres actuals divisioSeguraPer : (Eq a, Num a, Integral a) => (denom : a) -- etiqueta i tipus del denominador -> a -- tipus del numerador -> So (noZero denom) -- Tal_que: prova de la precondició sobre paràmetres formals -> a -- tipus del resultat divisioSeguraPer dn x p = x `div` dn readInt : String -> Int readInt str = cast str dynamicTest : IO () dynamicTest = do putStr "entreu el denominador de la divisió: " str <- getLine let denom = readInt str -- comprova amb "choose" la precondició sobre els paràmetres actuals de la crida case choose (noZero denom) of Right _ => putStrLn "el denominador no pot ser zero!!" -- precondició fallida Left provaDeLaPrecondició => do -- precondició provada let res = divisioSeguraPer denom 5 provaDeLaPrecondició putStrLn $ "el resultat és: " ++ show res main : IO () main = dynamicTest Compilació i execució al Linux:
idris -o dynsafediv DynamicSafeDiv.idr ./dynsafediv Un tipus com a proposició
[modifica]Del codi de Data.List una prova inductiva de la comprovació de pertinença a una llista:
module Data.List %access public ||| Tipus com a prova. ||| El tipus (Elem z zs) és una prova que `z` és element de `zs` ||| sempre que es doni algun dels casos que es descriuen: using (x: a, y: a, xs: List a) -- tipus de les variables del bloc data Elem : a -> List a -> Type where -- El Tipus Elem és un tipus probatori de la pertinença a llista: Here : Elem x (x :: xs) -- o bé (cas bàsic) x coincideix amb el cap (variable coincident) There : Elem x xs -> Elem x (y :: xs) -- o bé (cas inductiu) cal aportar la prova (com a paràmetre) que x pertanyi a la cua -- Cas de llista buida: el tipus (Elem x []) està deshabitat (no té valors), -- provant que és impossible que cap elem. x pertanyi a la llista buida. instance Uninhabited (Elem {a} x []) where uninhabited Here impossible -- és impossible que coincideixi amb el cap uninhabited (There p) impossible -- és impossible que pertanyi a la cua ||| Is the given element a member of the given list. ||| ||| @x The element to be tested. ||| @xs The list to be checked against isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs) isElem x [] = No absurd isElem x (y :: xs) with (decEq x y) -- ''with '' afegeix una expressió a encaixar després de '|' -- a les definicions subseqüents isElem x (x :: xs) | (Yes refl) = Yes Here isElem x (y :: xs) | (No contra) with (isElem x xs) isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf) isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f) where mkNo : {xs' : List a} -> ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) -> Elem x' (y' :: xs') -> _|_ mkNo f g Here = f refl mkNo f g (There x) = g x Referències
[modifica]- ↑ 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
[modifica]- Pàgina inicial de l'Idris: www.idris-lang.org
- Biblioteques en Idris: Biblioteques
