| Idris | |
|---|---|
| Sprog klasse | Funktionel |
| Dukkede op i | 2007 [3] [4] [5] |
| Forfatter | Edwin Brady |
| Filtypenavn _ | .idreller.lidr |
| Frigøre | Idris 2 version 0.5.1 [1] (20. september 2021 ) |
| Type system | streng , statisk , afhængig type support |
| Blev påvirket | Agda , Coq , [2] Epigram , Haskell , [2] ML , [2] Rust |
| Licens | BSD-3 |
| Internet side | idris-lang.org |
Idris er et rent , totalt funktionelt programmeringssprog til generelle formål med en Haskell - lignende syntaks og understøttelse af afhængige typer [6] . Typesystemet ligner Agda -systemet .
Sproget understøtter automatiske korrekturer , der kan sammenlignes med Coq , herunder understøttelse af taktik, men fokuserer ikke på dem, men er placeret som et programmeringssprog til generelle formål . Målene for dets oprettelse: "tilstrækkelig" ydeevne, nem håndtering af bivirkninger og midler til implementering af indlejrbare domænespecifikke sprog .
Implementeret i Haskell , tilgængelig som en Hackage- pakke [7] . Idris kildekode er kompileret til et sæt mellemrepræsentationer [8] og fra dem til C -kode, som udføres ved hjælp af en kopigarbage collector ved hjælp af Cheney-algoritmen . Også officielt implementeret er muligheden for at kompilere til JavaScript -kode (inklusive for Node.js ). Der er tredjepartsimplementeringer af kodegeneratorer til Java , JVM , CIL , Erlang , PHP og (begrænset) LLVM .
Sproget er opkaldt efter den syngende drage Idris fra det britiske børne-tv-show Ivor the Tank Engine fra 1970 [9] .
Sproget kombinerer funktioner fra de store populære funktionelle programmeringssprog med funktioner lånt fra automatiske korrektursystemer, hvilket effektivt udvisker grænsen mellem de to sprogklasser.
Den anden version af sproget (udgivet i 2020, baseret på "kvantitativ typeteori" [10] ) adskiller sig væsentligt fra den første: fuld understøttelse af lineære typer er blevet tilføjet , koden er kompileret som standard i Scheme , sprogkompileren er skrevet på selve sproget .
Sprogets syntaks (som Agda ) er tæt på Haskells [11] . Hej verden! på Idris ser sådan ud:
modul Hoved main : IO () main = putStrLn "Hej, verden!"Forskellene mellem dette program og dets Haskell-ækvivalent er det enkelte (i stedet for dobbelt) kolon i hovedfunktionssignaturen og fraværet af ordet "hvor" i modulerklæringen.
Som de fleste moderne funktionelle programmeringssprog understøtter sproget rekursive (defineret ved induktion) datatyper og parametrisk polymorfi . Sådanne typer kan defineres som i den traditionelle "Haskell98"-syntaks:
data Træ a = Node ( Træ a ) ( Træ a ) | blad aog i den mere generelle GADT- syntaks:
data Træ : Type -> Type hvor Node : Træ a -> Træ a -> Træ et blad : a -> Træ aVed hjælp af afhængige typer er det muligt på stadiet af typekontrol at udføre beregninger, der involverer de værdier, der parametrerer typerne. Følgende kode definerer en liste med en statisk given længde, traditionelt kaldet en vektor :
data Vect : Nat -> Type -> Type where Nil : Vect 0 a (::) : ( x : a ) -> ( xs : Vect na ) -> Vect ( n + 1 ) aDenne type kan bruges sådan:
total tilføjelse : Vect na -> Vect ma -> Vect ( n + m ) a tilføje Nil ys = ys tilføj ( x :: xs ) ys = x :: tilføj xs ysFunktionen tilføjer en vektor af mtypeelementer atil en vektor af ntypeelementer a. Fordi den nøjagtige type af inputvektorerne afhænger af værdier, der er bestemt kendt på kompileringstidspunktet, vil den resulterende vektor indeholde nøjagtigt (n + m)elementer af typen a.
Ordet " total" påberåber sig et parse-fuldstændighedstjek mod , som for at undgå at gå ind i en uendelig løkke vil rapportere en fejl, hvis funktionen ikke dækker alle mulige tilfælde af , eller ikke kan (automatisk) bevises.
Et andet eksempel: parvis tilføjelse af to vektorer parametriseret af deres længde:
totalt parTilføj : Antal a => Vect na -> Vect na -> Vect na parAdd Nul Nul = Nul parAdd ( x :: xs ) ( y :: ys ) = x + y :: parAdd xs ysNumbetyder, at typen atilhører typeklassen Num . Funktionen passerer med succes typekontrollen, det tilfælde, hvor en af vektorerne vil have værdien nul, mens den anden vil være et tal, kan ikke ske. Typesystemet kontrollerer på kompileringstidspunktet, at længden af begge vektorer passer. Dette forenkler teksten til funktionen, som ikke længere er nødvendig for at håndtere dette specielle tilfælde.
Afhængige typer er kraftige nok til at beskrive de fleste af programmernes egenskaber, så et Idris-program kan bevise invarianter på kompileringstidspunktet. Dette gør sproget til et interaktivt korrektursystem .
Idris understøtter to måder at arbejde med det automatiske bevissystem: ved at skrive successive opkald til taktik ( Coq -stil , mens sættet af tilgængelige taktikker ikke er så rigt som i Coq, men kan udvides med standard metaprogrammeringsværktøjer ) eller ved trin- for- -trinssikker udvikling ( Epigram og Agda stil ).