Idris (llenguatge de programació)

Idris

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

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

Per una informació actualitzada, consulteu la documentació en forma de guia.^[8][9]

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.^[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

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

1. Pàgina inicial de l'Idris
2. Edwin Brady
3. Language features(anglès) Característiques del llenguatge
4. Inria - The Coq Proof Assistant(anglès)
5. Univ. de Chalmers - Agda(anglès)
6. Univ. de Cambridge - Isabelle generic proof assistant(anglès)
7. paquet Idris al Hackage
8. The Idris Tutorial(anglès)
9. Reference - syntax guide(anglès)
10. Named implementations(anglès)

Enllaços externs

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