Idris (llenguatge de programació)

De Viquipèdia
Jump to navigation Jump to search
Infotaula de llenguatge de programacióIdris
Tipus purely functional programming language i llenguatge de programació
Data de creació 2009
Llenguatge de programació Haskell
Influenciat per Haskell
Extensió dels fitxers idr i lidr
Pàgina web Web oficial
Modifica dades a Wikidata

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 de proves (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.

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, s'en 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.

Diferències amb el Haskell[modifica]

  • 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
  • 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 - Càlculs encapsulats[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
                 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]

Enllaços externs[modifica]