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.Pàgina inicial de l'IdrisEdwin 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).Language features Característiques del llenguatge
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,Inria - The Coq Proof Assistant AgdaUniv. de Chalmers - Agda o bé Isabelle.Univ. de Cambridge - Isabelle generic proof assistant
Programa Hola món 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 Hackagepaquet Idris al 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 .
Característiques Per una informació actualitzada, consulteu la documentació en forma de guia.The Idris TutorialReference - syntax guide
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:
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 _|_ 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.Named implementations 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 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.
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 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 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ó 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
Enllaços externs Pàgina inicial de l'Idris: www.idris-lang.org Biblioteques en Idris: Biblioteques
Categoria:Llenguatges de programació funcional Categoria:Llenguatge de programació Haskell