| Idris | |
|---|---|
| Språkklass | Funktionell |
| Framträdde i | 2007 [3] [4] [5] |
| Författare | Edwin Brady |
| Filtillägg _ | .idreller.lidr |
| Släpp | Idris 2 version 0.5.1 [1] (20 september 2021 ) |
| Typ system | strikt , statiskt , beroende typstöd |
| Blivit påverkad | Agda , Coq , [2] Epigram , Haskell , [2] ML , [2] Rust |
| Licens | BSD-3 |
| Hemsida | idris-lang.org |
Idris är ett rent , totalt funktionellt allmänt programmeringsspråk med en Haskell - liknande syntax och stöd för beroende typer [6] . Typsystemet liknar Agda -systemet .
Språket stöder automatiska korrekturer jämförbara med Coq , inklusive stöd för taktik, men fokuserar inte på dem, utan är positionerat som ett allmänt programmeringsspråk . Målen med skapandet: "tillräcklig" prestanda, enkel biverkningshantering och sätt att implementera inbäddningsbara domänspecifika språk .
Implementerat i Haskell , tillgängligt som ett Hackage- paket [7] . Idris källkod kompileras till en uppsättning mellanrepresentationer [8] och från dem till C -kod, som exekveras med hjälp av en skräpsamlare som använder Cheney-algoritmen . Officiellt implementerad är också möjligheten att kompilera till JavaScript -kod (inklusive för Node.js ). Det finns tredjepartsimplementationer av kodgeneratorer för Java , JVM , CIL , Erlang , PHP och (begränsat) LLVM .
Språket är uppkallat efter den sjungande draken Idris från 1970 års brittiska barn-tv-program Ivor the Tank Engine [9] .
Språket kombinerar funktioner från de stora populära funktionella programmeringsspråken med funktioner lånade från automatiska provsystem, vilket effektivt suddar ut gränsen mellan de två språkklasserna.
Den andra versionen av språket (släpptes 2020, baserad på den "kvantitativa typteorin" [10] ) skiljer sig markant från den första: fullt stöd för linjära typer har lagts till , koden kompileras som standard i Scheme , språkkompilatorn är skriven på själva språket .
Språkets syntax (som Agda ) är nära den för Haskell [11] . Hej världen! på Idris ser ut så här:
modul Main main : IO () main = putStrLn "Hej världen!"Skillnaderna mellan detta program och dess Haskell-motsvarighet är det enda (istället för dubbelt) kolon i huvudfunktionssignaturen och frånvaron av ordet "var" i moduldeklarationen.
Liksom de flesta moderna funktionella programmeringsspråk, stöder språket rekursiva (definierade av induktion) datatyper och parametrisk polymorfism . Sådana typer kan definieras som i den traditionella "Haskell98"-syntaxen:
data Träd a = Nod ( Träd a ) ( Träd a ) | blad aoch i den mer allmänna GADT- syntaxen:
data Träd : Typ -> Typ där Nod : Träd a -> Träd a -> Träd ett blad : a -> Träd aMed hjälp av beroende typer är det möjligt, i stadiet av typkontroll, att utföra beräkningar som involverar de värden som parametrerar typerna. Följande kod definierar en lista med en statiskt given längd, traditionellt kallad vektor :
data Vect : Nat -> Typ -> Typ där Nol : Vect 0 a (::) : ( x : a ) -> ( xs : Vect na ) -> Vect ( n + 1 ) aDenna typ kan användas så här:
total tillägg : Vect na -> Vect ma -> Vect ( n + m ) a tillägg Nil ys = ys lägg till ( x :: xs ) ys = x :: lägg till xs ysFunktionen lägger till en vektor av typelement mtill en avektor av ntypelement a. Eftersom den exakta typen av indatavektorer beror på värden som definitivt är kända vid kompileringstidpunkten, kommer den resulterande vektorn att innehålla exakt (n + m)element av typen a.
Ordet " total" anropar en analys av fullständighetskontroll mot , som, för att undvika att gå in i en oändlig loop , kommer att rapportera ett fel om funktionen inte täcker alla möjliga fall av , eller inte kan (automatiskt) bevisas.
Ett annat exempel: parvis addition av två vektorer parametriserade av deras längd:
totalt parLägg till : Num a => Vect na -> Vect na -> Vect na parAdd Noll Nol = Noll parLägg till ( x :: xs ) ( y :: ys ) = x + y :: parLägg till xs ysNumbetyder att typen atillhör typklassen Num . Funktionen klarar typkontrollen framgångsrikt, fallet när en av vektorerna kommer att ha värdet Noll, medan den andra kommer att vara ett tal, kan inte hända. Typsystemet kontrollerar vid kompilering att längden på båda vektorerna kommer att matcha. Detta förenklar texten i funktionen, som inte längre krävs för att hantera detta specialfall.
Beroende typer är tillräckligt kraftfulla för att beskriva de flesta egenskaperna hos program, så att ett Idris-program kan bevisa invarianter vid kompilering. Detta gör språket till ett interaktivt korrektursystem .
Idris stöder två sätt att arbeta med det automatiska bevissystemet: genom att skriva successiva anrop till taktik ( Coq -stil , medan uppsättningen av tillgängliga taktiker inte är lika rik som i Coq, men kan utökas med vanliga metaprogrammeringsverktyg ) eller steg för steg -stegssäker utveckling ( Epigram och Agda stil ).